text:
------------------------------------------------------------------------------
-- Streams properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Stream.PropertiesI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.Conat
open import FOTC.Data.Conat.Equality.Type
open import FOTC.Data.Colist
open import FOTC.Data.Colist.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.Stream

-----------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Stream predicate is also a pre-fixed point of the functional
-- StreamF, i.e.
--
-- StreamF Stream ≤ Stream (see FOTC.Data.Stream.Type).
Stream-in : ∀ {xs} →
            ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs' →
            Stream xs
Stream-in h = Stream-coind A h' h
  where
  A : D → Set
  A xs = ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs'

  h' : ∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'
  h' (x' , xs' , prf , Sxs') = x' , xs' , prf , Stream-out Sxs'

zeros-Stream : Stream zeros
zeros-Stream = Stream-coind A h refl
  where
  A : D → Set
  A xs = xs ≡ zeros

  h : ∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'
  h Axs = zero , zeros , trans Axs zeros-eq , refl

ones-Stream : Stream ones
ones-Stream = Stream-coind A h refl
  where
  A : D → Set
  A xs = xs ≡ ones

  h : ∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'
  h Axs = succ₁ zero , ones , trans Axs ones-eq , refl

∷-Stream : ∀ {x xs} → Stream (x ∷ xs) → Stream xs
∷-Stream {x} {xs} h = ∷-Stream-helper (Stream-out h)
  where
  ∷-Stream-helper : ∃[ x' ] ∃[ xs' ] x ∷ xs ≡ x' ∷ xs' ∧ Stream xs' →
                    Stream xs
  ∷-Stream-helper (x' , xs' , prf , Sxs') =
    subst Stream (sym (∧-proj₂ (∷-injective prf))) Sxs'

-- Version using Agda with constructor.
∷-Stream' : ∀ {x xs} → Stream (x ∷ xs) → Stream xs
∷-Stream' h with Stream-out h
... | x' , xs' , prf , Sxs' =
  subst Stream (sym (∧-proj₂ (∷-injective prf))) Sxs'

Stream→Colist : ∀ {xs} → Stream xs → Colist xs
Stream→Colist {xs} Sxs = Colist-coind A h₁ h₂
  where
  A : D → Set
  A ys = Stream ys

  h₁ : ∀ {xs} → A xs → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')
  h₁ Axs with Stream-out Axs
  ... | x' , xs' , prf , Sxs' = inj₂ (x' , xs' , prf , Sxs')

  h₂ : A xs
  h₂ = Sxs

-- Adapted from (Sander 1992, p. 59).
streamLength : ∀ {xs} → Stream xs → length xs ≈ ∞
streamLength {xs} Sxs = ≈-coind R h₁ h₂
  where
  R : D → D → Set
  R m n = ∃[ xs ] Stream xs ∧ m ≡ length xs ∧ n ≡ ∞

  h₁ : ∀ {m n} → R m n →
       m ≡ zero ∧ n ≡ zero
         ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ R m' n')
  h₁ {m} {n} (xs , Sxs , m=lxs , n≡∞) = helper₁ (Stream-out Sxs)
    where
    helper₁ : (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs') →
              m ≡ zero ∧ n ≡ zero
                ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ R m' n')
    helper₁ (x' , xs' , xs≡x'∷xs' , Sxs') =
      inj₂ (length xs'
           , ∞
           , helper₂
           , trans n≡∞ ∞-eq
           , (xs' , Sxs' , refl , refl))
        where
        helper₂ : m ≡ succ₁ (length xs')
        helper₂ = trans m=lxs (trans (lengthCong xs≡x'∷xs') (length-∷ x' xs'))

  h₂ : R (length xs) ∞
  h₂ = xs , Sxs , refl , refl

-- Adapted from (Sander 1992, p. 59). Version using Agda with
-- constructor.
streamLength' : ∀ {xs} → Stream xs → length xs ≈ ∞
streamLength' {xs} Sxs = ≈-coind R h₁ h₂
  where
  R : D → D → Set
  R m n = ∃[ xs ] Stream xs ∧ m ≡ length xs ∧ n ≡ ∞

  h₁ : ∀ {m n} → R m n →
       m ≡ zero ∧ n ≡ zero
         ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ R m' n')
  h₁ {m} (xs , Sxs , m=lxs , n≡∞) with Stream-out Sxs
  ... | x' , xs' , xs≡x'∷xs' , Sxs' =
    inj₂ (length xs' , ∞ , helper , trans n≡∞ ∞-eq , (xs' , Sxs' , refl , refl))
    where
    helper : m ≡ succ₁ (length xs')
    helper = trans m=lxs (trans (lengthCong xs≡x'∷xs') (length-∷ x' xs'))

  h₂ : R (length xs) ∞
  h₂ = xs , Sxs , refl , refl

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --sized-types #-}

module SizedTypesScopeExtrusion where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

data Empty : Set where

data Unit : Set where
  unit : Unit

Zero : (i : Size) -> Nat {i} -> Set
Zero ._ zero = Unit
Zero ._ (suc _) = Empty

bla : Set
bla = (x : Nat) -> (i : Size) -> Zero i x

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module DifferentArities where

open import Common.Equality
open import Common.Prelude

f : Nat → Nat → Nat
f zero      = λ x → x
f (suc n) m = f n (suc m)

testf1 : f zero ≡ λ x → x
testf1 = refl

testf2 : ∀ {n m} → f (suc n) m ≡ f n (suc m)
testf2 = refl

testf3 : f 4 5 ≡ 9
testf3 = refl

-- Andreas, 2015-01-21 proper matching on additional argument

Sum : Nat → Set
Sum 0       = Nat
Sum (suc n) = Nat → Sum n

sum : (acc : Nat) (n : Nat) → Sum n
sum acc 0         = acc
sum acc (suc n) 0 = sum acc n
sum acc (suc n) m = sum (m + acc) n

nzero : (n : Nat) → Sum n
nzero 0 = 0
nzero (suc n) m = nzero n

mult :  (acc : Nat) (n : Nat) → Sum n
mult acc 0         = acc
mult acc (suc n) 0 = nzero n
mult acc (suc n) m = mult (m * acc) n

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module safety where

open import Algebra
open import Data.List
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Rational
open import Data.Rational.Properties
open import Data.Nat using (z≤n; s≤s)
open import Data.Integer using (+≤+; +<+; +_)
open import Data.Vec using (_∷_)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality

open import Vehicle.Data.Tensor

open ≤-Reasoning

------------------------------------------------------------------------
-- Things to work out how to put in standard library

2ℚ = + 2 / 1
3ℚ = + 3 / 1

p+q-q≡p : ∀ p q → p + q - q ≡ p
p+q-q≡p p q = begin-equality
  p + q - q   ≡⟨ +-assoc p q (- q) ⟩
  p + (q - q) ≡⟨ cong (λ v → p + v) (+-inverseʳ q) ⟩
  p + 0ℚ      ≡⟨ +-identityʳ p ⟩
  p           ∎

+-isCommutativeSemigroup : IsCommutativeSemigroup _≡_ _+_
+-isCommutativeSemigroup = isCommutativeSemigroup
  where open IsCommutativeMonoid +-0-isCommutativeMonoid

+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
  { isCommutativeSemigroup = +-isCommutativeSemigroup
  }

2*x≡x+x : ∀ p → 2ℚ * p ≡ p + p
2*x≡x+x p = begin-equality
  2ℚ * p          ≡⟨⟩
  (1ℚ + 1ℚ) * p   ≡⟨ *-distribʳ-+ p 1ℚ 1ℚ ⟩
  1ℚ * p + 1ℚ * p ≡⟨ cong₂ _+_ (*-identityˡ p) (*-identityˡ p) ⟩
  p + p           ∎

open import Algebra.Properties.CommutativeSemigroup +-commutativeSemigroup

------------------------------------------------------------------------
-- The controller

postulate controller : ℚ → ℚ → ℚ

postulate controller-lem : ∀ x y → ∣ x ∣ < 3ℚ → ∣ controller x y + 2ℚ * x - y ∣ < 2ℚ

------------------------------------------------------------------------
-- The model

record State : Set where
  no-eta-equality
  field
    windSpeed : ℚ
    position  : ℚ
    velocity  : ℚ

open State

initialState : State
initialState = record
  { windSpeed = 0ℚ
  ; position  = 0ℚ
  ; velocity  = 0ℚ
  }

nextState : ℚ → State → State
nextState changeInWindSpeed s = record
  { windSpeed = newWindSpeed
  ; position  = newPosition
  ; velocity  = velocity s + controller newPosition (position s)
  }
  where
  newWindSpeed = windSpeed s + changeInWindSpeed
  newPosition  = position s + velocity s + newWindSpeed

finalState : List ℚ → State
finalState xs = foldr nextState initialState xs

------------------------------------------------------------------------
-- Definition and proof of safety

stateSum : State → ℚ
stateSum s = position s + velocity s + windSpeed s

Safe : State → Set
Safe s = ∣ position s ∣ < 3ℚ

Good : State → Set
Good s = ∣ stateSum s ∣ < 2ℚ

LowWind : ℚ → Set
LowWind x = ∣ x ∣ ≤ 1ℚ

-- A state being good will imply the next state is safe

good⇒nextSafe : ∀ dw → ∣ dw ∣ ≤ 1ℚ → ∀ s → Good s → Safe (nextState dw s)
good⇒nextSafe dw ∣dw∣≤1 s ∣Σ∣<2 =  begin-strict
  ∣ (position s + velocity s) + (windSpeed s + dw) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (position s + velocity s) (windSpeed s) dw) ⟩
  ∣ (position s + velocity s) + windSpeed s + dw   ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (stateSum s) dw ⟩
  ∣ position s + velocity s + windSpeed s ∣ + ∣ dw ∣ <⟨ +-monoˡ-< ∣ dw ∣ ∣Σ∣<2 ⟩
  2ℚ + ∣ dw ∣                                        ≤⟨ +-monoʳ-≤ 2ℚ ∣dw∣≤1 ⟩
  2ℚ + 1ℚ                                            ≡⟨⟩
  3ℚ                                                 ∎

-- Initial state is both safe and good

initialState-safe : Safe initialState
initialState-safe = *<* (+<+ (s≤s z≤n))

initialState-good : Good initialState
initialState-good = *<* (+<+ (s≤s z≤n))

good⇒nextGood : ∀ dw → ∣ dw ∣ ≤ 1ℚ → ∀ s → Good s → Good (nextState dw s)
good⇒nextGood dw ∣dw∣≤1 s Σ≤2 =
  let
    s' = nextState dw s
    dv = controller (position s') (position s)
    s'-safe = good⇒nextSafe dw ∣dw∣≤1 s Σ≤2
  in
  begin-strict
    ∣ position s' + velocity s' + windSpeed s' ∣                                 ≡⟨⟩
    ∣ position s' + (velocity s + dv) + windSpeed s' ∣                           ≡⟨ cong (λ v → ∣ v + windSpeed s' ∣) (x∙yz≈zx∙y (position s') (velocity s) dv) ⟩
    ∣ dv + position s' + velocity s + windSpeed s'   ∣                           ≡⟨ cong ∣_∣ (sym (p+q-q≡p (dv + position s' + velocity s + windSpeed s') (position s))) ⟩
    ∣ dv + position s' + velocity s + windSpeed s' + position s - position s ∣   ≡⟨ cong (λ v → ∣ v + position s - position s ∣) (+-assoc (dv + position s') (velocity s) (windSpeed s'))  ⟩
    ∣ dv + position s' + (velocity s + windSpeed s') + position s - position s ∣ ≡⟨ cong (λ v → ∣ v - position s ∣) (+-assoc (dv + position s') (velocity s + windSpeed s') (position s)) ⟩
    ∣ dv + position s' + (velocity s + windSpeed s' + position s) - position s ∣ ≡⟨ cong (λ v → ∣ dv + position s' + v - position s ∣) (xy∙z≈zx∙y (velocity s) (windSpeed s') (position s)) ⟩
    ∣ dv + position s' + (position s + velocity s + windSpeed s') - position s ∣ ≡⟨⟩
    ∣ dv + position s' + position s' - position s ∣                              ≡⟨ cong (λ v → ∣ v - position s ∣) (+-assoc dv (position s') (position s')) ⟩
    ∣ dv + (position s' + position s') - position s ∣                            ≡⟨ cong (λ v → ∣ dv + v - position s ∣) (sym (2*x≡x+x (position s'))) ⟩
    ∣ dv + 2ℚ * position s' - position s ∣                                       <⟨ controller-lem (position s') (position s) s'-safe ⟩
    2ℚ                                                                           ∎

finalState-good : ∀ xs → All LowWind xs → Good (finalState xs)
finalState-good []       []         = initialState-good
finalState-good (x ∷ xs) (px ∷ pxs) = good⇒nextGood x px (finalState xs) (finalState-good xs pxs)

finalState-safe : ∀ xs → All LowWind xs → Safe (finalState xs)
finalState-safe []       []         = initialState-safe
finalState-safe (x ∷ xs) (px ∷ pxs) = good⇒nextSafe x px (finalState xs) (finalState-good xs pxs)

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


text:
------------------------------------------------------------------------
-- Finite maps, i.e. lookup tables (currently only some type
-- signatures)
------------------------------------------------------------------------

module Data.Map where

open import Relation.Nullary
open import Relation.Binary
open import Data.List as L using (List)
open import Data.Product

module Map₁ (key-dto : DecTotalOrder) (elem-s : Setoid) where

  open DecTotalOrder key-dto renaming (carrier to key)
  open Setoid elem-s         renaming (carrier to elem; _≈_ to _≗_)

  infixr 6 _∪_
  infix  5 _∈?_
  infix  4 _∈_ _|≈|_

  abstract postulate decSetoid : DecSetoid

  Map : Set
  Map = Setoid.carrier (DecSetoid.setoid decSetoid)

  _|≈|_ : Rel Map
  _|≈|_ = Setoid._≈_ (DecSetoid.setoid decSetoid)

  abstract
   postulate
    empty  : Map
    insert : key → elem → Map → Map
    _∪_    : Map → Map → Map
    _∈_    : key → Map → Set
    _↦_∈_  : key → elem → Map → Set

  data LookupResult (k : key) (s : Map) : Set where
    found    : (e : elem) (k↦e∈s : k ↦ e ∈ s) → LookupResult k s
    notFound : (k∉s : ¬ k ∈ s) → LookupResult k s

  abstract
   postulate
    _∈?_   : (k : key) → (s : Map) → LookupResult k s
    toList : Map → List (key × elem)

   postulate
    prop-∈₁ : ∀ {x v s}   → x ↦ v ∈ s → x ∈ s
    prop-∈₂ : ∀ {x s}     → x ∈ s → Σ elem (λ v → x ↦ v ∈ s)
    prop-∈₃ : ∀ {x v w s} → x ↦ v ∈ s → x ↦ w ∈ s → v ≗ w

    prop-∈-insert₁ : ∀ {x y v w s} →
                     x ≈ y → v ≗ w → x ↦ v ∈ insert y w s
    prop-∈-insert₂ : ∀ {x y v w s} →
                     ¬ x ≈ y → x ↦ v ∈ s → x ↦ v ∈ insert y w s
    prop-∈-insert₃ : ∀ {x y v w s} →
                     ¬ x ≈ y → x ↦ v ∈ insert y w s → x ↦ v ∈ s

    prop-∈-empty : ∀ {x} → ¬ x ∈ empty

    prop-∈-∪ : ∀ {x s₁ s₂} → x ∈ s₁ → x ∈ s₁ ∪ s₂

    prop-∪₁ : ∀ {s₁ s₂}    → s₁ ∪ s₂        |≈| s₂ ∪ s₁
    prop-∪₂ : ∀ {s₁ s₂ s₃} → s₁ ∪ (s₂ ∪ s₃) |≈| (s₁ ∪ s₂) ∪ s₃

    prop-∈-|≈|₁ : ∀ {x}   → (λ s → x ∈ s)     Respects _|≈|_
    prop-∈-|≈|₂ : ∀ {x v} → (λ s → x ↦ v ∈ s) Respects _|≈|_
    prop-∈-≈₁   : ∀ {s}   → (λ x → x ∈ s)     Respects _≈_
    prop-∈-≈₂   : ∀ {v s} → (λ x → x ↦ v ∈ s) Respects _≈_
    prop-∈-≗    : ∀ {x s} → (λ v → x ↦ v ∈ s) Respects _≗_

    -- TODO: Postulates for toList.

  singleton : key → elem → Map
  singleton k v = insert k v empty

  ⋃_ : List Map → Map
  ⋃_ = L.foldr _∪_ empty

  fromList : List (key × elem) → Map
  fromList = L.foldr (uncurry insert) empty

open Map₁ public renaming (Map to _⇰_)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module List.Permutation.Alternative (A : Set) where

open import Data.List

data _∼_ : List A → List A → Set where
  ∼refl : {xs : List A}
                   → xs ∼ xs
  ∼trans : {xs ys zs : List A}
                   → xs ∼ ys
                   → ys ∼ zs
                   → xs ∼ zs
  ∼head : {xs ys : List A}(x : A)
                   → xs ∼ ys
                   → (x ∷ xs) ∼ (x ∷ ys)
  ∼swap : {xs ys : List A}{x y : A}
                   → (x ∷ y ∷ xs) ∼ ys
                   → (y ∷ x ∷ xs) ∼ ys

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Data.Binary.Tests.Semantics where

open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.List as List using (List; _∷_; [])
open import Relation.Binary.PropositionalEquality

prop : ℕ → Set
prop n = let xs = List.upTo n in List.map (λ x → ⟦ ⟦ x ⇑⟧ ⇓⟧ ) xs ≡ xs

_ : prop 50
_ = refl

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module CTL.Modalities.AF where

open import FStream.Core
open import Library

-- Certainly sometime : s₀ ⊧ φ ⇔ ∀ s₀ R s₁ R ... ∃ i . sᵢ ⊧ φ
-- TODO Unclear whether this needs sizes
data AF' {ℓ₁ ℓ₂} {C : Container ℓ₁}
     (props : FStream' C (Set ℓ₂)) : Set (ℓ₁ ⊔ ℓ₂) where
  alreadyA : head props → AF' props
  notYetA  : A (fmap AF' (inF (tail props))) → AF' props
open AF' public

AF : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁}
     → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
AF props = APred AF' (inF props)

mutual
  AFₛ' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  head (AFₛ' props) = AF' props
  tail (AFₛ' props) = AFₛ (tail props)

  AFₛ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁}
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  inF (AFₛ props) = fmap AFₛ' (inF props)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
-- Andreas, 2011-04-26
{-# OPTIONS --universe-polymorphism #-}
module Issue411 where
import Common.Irrelevance

record A : Set₁ where
  field
    .foo : Set
-- this yielded a panic "-1 not a valid deBruijn index" due to old code for assignS


text:
{-# OPTIONS --without-K --safe #-}

open import Relation.Binary using (Rel)

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Morphism.Definitions
  {k ℓᵏ} (K : Field k ℓᵏ)
  {a} (A : Set a)
  {b} (B : Set b)
  {ℓ} (_≈_ : Rel B ℓ)
  where

open import Algebra.Linear.Core
open import Function

import Algebra.Morphism as Morphism
open Morphism.Definitions A B _≈_

private
  K' : Set k
  K' = Field.Carrier K

Linear : Morphism
       -> VectorAddition A -> ScalarMultiplication K' A
       -> VectorAddition B -> ScalarMultiplication K' B
       -> Set _
Linear ⟦_⟧ _+₁_ _∙₁_ _+₂_ _∙₂_ =
  ∀ (a b : K') (u v : A) ->
    ⟦ (a ∙₁ u) +₁ (b ∙₁ v) ⟧ ≈ ((a ∙₂ ⟦ u ⟧) +₂ (b ∙₂ ⟦ v ⟧))

ScalarHomomorphism : Morphism
                   -> ScalarMultiplication K' A
                   -> ScalarMultiplication K' B
                   -> Set _
ScalarHomomorphism ⟦_⟧ _∙_ _∘_ = ∀ (c : K') (u : A) -> ⟦ c ∙ u ⟧ ≈ (c ∘ ⟦ u ⟧)

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module SafeFlagPrimTrustMe where

open import Agda.Builtin.Equality

private
 primitive
   primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- statically checked sorted lists
-- see http://www2.tcs.ifi.lmu.de/~abel/DepTypes.pdf

module SortedList where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Bool using (Bool; true; false)

----------------------------------------------------------------------
-- Curry-Howard stuff

Proposition = Set

-- intentionally blank. signifies the empty set in the type system.
data Absurd : Proposition where

-- tt = trivially true
data Truth : Proposition where
  tt : Truth

-- ∧ = conjunction
data _∧_ (A B : Proposition) : Proposition where
    _,_ : A → B → A ∧ B

fst : {A B : Proposition} → A ∧ B → A
fst (a , b) = a

snd : {A B : Proposition} → A ∧ B → B
snd (a , b) = b

-- Cartesian product = conjunction
_×_ = _∧_

-- ∨ = disjunction
data _∨_ (A B : Proposition) : Proposition where
  inl : A → A ∨ B
  inr : B → A ∨ B

-- given: A or B is true, A implies C, B implies C. then C is true.
case : {A B C : Proposition} → A ∨ B → (A → C) → (B → C) → C
case (inl a) f g = f a
case (inr b) f g = g b

-- map booleans to propositions by mapping true to Truth and false to Absurd
True : Bool → Proposition
True true = Truth
True false = Absurd

----------------------------------------------------------------------

_≤_ : ℕ → ℕ → Bool
zero ≤ n = true
suc m ≤ zero = false
suc m ≤ suc n = m ≤ n

-- proposition: ≤ is reflexive. proof: induction.
refl≤ : (n : ℕ) → True (n ≤ n)
refl≤ zero = tt
refl≤ (suc n) = refl≤ n

----------------------------------------------------------------------

data SortedList : ℕ → Set where
  ∅ : SortedList zero
  ⋉ : {n : ℕ} (m : ℕ) → True (n ≤ m) → SortedList n → SortedList m

-- the arguments to ⋉ are
-- m : a natural number to prepend to the given sorted list xs
-- p : a proof that m (the new head) is ≥ head xs
-- xs : a list such that head xs = n

-- for constant natural numbers, proofs that n ≤ m are trivial since
-- ≤ is decidable; this is why we pass in `tt` in the examples below

-- examples:
one : ℕ
one = suc zero

s1 = ⋉ one tt (⋉ zero tt ∅)
-- s2 = ⋉ zero tt (⋉ one tt ∅) -- fails statically, as desired
s3 = ⋉ one tt s1       -- normal form: ⋉ 1 tt (⋉ 1 tt (⋉ 0 tt ∅))
s4 = ⋉ (suc one) tt s1 -- normal form: ⋉ 2 tt (⋉ 1 tt (⋉ 0 tt ∅))

max_stars_repo_name: sshastry/agda-examples

max_issues_repo_name: sshastry/agda-examples

max_forks_repo_name: sshastry/agda-examples


text:
module 110-natural-model where

open import 010-false-true
open import 020-equivalence
open import 100-natural

-- We prove that there is a model of the naturals within Agda's lambda
-- calculus. This also shows that the Peano axioms are consistent.

data ℕ : Set where
  zero : ℕ
  suc : ℕ -> ℕ

thm-ℕ-is-natural : Natural zero suc _≡_
thm-ℕ-is-natural = record {
  equiv = thm-≡-is-equivalence;
  sucn!=zero = sucn!=zero;
  sucinjective = sucinjective;
  cong = cong;
  induction = induction
  }
  where
    sucn!=zero : ∀ {r} -> suc r ≡ zero -> False
    sucn!=zero ()
    sucinjective : ∀ {r s} -> suc r ≡ suc s -> r ≡ s
    sucinjective refl = refl
    cong : ∀ {r s} -> r ≡ s -> suc r ≡ suc s
    cong refl = refl

    -- This is the only tricky bit: proving the principle of induction.
    induction : (p : ℕ -> Set) -> p zero -> (∀ n -> p n -> p (suc n)) -> ∀ n -> p n
    -- We first prove that p n holds for n equal to zero. This is just
    -- the base case.
    induction p base hypothesis zero = base
    -- Then we prove that p (suc n) holds, using induction on n, that is,
    -- we may assume that p n is proven, or more precisely, that
    -- "induction p base hypothesis n" is a proof of p n.
    induction p base hypothesis (suc n) =
      hypothesis n (induction p base hypothesis n)

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.NType2
open import lib.types.Int
open import lib.types.Group
open import lib.types.List
open import lib.types.Word
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.FreeAbelianGroup
open import lib.groups.GeneratedGroup
open import lib.types.SetQuotient

module lib.groups.Int where

ℤ-group-structure : GroupStructure ℤ
ℤ-group-structure = record
  { ident = 0
  ; inv = ℤ~
  ; comp = _ℤ+_
  ; unit-l = ℤ+-unit-l
  ; assoc = ℤ+-assoc
  ; inv-l = ℤ~-inv-l
  }

ℤ-group : Group₀
ℤ-group = group _ ℤ-group-structure

ℤ-group-is-abelian : is-abelian ℤ-group
ℤ-group-is-abelian = ℤ+-comm

ℤ-abgroup : AbGroup₀
ℤ-abgroup = ℤ-group , ℤ-group-is-abelian

private
  module OneGeneratorFreeAbGroup = FreeAbelianGroup Unit

OneGenFreeAbGroup : AbGroup lzero
OneGenFreeAbGroup = OneGeneratorFreeAbGroup.FreeAbGroup

private
  module OneGenFreeAbGroup = AbGroup OneGenFreeAbGroup

ℤ-iso-FreeAbGroup-Unit : ℤ-group ≃ᴳ OneGenFreeAbGroup.grp
ℤ-iso-FreeAbGroup-Unit = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  open OneGeneratorFreeAbGroup
  module F = Freeness ℤ-abgroup
  to : Group.El ℤ-group → OneGenFreeAbGroup.El
  to = OneGenFreeAbGroup.exp qw[ inl unit :: nil ]
  from : OneGenFreeAbGroup.El → Group.El ℤ-group
  from = GroupHom.f (F.extend (λ _ → 1))
  abstract
    to-pres-comp = OneGenFreeAbGroup.exp-+ qw[ inl unit :: nil ]

    to-from' : ∀ l → to (Word-extendᴳ ℤ-group (λ _ → 1) l) == qw[ l ]
    to-from' nil = idp
    to-from' (inl unit :: nil) = idp
    to-from' (inl unit :: l@(_ :: _)) =
        OneGenFreeAbGroup.exp-succ qw[ inl unit :: nil ] (Word-extendᴳ ℤ-group (λ _ → 1) l)
      ∙ ap (OneGenFreeAbGroup.comp qw[ inl unit :: nil ]) (to-from' l)
    to-from' (inr unit :: nil) = idp
    to-from' (inr unit :: l@(_ :: _)) =
        OneGenFreeAbGroup.exp-pred qw[ inl unit :: nil ] (Word-extendᴳ ℤ-group (λ _ → 1) l)
      ∙ ap (OneGenFreeAbGroup.comp qw[ inr unit :: nil ]) (to-from' l)

    to-from : ∀ fs → to (from fs) == fs
    to-from = QuotWord-elim to-from' (λ _ → prop-has-all-paths-↓)

    from-to : ∀ z → from (to z) == z
    from-to (pos 0) = idp
    from-to (pos 1) = idp
    from-to (negsucc 0) = idp
    from-to (pos (S (S n))) =
        GroupHom.pres-comp (F.extend (λ _ → 1))
          qw[ inl unit :: nil ] (OneGenFreeAbGroup.exp qw[ inl unit :: nil ] (pos (S n)))
      ∙ ap succ (from-to (pos (S n)))
    from-to (negsucc (S n)) =
        GroupHom.pres-comp (F.extend (λ _ → 1))
          qw[ inr unit :: nil ] (OneGenFreeAbGroup.exp qw[ inl unit :: nil ] (negsucc n))
      ∙ ap pred (from-to (negsucc n))

exp-shom : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) (g : GEl) → ℤ-group-structure →ᴳˢ GS
exp-shom GS g = group-structure-hom (GroupStructure.exp GS g) (GroupStructure.exp-+ GS g)

exp-hom : ∀ {i} (G : Group i) (g : Group.El G) → ℤ-group →ᴳ G
exp-hom G g = group-hom (Group.exp G g) (Group.exp-+ G g)

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module _ where

open import Common.Prelude

print : Float → IO Unit
print x = putStrLn (primShowFloat x)

printB : Bool → IO Unit
printB true  = putStrLn "true"
printB false = putStrLn "false"

_/_   = primFloatDiv
_==_  = primFloatEquality
_=N=_ = primFloatNumericalEquality
_<N_  = primFloatNumericalLess
_<_   = primFloatLess

NaN : Float
NaN = 0.0 / 0.0

-NaN : Float
-NaN = primFloatNegate NaN

Inf : Float
Inf = 1.0 / 0.0

-Inf : Float
-Inf = -1.0 / 0.0

sin   = primSin
cos   = primCos
tan   = primTan
asin  = primASin
acos  = primACos
atan  = primATan
atan2 = primATan2

isZero : Float → String
isZero 0.0  = "pos"
isZero -0.0 = "neg"
isZero _    = "nonzero"

main : IO Unit
main =
  putStr "123.4 = " ,, print 123.4 ,,
  putStr "-42.9 = " ,, print -42.9 ,,

  -- Disabled because Issue #2359.
  -- putStr "1.0   = " ,, print 1.0 ,,
  -- putStr "-0.0  = " ,, print -0.0  ,,

  putStr "NaN   = " ,, print NaN   ,,
  putStr "Inf   = " ,, print Inf   ,,
  putStr "-Inf  = " ,, print -Inf  ,,

  putStr "Inf == Inf = " ,, printB (Inf == Inf) ,,

  -- Issues #2155 and #2194.
  putStr "NaN == NaN = " ,, printB (NaN == NaN) ,,
  -- Issue #2194.
  putStr "NaN == -NaN = " ,, printB (NaN == (primFloatNegate NaN)) ,,

  -- Issue #2169.
  putStr "0.0 == -0.0 = " ,, printB (0.0 == -0.0) ,,

  -- Issue #2216
  putStr "isZero  0.0 = " ,, putStrLn (isZero 0.0) ,,
  putStr "isZero -0.0 = " ,, putStrLn (isZero -0.0) ,,
  putStr "isZero  1.0 = " ,, putStrLn (isZero 1.0) ,,

  -- numerical equality
  putStr "NaN =N= NaN  = " ,, printB (NaN =N= NaN) ,,
  putStr "0.0 =N= -0.0 = " ,, printB (0.0 =N= -0.0) ,,
  putStr "0.0 =N= 12.0 = " ,, printB (0.0 =N= 12.0) ,,

  putStr "NaN  < -Inf = " ,, printB (NaN < -Inf) ,,
  putStr "-Inf < NaN  = " ,, printB (-Inf < NaN) ,,
  putStr "0.0  < -0.0 = " ,, printB (0.0 < -0.0) ,,
  putStr "-0.0 < 0.0  = " ,, printB (-0.0 < 0.0) ,,

  -- Issue #2208.
  putStr "NaN  < NaN  = " ,, printB (NaN < NaN) ,,
  putStr "-NaN < -NaN = " ,, printB (-NaN < -NaN) ,,
  putStr "NaN  < -NaN = " ,, printB (NaN < -NaN) ,,
  putStr "-NaN < NaN  = " ,, printB (-NaN < NaN) ,,
  putStr "NaN  < -5.0 = " ,, printB (NaN < -5.0) ,,
  putStr "-5.0 < NaN  = " ,, printB (-5.0 < NaN) ,,

  putStr "NaN  <N -Inf = " ,, printB (NaN <N -Inf) ,,
  putStr "-Inf <N NaN  = " ,, printB (-Inf <N NaN) ,,
  putStr "0.0  <N -0.0 = " ,, printB (0.0 <N -0.0) ,,
  putStr "-0.0 <N 0.0  = " ,, printB (-0.0 <N 0.0) ,,

  -- Issue #2208.
  putStr "NaN  <N NaN  = " ,, printB (NaN <N NaN) ,,
  putStr "-NaN <N -NaN = " ,, printB (-NaN <N -NaN) ,,
  putStr "NaN  <N -NaN = " ,, printB (NaN <N -NaN) ,,
  putStr "-NaN <N NaN  = " ,, printB (-NaN <N NaN) ,,
  putStr "NaN  <N -5.0 = " ,, printB (NaN <N -5.0) ,,
  putStr "-5.0 <N NaN  = " ,, printB (-5.0 <N NaN) ,,

  putStr "e                   = " ,, print (primExp 1.0) ,,
  putStr "sin (asin 0.6)      = " ,, print (sin (asin 0.6)) ,,
  putStr "cos (acos 0.6)      = " ,, print (cos (acos 0.6)) ,,
  putStr "tan (atan 0.4)      = " ,, print (tan (atan 0.4)) ,,
  putStr "tan (atan2 0.4 1.0) = " ,, print (tan (atan2 0.4 1.0)) ,,
  return unit

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Morphism
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Algebra.Linear.Morphism.Definitions K public
open import Algebra.Linear.Morphism.Bundles     K public
open import Algebra.Linear.Morphism.VectorSpace K public


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Reflection.StrictEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv.Base
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.List.Base
open import Cubical.Data.Unit.Base

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

strictEquivClauses : R.Term → R.Term → List R.Clause
strictEquivClauses f g =
  R.clause []
    (R.proj (quote fst) v∷ [])
    f
  ∷ R.clause []
    (R.proj (quote snd) v∷ R.proj (quote equiv-proof) v∷ [])
    (R.def (quote strictContrFibers) (g v∷ []))
  ∷ []

strictEquivTerm : R.Term → R.Term → R.Term
strictEquivTerm f g = R.pat-lam (strictEquivClauses f g) []

strictEquivMacro : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (A → B) → (B → A) → R.Term → R.TC Unit
strictEquivMacro {A = A} {B} f g hole =
  R.quoteTC (A ≃ B) >>= λ equivTy →
  R.checkType hole equivTy >>
  R.quoteTC f >>= λ `f` →
  R.quoteTC g >>= λ `g` →
  R.unify (strictEquivTerm `f` `g`) hole

strictIsoToEquivMacro : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → Iso A B → R.Term → R.TC Unit
strictIsoToEquivMacro isom =
  strictEquivMacro (Iso.fun isom) (Iso.inv isom)

-- For use with unquoteDef

defStrictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → (A → B) → (B → A) → R.TC Unit
defStrictEquiv idName f g =
  R.quoteTC f >>= λ `f` →
  R.quoteTC g >>= λ `g` →
  R.defineFun idName (strictEquivClauses `f` `g`)

defStrictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → Iso A B → R.TC Unit
defStrictIsoToEquiv idName isom =
  defStrictEquiv idName (Iso.fun isom) (Iso.inv isom)

-- For use with unquoteDef

declStrictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → (A → B) → (B → A) → R.TC Unit
declStrictEquiv {A = A} {B = B} idName f g =
  R.quoteTC (A ≃ B) >>= λ ty →
  R.declareDef (varg idName) ty >>
  defStrictEquiv idName f g

declStrictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → R.Name → Iso A B → R.TC Unit
declStrictIsoToEquiv idName isom =
  declStrictEquiv idName (Iso.fun isom) (Iso.inv isom)

macro
  -- (f : A → B) → (g : B → A) → (A ≃ B)
  -- Assumes that `f` and `g` are inverse up to definitional equality
  strictEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
    → (A → B) → (B → A) → R.Term → R.TC Unit
  strictEquiv = strictEquivMacro

  -- (isom : Iso A B) → (A ≃ B)
  -- Assumes that the functions defining `isom` are inverse up to definitional equality
  strictIsoToEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
    → Iso A B → R.Term → R.TC Unit
  strictIsoToEquiv = strictIsoToEquivMacro

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-# OPTIONS --without-K --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.ShapeView {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Agda.Primitive

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Reflexivity

open import Tools.Embedding
open import Tools.Product
open import Tools.Empty using (⊥; ⊥-elim ; ⊥-elimω)
import Tools.PropositionalEquality as PE

-- Type for maybe embeddings of reducible types
data MaybeEmb (l : TypeLevel) (⊩⟨_⟩ : TypeLevel → Set) : Set where
  noemb : ⊩⟨ l ⟩ → MaybeEmb l ⊩⟨_⟩
  emb   : ∀ {l′} → l′ < l → MaybeEmb l′ ⊩⟨_⟩ → MaybeEmb l ⊩⟨_⟩

-- Specific reducible types with possible embedding

_⊩⟨_⟩U : (Γ : Con Term) (l : TypeLevel) → Set
Γ ⊩⟨ l ⟩U = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩U)

_⊩⟨_⟩ℕ_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩ℕ A = MaybeEmb l (λ l′ → Γ ⊩ℕ A)

_⊩⟨_⟩ne_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩ne A = MaybeEmb l (λ l′ → Γ ⊩ne A)

data _⊩⟨_⟩Π_ (Γ : Con Term) (l : TypeLevel) (A : Term) : Setω where
  noemb : Γ ⊩′⟨ l ⟩Π A → Γ ⊩⟨ l ⟩Π A
  emb : ∀ {l′} → l′ < l → Γ ⊩⟨ l′ ⟩Π A → Γ ⊩⟨ l ⟩Π A

-- -- Construct a general reducible type from a specific

U-intr : ∀ {Γ l} → Γ ⊩⟨ l ⟩U → Γ ⊩⟨ l ⟩ U
U-intr (noemb (Uᵣ l′ l< ⊢Γ)) = Uᵣ′ l′ l< ⊢Γ
U-intr (emb 0<1 x) = emb′ 0<1 (U-intr x)

ℕ-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩ℕ A → Γ ⊩⟨ l ⟩ A
ℕ-intr (noemb x) = ℕᵣ x
ℕ-intr (emb 0<1 x) = emb′ 0<1 (ℕ-intr x)

ne-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩ne A → Γ ⊩⟨ l ⟩ A
ne-intr (noemb x) = LRPack _ _ _ (LRne x)
ne-intr (emb 0<1 x) = emb′ 0<1 (ne-intr x)

Π-intr : ∀ {A Γ l} → Γ ⊩⟨ l ⟩Π A → Γ ⊩⟨ l ⟩ A
Π-intr (noemb x) = LRPack _ _ _ (LRΠ x)
Π-intr (emb 0<1 x) = emb′ 0<1 (Π-intr x)

-- -- Construct a specific reducible type from a general with some criterion

U-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ U → Γ ⊩⟨ l ⟩U
U-elim (Uᵣ′ l′ l< ⊢Γ) = noemb (Uᵣ l′ l< ⊢Γ)
U-elim (ℕᵣ D) = ⊥-elim (U≢ℕ (whnfRed* (red D) Uₙ))
U-elim (ne′ K D neK K≡K) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-elim (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = ⊥-elim (U≢Π (whnfRed* (red D) Uₙ))
U-elim (emb′ 0<1 x) with U-elim x
U-elim (emb′ 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
U-elim (emb′ 0<1 x) | emb () x₁

ℕ-elim′ : ∀ {A Γ l} → Γ ⊢ A ⇒* ℕ → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩ℕ A
ℕ-elim′ D (Uᵣ′ l′ l< ⊢Γ) = ⊥-elim (U≢ℕ (whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , ℕₙ)))
ℕ-elim′ D (ℕᵣ D′) = noemb D′
ℕ-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (ℕ≢ne neK (whrDet* (D , ℕₙ) (red D′ , ne neK)))
ℕ-elim′ D (Πᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (ℕ≢Π (whrDet* (D , ℕₙ) (red D′ , Πₙ)))
ℕ-elim′ D (emb′ 0<1 x) with ℕ-elim′ D x
ℕ-elim′ D (emb′ 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
ℕ-elim′ D (emb′ 0<1 x) | emb () x₂

ℕ-elim : ∀ {Γ l} → Γ ⊩⟨ l ⟩ ℕ → Γ ⊩⟨ l ⟩ℕ ℕ
ℕ-elim [ℕ] = ℕ-elim′ (id (escape [ℕ])) [ℕ]

ne-elim′ : ∀ {A Γ l K} → Γ ⊢ A ⇒* K → Neutral K → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩ne A
ne-elim′ D neK (Uᵣ′ l′ l< ⊢Γ) =
  ⊥-elim (U≢ne neK (whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , ne neK)))
ne-elim′ D neK (ℕᵣ D′) = ⊥-elim (ℕ≢ne neK (whrDet* (red D′ , ℕₙ) (D , ne neK)))
ne-elim′ D neK (ne′ K D′ neK′ K≡K) = noemb (ne K D′ neK′ K≡K)
ne-elim′ D neK (Πᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Π≢ne neK (whrDet* (red D′ , Πₙ) (D , ne neK)))
ne-elim′ D neK (emb′ 0<1 x) with ne-elim′ D neK x
ne-elim′ D neK (emb′ 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
ne-elim′ D neK (emb′ 0<1 x) | emb () x₂

ne-elim : ∀ {Γ l K} → Neutral K  → Γ ⊩⟨ l ⟩ K → Γ ⊩⟨ l ⟩ne K
ne-elim neK [K] = ne-elim′ (id (escape [K])) neK [K]

Π-elim′ : ∀ {A Γ F G l} → Γ ⊢ A ⇒* Π F ▹ G → Γ ⊩⟨ l ⟩ A → Γ ⊩⟨ l ⟩Π A
Π-elim′ D (Uᵣ′ l′ l< ⊢Γ) = ⊥-elimω (U≢Π (whrDet* (id (Uⱼ ⊢Γ) , Uₙ) (D , Πₙ)))
Π-elim′ D (ℕᵣ D′) = ⊥-elimω (ℕ≢Π (whrDet* (red D′ , ℕₙ) (D , Πₙ)))
Π-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elimω (Π≢ne neK (whrDet* (D , Πₙ) (red D′ , ne neK)))
Π-elim′ D (Πᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  noemb (Πᵣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
Π-elim′ D (emb′ 0<1 x) with Π-elim′ D x
Π-elim′ D (emb′ 0<1 x) | noemb x₁ = emb 0<1 (noemb x₁)
Π-elim′ D (emb′ 0<1 x) | emb () x₂

Π-elim : ∀ {Γ F G l} → Γ ⊩⟨ l ⟩ Π F ▹ G → Γ ⊩⟨ l ⟩Π Π F ▹ G
Π-elim [Π] = Π-elim′ (id (escape [Π])) [Π]

-- Extract a type and a level from a maybe embedding
extractMaybeEmb : ∀ {l ⊩⟨_⟩} → MaybeEmb l ⊩⟨_⟩ → ∃ λ l′ → ⊩⟨ l′ ⟩
extractMaybeEmb (noemb x) = _ , x
extractMaybeEmb (emb 0<1 x) = extractMaybeEmb x

extractMaybeEmbΠl : ∀ {Γ A l} → Γ ⊩⟨ l ⟩Π A → TypeLevel
extractMaybeEmbΠl {l = l} (noemb x) = l
extractMaybeEmbΠl (emb 0<1 x) = ⁰

extractMaybeEmbΠ : ∀ {Γ A l} → ([A] : Γ ⊩⟨ l ⟩Π A) → Γ ⊩′⟨ extractMaybeEmbΠl [A] ⟩Π A
extractMaybeEmbΠ {l = l} (noemb x) = x
extractMaybeEmbΠ (emb 0<1 (noemb x)) = x

-- emb, but with a propositional equality for the target level
emb″ : ∀ {Γ A} (l : TypeLevel) → (l PE.≡ ¹) → (p : Γ ⊩⟨ ⁰ ⟩ A) → Γ ⊩⟨ l ⟩ A
emb″ .¹ PE.refl p = emb′ 0<1 p

-- A view for constructor equality of types where embeddings are ignored
data ShapeView Γ (l l′ : TypeLevel) : ∀ A B (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ B)
     → Set (lsuc (lsuc (toLevel l ⊔ toLevel l′))) where
  Uᵥ : ∀ l'A l<A ⊢ΓA l'B l<B ⊢ΓB
    → ShapeView Γ l l′ U U
      (LRPack _ _ _ (LRU ⊢ΓA l'A l<A))
      (LRPack _ _ _ (LRU ⊢ΓB l'B l<B))
  ℕᵥ : ∀ {A B} ℕA ℕB
    → ShapeView Γ l l′ A B
      (LRPack _ _ _ (LRℕ ℕA))
      (LRPack _ _ _ (LRℕ ℕB))
  ne  : ∀ {A B} neA neB
      → ShapeView Γ l l′ A B
        (LRPack _ _ _ (LRne neA))
        (LRPack _ _ _ (LRne neB))
  Πᵥ : ∀ {A B} ΠA ΠB
     → ShapeView Γ l l′ A B
       (LRPack _ _ _ (LRΠ ΠA))
       (LRPack _ _ _ (LRΠ ΠB))
  emb⁰¹ : ∀ {A B p q}
        → (l≡ : l PE.≡ ¹)
        → ShapeView Γ ⁰ l′ A B p q
        → ShapeView Γ l l′ A B (emb″ l l≡ p) q
  emb¹⁰ : ∀ {A B p q}
        → (l≡ : l′ PE.≡ ¹)
        → ShapeView Γ l ⁰ A B p q
        → ShapeView Γ l l′ A B p (emb″ l′ l≡ q)

-- Construct an shape view from an equality
goodCases : ∀ {l l′ Γ A B} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
          → Γ ⊩⟨ l ⟩ A ≡ B / [A] → ShapeView Γ l l′ A B [A] [B]
goodCases (Uᵣ′ lA l<A ⊢ΓA) (Uᵣ′ lB l<B ⊢ΓB) A≡B = Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB
goodCases (Uᵣ′ _ _ ⊢Γ) (ℕᵣ D) (U₌ PE.refl) = ⊥-elim (U≢ℕ (whnfRed* (red D) Uₙ))
goodCases (Uᵣ′ _ _ ⊢Γ) (ne′ K D neK K≡K) (U₌ PE.refl) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
goodCases (Uᵣ′ _ _ ⊢Γ) (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (U₌ PE.refl) =
  ⊥-elim (U≢Π (whnfRed* (red D) Uₙ))
goodCases (ℕᵣ D) (Uᵣ′ _ _ ⊢Γ) (ιx (ℕ₌ A≡B)) = ⊥-elim (U≢ℕ (whnfRed* A≡B Uₙ))
goodCases (ℕᵣ ℕA) (ℕᵣ ℕB) A≡B = ℕᵥ ℕA ℕB
goodCases (ℕᵣ D) (ne′ K D₁ neK K≡K) (ιx (ℕ₌ A≡B)) =
  ⊥-elim (ℕ≢ne neK (whrDet* (A≡B , ℕₙ) (red D₁ , ne neK)))
goodCases (ℕᵣ D) (Πᵣ′ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) (ιx (ℕ₌ A≡B)) =
  ⊥-elim (ℕ≢Π (whrDet* (A≡B , ℕₙ) (red D₁ , Πₙ)))
goodCases (ne′ K D neK K≡K) (Uᵣ′ _ _ ⊢Γ) (ιx (ne₌ M D′ neM K≡M)) =
  ⊥-elim (U≢ne neM (whnfRed* (red D′) Uₙ))
goodCases (ne′ K D neK K≡K) (ℕᵣ D₁) (ιx (ne₌ M D′ neM K≡M)) =
  ⊥-elim (ℕ≢ne neM (whrDet* (red D₁ , ℕₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (ne′ K′ D′ neK′ K≡K′) A≡B = ne (ne K D neK K≡K) (ne K′ D′ neK′ K≡K′)
goodCases (ne′ K D neK K≡K) (Πᵣ′ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) (ιx (ne₌ M D′ neM K≡M)) =
  ⊥-elim (Π≢ne neM (whrDet* (red D₁ , Πₙ) (red D′ , ne neM)))
goodCases (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Uᵣ′ _ _ ⊢Γ)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (U≢Π (whnfRed* D′ Uₙ))
goodCases (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ D₁)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (ℕ≢Π (whrDet* (red D₁ , ℕₙ) (D′ , Πₙ)))
goodCases (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (Π≢ne neK (whrDet* (D′ , Πₙ) (red D₁ , ne neK)))
goodCases (LRPack _ _ _ (LRΠ ΠA)) (LRPack _ _ _ (LRΠ ΠB)) A≡B = Πᵥ ΠA ΠB
goodCases {l} [A] (emb′ 0<1 x) A≡B =
  emb¹⁰ PE.refl (goodCases {l} {⁰} [A] x A≡B)
goodCases {l′ = l} (emb′ 0<1 x) [B] (ιx A≡B) =
  emb⁰¹ PE.refl (goodCases {⁰} {l} x [B] A≡B)

-- Construct an shape view between two derivations of the same type
goodCasesRefl : ∀ {l l′ Γ A} ([A] : Γ ⊩⟨ l ⟩ A) ([A′] : Γ ⊩⟨ l′ ⟩ A)
              → ShapeView Γ l l′ A A [A] [A′]
goodCasesRefl [A] [A′] = goodCases [A] [A′] (reflEq [A])

-- A view for constructor equality between three types
data ShapeView₃ Γ (l l′ l″ : TypeLevel) : ∀ A B C
                 (p : Γ ⊩⟨ l  ⟩ A)
                 (q : Γ ⊩⟨ l′ ⟩ B)
                 (r : Γ ⊩⟨ l″ ⟩ C)
                 → Set (lsuc (lsuc (toLevel l ⊔ toLevel l′ ⊔ toLevel l″))) where
  Uᵥ : ∀ lA l<A ⊢ΓA lB l<B ⊢ΓB lC l<C ⊢ΓC
    → ShapeView₃ Γ l l′ l″ U U U
      (LRPack _ _ _ (LRU ⊢ΓA lA l<A))
      (LRPack _ _ _ (LRU ⊢ΓB lB l<B))
      (LRPack _ _ _ (LRU ⊢ΓC lC l<C))
  ℕᵥ : ∀ {A B C} ℕA ℕB ℕC
    → ShapeView₃ Γ l l′ l″ A B C
      (LRPack _ _ _ (LRℕ ℕA))
      (LRPack _ _ _ (LRℕ ℕB))
      (LRPack _ _ _ (LRℕ ℕC))
  ne  : ∀ {A B C} neA neB neC
      → ShapeView₃ Γ l l′ l″ A B C
        (LRPack _ _ _ (LRne neA))
        (LRPack _ _ _ (LRne neB))
        (LRPack _ _ _ (LRne neC))
  Πᵥ : ∀ {A B C} ΠA ΠB ΠC
     → ShapeView₃ Γ l l′ l″ A B C
       (LRPack _ _ _ (LRΠ ΠA))
       (LRPack _ _ _ (LRΠ ΠB))
       (LRPack _ _ _ (LRΠ ΠC))
  emb⁰¹¹ : ∀ {A B C p q r}
        → (l≡ : l PE.≡ ¹)
        → ShapeView₃ Γ ⁰ l′ l″ A B C p q r
        → ShapeView₃ Γ l l′ l″ A B C (emb″ l l≡ p) q r
  emb¹⁰¹ : ∀ {A B C p q r}
        → (l≡ : l′ PE.≡ ¹)
        → ShapeView₃ Γ l ⁰ l″ A B C p q r
        → ShapeView₃ Γ l l′ l″ A B C p (emb″ l′ l≡ q) r
  emb¹¹⁰ : ∀ {A B C p q r}
        → (l≡ : l″ PE.≡ ¹)
        → ShapeView₃ Γ l l′ ⁰ A B C p q r
        → ShapeView₃ Γ l l′ l″ A B C p q (emb″ l″ l≡ r)

-- Combines two two-way views into a three-way view
combine : ∀ {Γ l l′ l″ l‴ A B C [A] [B] [B]′ [C]}
        → ShapeView Γ l l′ A B [A] [B]
        → ShapeView Γ l″ l‴ B C [B]′ [C]
        → ShapeView₃ Γ l l′ l‴ A B C [A] [B] [C]
combine (Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB) (Uᵥ _ _ _ lC l<C ⊢ΓC) = Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB lC l<C ⊢ΓC
combine (Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB) (ℕᵥ ℕA ℕB) = ⊥-elim (U≢ℕ (whnfRed* (red ℕA) Uₙ))
combine (Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
combine (Uᵥ lA l<A ⊢ΓA lB l<B ⊢ΓB) (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
  ⊥-elim (U≢Π (whnfRed* (red D) Uₙ))
combine (ℕᵥ ℕA ℕB) (Uᵥ lB l<B ⊢ΓB lC l<C ⊢ΓC) = ⊥-elim (U≢ℕ (whnfRed* (red ℕB) Uₙ))
combine (ℕᵥ ℕA₁ ℕB₁) (ℕᵥ ℕA ℕB) = ℕᵥ ℕA₁ ℕB₁ ℕB
combine (ℕᵥ ℕA ℕB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕB , ℕₙ) (red D , ne neK)))
combine (ℕᵥ ℕA ℕB) (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
  ⊥-elim (ℕ≢Π (whrDet* (red ℕB , ℕₙ) (red D , Πₙ)))
combine (ne neA (ne K D neK K≡K)) (Uᵥ lB l<B ⊢ΓB lC l<C ⊢ΓC) =
  ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
combine (ne neA (ne K D neK K≡K)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕA , ℕₙ) (red D , ne neK)))
combine (ne neA₁ neB₁) (ne neA neB) = ne neA₁ neB₁ neB
combine (ne neA (ne K D₁ neK K≡K)) (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
  ⊥-elim (Π≢ne neK (whrDet* (red D , Πₙ) (red D₁ , ne neK)))
combine (Πᵥ ΠA (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Uᵥ lB l<B ⊢ΓB lC l<C ⊢ΓC) =
  ⊥-elim (U≢Π (whnfRed* (red D) Uₙ))
combine (Πᵥ ΠA (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢Π (whrDet* (red ℕA , ℕₙ) (red D , Πₙ)))
combine (Πᵥ ΠA (Πᵣ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext)) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (Π≢ne neK (whrDet* (red D₁ , Πₙ) (red D , ne neK)))
combine (Πᵥ ΠA₁ ΠB₁) (Πᵥ ΠA ΠB) = Πᵥ ΠA₁ ΠB₁ ΠB
combine (emb⁰¹ l≡ [AB]) [BC] = emb⁰¹¹ l≡ (combine [AB] [BC])
combine (emb¹⁰ l≡ [AB]) [BC] = emb¹⁰¹ l≡ (combine [AB] [BC])
combine [AB] (emb⁰¹ l≡ [BC]) = combine [AB] [BC]
combine [AB] (emb¹⁰ l≡ [BC]) = emb¹¹⁰ l≡ (combine [AB] [BC])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module IllTyped where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  false : Bool
  true  : Bool

F : Nat -> Set
F  zero	  = Nat
F (suc x) = Bool

postulate
  D : (x:Nat)(y:F x) -> Set
  T : Nat -> Set

  f : {x:Nat -> Nat}{y:F (x zero)} ->
      (T (x zero) -> T (suc zero)) ->
      (D zero zero -> D (x zero) y) ->
      Nat

test = f {?} (\x -> x) (\x -> x)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- 1 dimensional pretty printing of rose trees
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Text.Tree.Linear where

open import Level using (Level)
open import Size
open import Data.Bool.Base using (Bool; true; false; if_then_else_; _∧_)
open import Data.DifferenceList as DList renaming (DiffList to DList) using ()
open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_)
open import Data.Nat.Base using (ℕ; _∸_)
open import Data.Product using (_×_; _,_)
open import Data.String.Base
open import Data.Tree.Rose using (Rose; node)
open import Function.Base using (flip)

private
  variable
    a : Level
    A : Set a
    i : Size

display : Rose (List String) i → List String
display t = DList.toList (go (([] , t) ∷ [])) where

  padding : Bool → List Bool → String → String
  padding dir? []       str = str
  padding dir? (b ∷ bs) str =
    (if dir? ∧ List.null bs
     then if b then " ├ " else " └ "
     else if b then " │ "  else "   ")
    ++ padding dir? bs str

  nodePrefixes : List A → List Bool
  nodePrefixes as = true ∷ List.replicate (List.length as ∸ 1) false

  childrenPrefixes : List A → List Bool
  childrenPrefixes as = List.replicate (List.length as ∸ 1) true ∷ʳ false

  go : List (List Bool × Rose (List String) i) → DList String
  go []                       = DList.[]
  go ((bs , node a ts₁) ∷ ts) =
    let bs′ = List.reverse bs in
    DList.fromList (List.zipWith (flip padding bs′) (nodePrefixes a) a)
    DList.++ go (List.zip (List.map (_∷ bs) (childrenPrefixes ts₁)) ts₁)
    DList.++ go ts


text:
{-# OPTIONS --type-in-type #-}

Ty% : Set
Ty% =
   (Ty%         : Set)
   (nat top bot  : Ty%)
   (arr prod sum : Ty% → Ty% → Ty%)
 → Ty%

nat% : Ty%; nat% = λ _ nat% _ _ _ _ _ → nat%
top% : Ty%; top% = λ _ _ top% _ _ _ _ → top%
bot% : Ty%; bot% = λ _ _ _ bot% _ _ _ → bot%

arr% : Ty% → Ty% → Ty%; arr%
 = λ A B Ty% nat% top% bot% arr% prod sum →
     arr% (A Ty% nat% top% bot% arr% prod sum) (B Ty% nat% top% bot% arr% prod sum)

prod% : Ty% → Ty% → Ty%; prod%
 = λ A B Ty% nat% top% bot% arr% prod% sum →
     prod% (A Ty% nat% top% bot% arr% prod% sum) (B Ty% nat% top% bot% arr% prod% sum)

sum% : Ty% → Ty% → Ty%; sum%
 = λ A B Ty% nat% top% bot% arr% prod% sum% →
     sum% (A Ty% nat% top% bot% arr% prod% sum%) (B Ty% nat% top% bot% arr% prod% sum%)

Con% : Set; Con%
 = (Con% : Set)
   (nil  : Con%)
   (snoc : Con% → Ty% → Con%)
 → Con%

nil% : Con%; nil%
 = λ Con% nil% snoc → nil%

snoc% : Con% → Ty% → Con%; snoc%
 = λ Γ A Con% nil% snoc% → snoc% (Γ Con% nil% snoc%) A

Var% : Con% → Ty% → Set; Var%
 = λ Γ A →
   (Var% : Con% → Ty% → Set)
   (vz  : ∀ Γ A → Var% (snoc% Γ A) A)
   (vs  : ∀ Γ B A → Var% Γ A → Var% (snoc% Γ B) A)
 → Var% Γ A

vz% : ∀{Γ A} → Var% (snoc% Γ A) A; vz%
 = λ Var% vz% vs → vz% _ _

vs% : ∀{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A; vs%
 = λ x Var% vz% vs% → vs% _ _ _ (x Var% vz% vs%)

Tm% : Con% → Ty% → Set; Tm%
 = λ Γ A →
   (Tm%  : Con% → Ty% → Set)
   (var   : ∀ Γ A      → Var% Γ A → Tm% Γ A)
   (lam   : ∀ Γ A B    → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))
   (app   : ∀ Γ A B    → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)
   (tt    : ∀ Γ        → Tm% Γ top%)
   (pair  : ∀ Γ A B    → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B))
   (fst   : ∀ Γ A B    → Tm% Γ (prod% A B) → Tm% Γ A)
   (snd   : ∀ Γ A B    → Tm% Γ (prod% A B) → Tm% Γ B)
   (left  : ∀ Γ A B    → Tm% Γ A → Tm% Γ (sum% A B))
   (right : ∀ Γ A B    → Tm% Γ B → Tm% Γ (sum% A B))
   (case  : ∀ Γ A B C  → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C)
   (zero  : ∀ Γ        → Tm% Γ nat%)
   (suc   : ∀ Γ        → Tm% Γ nat% → Tm% Γ nat%)
   (rec   : ∀ Γ A      → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A)
 → Tm% Γ A

var% : ∀{Γ A} → Var% Γ A → Tm% Γ A; var%
 = λ x Tm% var% lam app tt pair fst snd left right case zero suc rec →
     var% _ _ x

lam% : ∀{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B); lam%
 = λ t Tm% var% lam% app tt pair fst snd left right case zero suc rec →
     lam% _ _ _ (t Tm% var% lam% app tt pair fst snd left right case zero suc rec)

app% : ∀{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B; app%
 = λ t u Tm% var% lam% app% tt pair fst snd left right case zero suc rec →
     app% _ _ _ (t Tm% var% lam% app% tt pair fst snd left right case zero suc rec)
         (u Tm% var% lam% app% tt pair fst snd left right case zero suc rec)

tt% : ∀{Γ} → Tm% Γ top%; tt%
 = λ Tm% var% lam% app% tt% pair fst snd left right case zero suc rec → tt% _

pair% : ∀{Γ A B} → Tm% Γ A → Tm% Γ B → Tm% Γ (prod% A B); pair%
 = λ t u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec →
     pair% _ _ _ (t Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)
          (u Tm% var% lam% app% tt% pair% fst snd left right case zero suc rec)

fst% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ A; fst%
 = λ t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec →
     fst% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd left right case zero suc rec)

snd% : ∀{Γ A B} → Tm% Γ (prod% A B) → Tm% Γ B; snd%
 = λ t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec →
     snd% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left right case zero suc rec)

left% : ∀{Γ A B} → Tm% Γ A → Tm% Γ (sum% A B); left%
 = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec →
     left% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right case zero suc rec)

right% : ∀{Γ A B} → Tm% Γ B → Tm% Γ (sum% A B); right%
 = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec →
     right% _ _ _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case zero suc rec)

case% : ∀{Γ A B C} → Tm% Γ (sum% A B) → Tm% Γ (arr% A C) → Tm% Γ (arr% B C) → Tm% Γ C; case%
 = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec →
     case% _ _ _ _
           (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)
           (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)
           (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero suc rec)

zero%  : ∀{Γ} → Tm% Γ nat%; zero%
 = λ Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc rec → zero% _

suc% : ∀{Γ} → Tm% Γ nat% → Tm% Γ nat%; suc%
 = λ t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec →
   suc% _ (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec)

rec% : ∀{Γ A} → Tm% Γ nat% → Tm% Γ (arr% nat% (arr% A A)) → Tm% Γ A → Tm% Γ A; rec%
 = λ t u v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec% →
     rec% _ _
          (t Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)
          (u Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)
          (v Tm% var% lam% app% tt% pair% fst% snd% left% right% case% zero% suc% rec%)

v0% : ∀{Γ A} → Tm% (snoc% Γ A) A; v0%
 = var% vz%

v1% : ∀{Γ A B} → Tm% (snoc% (snoc% Γ A) B) A; v1%
 = var% (vs% vz%)

v2% : ∀{Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A; v2%
 = var% (vs% (vs% vz%))

v3% : ∀{Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A; v3%
 = var% (vs% (vs% (vs% vz%)))

tbool% : Ty%; tbool%
 = sum% top% top%

true% : ∀{Γ} → Tm% Γ tbool%; true%
 = left% tt%

tfalse% : ∀{Γ} → Tm% Γ tbool%; tfalse%
 = right% tt%

ifthenelse% : ∀{Γ A} → Tm% Γ (arr% tbool% (arr% A (arr% A A))); ifthenelse%
 = lam% (lam% (lam% (case% v2% (lam% v2%) (lam% v1%))))

times4% : ∀{Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A)); times4%
  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))

add% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); add%
 = lam% (rec% v0%
       (lam% (lam% (lam% (suc% (app% v1% v0%)))))
       (lam% v0%))

mul% : ∀{Γ} → Tm% Γ (arr% nat% (arr% nat% nat%)); mul%
 = lam% (rec% v0%
       (lam% (lam% (lam% (app% (app% add% (app% v1% v0%)) v0%))))
       (lam% zero%))

fact% : ∀{Γ} → Tm% Γ (arr% nat% nat%); fact%
 = lam% (rec% v0% (lam% (lam% (app% (app% mul% (suc% v1%)) v0%)))
        (suc% zero%))

max_stars_repo_name: int-index/smalltt

max_issues_repo_name: int-index/smalltt

max_forks_repo_name: int-index/smalltt


text:
-- Andreas, 2012-09-07
module DataParameterPolarity where

data Bool : Set where
  true false : Bool

data ⊥ : Set where
record ⊤ : Set where

-- True uses its first argument.
True : Bool → Set
True true  = ⊤
True false = ⊥

-- Hence, D also uses its first argument.
-- A buggy polarity analysis may consider D as constant.
data D (b : Bool) : Set where
  c : True b → D b

d : {b : Bool} → D b → True b
d (c x) = x

-- This cast is fatal, possible if D is considered constant.
cast : (a b : Bool) → D a → D b
cast a b x = x

bot : ⊥
bot = d (cast true false (c _))


text:
{-

This file contains:

- Id, refl and J (with definitional computation rule)

- Basic theory about Id, proved using J

- Lemmas for going back and forth between Path and Id

- Function extensionality for Id

- fiber, isContr, equiv all defined using Id

- The univalence axiom expressed using only Id ([EquivContr])

- Propositional truncation and its elimination principle

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Id where

open import Cubical.Foundations.Prelude public
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ ; isPropIsContr)
  renaming ( refl      to reflPath
           ; transport to transportPath
           ; J         to JPath
           ; JRefl     to JPathRefl
           ; sym       to symPath
           ; _∙_       to compPath
           ; cong      to congPath
           ; funExt    to funExtPath
           ; isContr   to isContrPath
           ; isProp    to isPropPath
           ; isSet     to isSetPath
           ; fst       to pr₁ -- as in the HoTT book
           ; snd       to pr₂
           )
open import Cubical.Core.Glue
  renaming ( isEquiv      to isEquivPath
           ; _≃_         to EquivPath
           ; equivFun     to equivFunPath )

open import Cubical.Foundations.Equiv
  renaming ( fiber        to fiberPath
           ; equivIsEquiv to equivIsEquivPath
           ; equivCtr     to equivCtrPath )
  hiding   ( isPropIsEquiv )

open import Cubical.Foundations.Univalence
  renaming ( EquivContr   to EquivContrPath )
open import Cubical.HITs.PropositionalTruncation public
  renaming ( squash to squashPath
           ; recPropTrunc to recPropTruncPath
           ; elimPropTrunc to elimPropTruncPath )
open import Cubical.Core.Id public

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Version of the constructor for Id where the y is also
-- explicit. This is sometimes useful when it is needed for
-- typechecking (see JId below).
conId : ∀ {x : A} φ (y : A [ φ ↦ (λ _ → x) ])
          (w : (Path _ x (outS y)) [ φ ↦ (λ { (φ = i1) → λ _ → x}) ]) →
          x ≡ outS y
conId φ _ w = ⟨ φ , outS w ⟩

-- Reflexivity
refl : ∀ {x : A} → x ≡ x
refl {x = x} = ⟨ i1 , (λ _ → x) ⟩

-- Definition of J for Id
module _ {x : A} (P : ∀ (y : A) → Id x y → Type ℓ') (d : P x refl) where
  J : ∀ {y : A} (w : x ≡ y) → P y w
  J {y = y} = elimId P (λ φ y w → comp (λ i → P _ (conId (φ ∨ ~ i) (inS (outS w i))
                                                                   (inS (λ j → outS w (i ∧ j)))))
                                       (λ i → λ { (φ = i1) → d}) d) {y = y}

  -- Check that J of refl is the identity function
  Jdefeq : Path _ (J refl) d
  Jdefeq _ = d

-- Basic theory about Id, proved using J
transport : ∀ (B : A → Type ℓ') {x y : A}
           → x ≡ y → B x → B y
transport B {x} p b = J (λ y p → B y) b p

_⁻¹ : {x y : A} → x ≡ y → y ≡ x
_⁻¹ {x = x} p = J (λ z _ → z ≡ x) refl p

ap : ∀ {B : Type ℓ'} (f : A → B) → ∀ {x y : A} → x ≡ y → f x ≡ f y
ap f {x} = J (λ z _ → f x ≡ f z) refl

_∙_ : ∀ {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {x = x} p = J (λ y _ → x ≡ y) p

infix  4 _∙_
infix  3 _∎
infixr 2 _≡⟨_⟩_

_≡⟨_⟩_ : (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ p ⟩ q = p ∙ q

_∎ : (x : A) → x ≡ x
_ ∎ = refl

-- Convert between Path and Id
pathToId : ∀ {x y : A} → Path _ x y → Id x y
pathToId {x = x} = JPath (λ y _ → Id x y) refl

pathToIdRefl : ∀ {x : A} → Path _ (pathToId (λ _ → x)) refl
pathToIdRefl {x = x} = JPathRefl (λ y _ → Id x y) refl

idToPath : ∀ {x y : A} → Id x y → Path _ x y
idToPath {x = x} = J (λ y _ → Path _ x y) (λ _ → x)

idToPathRefl : ∀ {x : A} → Path _ (idToPath {x = x} refl) reflPath
idToPathRefl {x = x} _ _ = x

pathToIdToPath : ∀ {x y : A} → (p : Path _ x y) → Path _ (idToPath (pathToId p)) p
pathToIdToPath {x = x} = JPath (λ y p → Path _ (idToPath (pathToId p)) p)
                               (λ i → idToPath (pathToIdRefl i))

idToPathToId : ∀ {x y : A} → (p : Id x y) → Path _ (pathToId (idToPath p)) p
idToPathToId {x = x} = J (λ b p → Path _ (pathToId (idToPath p)) p) pathToIdRefl

-- We get function extensionality by going back and forth between Path and Id
funExt : ∀ {B : A → Type ℓ'} {f g : (x : A) → B x} →
         ((x : A) → f x ≡ g x) → f ≡ g
funExt p = pathToId (λ i x → idToPath (p x) i)

-- Equivalences expressed using Id

fiber : ∀ {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

isContr : Type ℓ → Type ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

isSet : Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

record isEquiv {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type (ℓ-max ℓ ℓ') where
  field
    equiv-proof : (y : B) → isContr (fiber f y)

open isEquiv public

infix 4 _≃_

_≃_ : ∀ (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
A ≃ B = Σ[ f ∈ (A → B) ] (isEquiv f)

equivFun : ∀ {B : Type ℓ'} → A ≃ B → A → B
equivFun e = pr₁ e

equivIsEquiv : ∀ {B : Type ℓ'} (e : A ≃ B) → isEquiv (equivFun e)
equivIsEquiv e = pr₂ e

equivCtr : ∀ {B : Type ℓ'} (e : A ≃ B) (y : B) → fiber (equivFun e) y
equivCtr e y = e .pr₂ .equiv-proof y .pr₁

-- Functions for going between the various definitions. This could
-- also be achieved by making lines in the universe and transporting
-- back and forth along them.

fiberPathToFiber : ∀ {B : Type ℓ'} {f : A → B} {y : B} →
  fiberPath f y → fiber f y
fiberPathToFiber (x , p) = (x , pathToId p)

fiberToFiberPath : ∀ {B : Type ℓ'} {f : A → B} {y : B} →
  fiber f y → fiberPath f y
fiberToFiberPath (x , p) = (x , idToPath p)

fiberToFiber : ∀ {B : Type ℓ'} {f : A → B} {y : B}
  (p : fiber f y) → Path _ (fiberPathToFiber (fiberToFiberPath p)) p
fiberToFiber (x , p) = λ i → x , idToPathToId p i

fiberPathToFiberPath : ∀ {B : Type ℓ'} {f : A → B} {y : B}
  (p : fiberPath f y) → Path _ (fiberToFiberPath (fiberPathToFiber p)) p
fiberPathToFiberPath (x , p) = λ i → x , pathToIdToPath p i

isContrPathToIsContr : isContrPath A → isContr A
isContrPathToIsContr (ctr , p) = (ctr , λ y → pathToId (p y))

isContrToIsContrPath : isContr A → isContrPath A
isContrToIsContrPath (ctr , p) = (ctr , λ y → idToPath (p y))

isPropPathToIsProp : isPropPath A → isProp A
isPropPathToIsProp H x y = pathToId (H x y)

isPropToIsPropPath : isProp A → isPropPath A
isPropToIsPropPath H x y i = idToPath (H x y) i

-- Specialized helper lemmas for going back and forth between
-- isContrPath and isContr:

helper1 : ∀ {A B : Type ℓ} (f : A → B) (g : B → A)
            (h : ∀ y → Path _ (f (g y)) y) → isContrPath A → isContr B
helper1 f g h (x , p) =
  (f x , λ y → pathToId (λ i → hcomp (λ j → λ { (i = i0) → f x
                                              ; (i = i1) → h y j })
                                     (f (p (g y) i))))

helper2 : ∀ {A B : Type ℓ} (f : A → B) (g : B → A)
            (h : ∀ y → Path _ (g (f y)) y) → isContr B → isContrPath A
helper2 {A = A} f g h (x , p) = (g x , λ y → idToPath (rem y))
  where
  rem : ∀ (y : A) → g x ≡ y
  rem y =
    g x     ≡⟨ ap g (p (f y)) ⟩
    g (f y) ≡⟨ pathToId (h y) ⟩
    y       ∎

-- This proof is essentially the one for proving that isContr with
-- Path is a proposition, but as we are working with Id we have to
-- insert a lof of conversion functions. It is still nice that is
-- works like this though.
isPropIsContr : ∀ (p1 p2 : isContr A) → Path (isContr A) p1 p2
isPropIsContr (a0 , p0) (a1 , p1) j =
  ( idToPath (p0 a1) j ,
    hcomp (λ i → λ { (j = i0) →  λ x → idToPathToId (p0 x) i
                   ; (j = i1) →  λ x → idToPathToId (p1 x) i })
          (λ x → pathToId (λ i → hcomp (λ k → λ { (i = i0) → idToPath (p0 a1) j
                                                ; (i = i1) → idToPath (p0 x) (j ∨ k)
                                                ; (j = i0) → idToPath (p0 x) (i ∧ k)
                                                ; (j = i1) → idToPath (p1 x) i })
                                       (idToPath (p0 (idToPath (p1 x) i)) j))))

-- We now prove that isEquiv is a proposition
isPropIsEquiv : ∀ {A : Type ℓ} {B : Type ℓ} → {f : A → B} → (h1 h2 : isEquiv f) → Path _ h1 h2
equiv-proof (isPropIsEquiv {f = f} h1 h2 i) y =
  isPropIsContr {A = fiber f y} (h1 .equiv-proof y) (h2 .equiv-proof y) i

-- Go from a Path equivalence to an Id equivalence
equivPathToEquiv : ∀ {A : Type ℓ} {B : Type ℓ'} → EquivPath A B → A ≃ B
equivPathToEquiv (f , p) =
  (f , λ { .equiv-proof y → helper1 fiberPathToFiber fiberToFiberPath fiberToFiber (p .equiv-proof y) })

-- Go from an Id equivalence to a Path equivalence
equivToEquivPath : ∀ {A : Type ℓ} {B : Type ℓ'} → A ≃ B → EquivPath A B
equivToEquivPath (f , p) =
  (f , λ { .equiv-proof y → helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y) })

equivToEquiv : ∀ {A : Type ℓ} {B : Type ℓ} → (p : A ≃ B) → Path _ (equivPathToEquiv (equivToEquivPath p)) p
equivToEquiv (f , p) i =
  (f , isPropIsEquiv (λ { .equiv-proof y → helper1 fiberPathToFiber fiberToFiberPath fiberToFiber
                                             (helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y)) }) p i)

-- We can finally prove univalence with Id everywhere from the one for Path
EquivContr : ∀ (A : Type ℓ) → isContr (Σ[ T ∈ Type ℓ ] (T ≃ A))
EquivContr A = helper1 f1 f2 f12 (EquivContrPath A)
  where
  f1 : ∀ {ℓ} {A : Type ℓ} → Σ[ T ∈ Type ℓ ] (EquivPath T A) → Σ[ T ∈ Type ℓ ] (T ≃ A)
  f1 (x , p) = x , equivPathToEquiv p

  f2 : ∀ {ℓ} {A : Type ℓ} → Σ[ T ∈ Type ℓ ] (T ≃ A) → Σ[ T ∈ Type ℓ ] (EquivPath T A)
  f2 (x , p) = x , equivToEquivPath p

  f12 : ∀ {ℓ} {A : Type ℓ} → (y : Σ[ T ∈ Type ℓ ] (T ≃ A)) → Path _ (f1 (f2 y)) y
  f12 (x , p) = λ i → x , equivToEquiv p i

-- Propositional truncation

∥∥-isProp : ∀ (x y : ∥ A ∥) → x ≡ y
∥∥-isProp x y = pathToId (squashPath x y)

∥∥-recursion : ∀ {A : Type ℓ} {P : Type ℓ} → isProp P → (A → P) → ∥ A ∥ → P
∥∥-recursion Pprop f x = recPropTruncPath (isPropToIsPropPath Pprop) f x

∥∥-induction : ∀ {A : Type ℓ} {P : ∥ A ∥ → Type ℓ} → ((a : ∥ A ∥) → isProp (P a)) →
                ((x : A) → P ∣ x ∣) → (a : ∥ A ∥) → P a
∥∥-induction Pprop f x = elimPropTruncPath (λ a → isPropToIsPropPath (Pprop a)) f x

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Pointwise.Extensional directly.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Relation.Pointwise.Inductive where

open import Data.Vec.Relation.Binary.Pointwise.Inductive public


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Nat

test : (n : Nat) → Nat
test n with zero
... | n = {!n!}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- This file is imported by Issue1597.Main

module Issue1597 where

module A where
  module M where -- needs to be module
    postulate Nat : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- The division specification
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module LTC-PCF.Program.Division.Specification where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities

------------------------------------------------------------------------------
-- Specification: The division is total and the result is correct.
divSpec : D → D → D → Set
divSpec i j q = N q ∧ (∃[ r ] N r ∧ r < j ∧ i ≡ j * q + r)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Categories.Ran where

open import Level
open import Categories.Category
open import Categories.Functor hiding (_≡_)
open import Categories.NaturalTransformation

record Ran {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} {o₂ ℓ₂ e₂}
           {A : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} {C : Category o₂ ℓ₂ e₂}
           (F : Functor A B) (X : Functor A C) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁ ⊔ o₂ ⊔ ℓ₂ ⊔ e₂) where
  field
    R : Functor B C
    η : NaturalTransformation (R ∘ F) X

    δ : (M : Functor B C) → (α : NaturalTransformation (M ∘ F) X) → NaturalTransformation M R

    .δ-unique : {M : Functor B C} → {α : NaturalTransformation (M ∘ F) X} →
                (δ′ : NaturalTransformation M R) → α ≡ η ∘₁ (δ′ ∘ʳ F) → δ′ ≡ δ M α
    .commutes : (M : Functor B C) → (α : NaturalTransformation (M ∘ F) X) → α ≡ η ∘₁ (δ M α ∘ʳ F)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Hash
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Encode

-- This module brings in the base types used through libra
-- and those necessary for the abstract model.
module LibraBFT.Abstract.Types where

  open import LibraBFT.Base.Types public

  -- Simple way to flag meta-information without having it getting
  -- in the way.
  Meta : ∀{ℓ} → Set ℓ → Set ℓ
  Meta x = x

  -- An epoch-configuration carries only simple data about the epoch; the complicated
  -- parts will be provided by the System, defined below.
  --
  -- The reason for the separation is that we should be able to provide
  -- an EpochConfig from a single peer state.
  record EpochConfig : Set₁ where
    constructor mkEpochConfig
    field
      -- TODO-2 : This should really be a UID as Hash should not show up in the Abstract
      -- namespace.  This will require some refactoring of modules and reordering of
      -- module parameters.
      genesisUID : Hash
      epochId   : EpochId
      authorsN  : ℕ

    -- The set of members of this epoch.
    Member : Set
    Member = Fin authorsN

    -- There is a partial isomorphism between NodeIds and the
    -- authors participating in this epoch.
    field
      toNodeId  : Member → NodeId
      isMember? : NodeId → Maybe Member

      nodeid-author-id : ∀{α}     → isMember? (toNodeId α) ≡ just α
      author-nodeid-id : ∀{nid α} → isMember? nid ≡ just α
                                  → toNodeId α ≡ nid

      getPubKey : Member → PK

      PK-inj : ∀ {m1 m2} → getPubKey m1 ≡ getPubKey m2 → m1 ≡ m2

      IsQuorum : List Member → Set

      bft-assumption : ∀ {xs ys}
                     → IsQuorum xs → IsQuorum ys
                     → ∃[ α ] (α ∈ xs × α ∈ ys × Meta-Honest-PK (getPubKey α))

  open EpochConfig

  toNodeId-inj : ∀{𝓔}{x y : Member 𝓔} → toNodeId 𝓔 x ≡ toNodeId 𝓔 y → x ≡ y
  toNodeId-inj {𝓔} hyp = just-injective (trans (sym (nodeid-author-id 𝓔))
                                        (trans (cong (isMember? 𝓔) hyp)
                                               (nodeid-author-id 𝓔)))

  record EpochConfigFor (eid : ℕ) : Set₁ where
    field
     epochConfig : EpochConfig
     forEpochId  : epochId epochConfig ≡ eid

  MemberSubst : ∀ {𝓔} {𝓔'}
              → 𝓔' ≡ 𝓔
              → EpochConfig.Member 𝓔
              → EpochConfig.Member 𝓔'
  MemberSubst refl = id

  -- A member of an epoch is considered "honest" iff its public key is honest.
  Meta-Honest-Member : (𝓔 : EpochConfig) → Member 𝓔 → Set
  Meta-Honest-Member 𝓔 α = Meta-Honest-PK (getPubKey 𝓔 α)

  -- Naturally, if two witnesses that two authors belong
  -- in the epoch are the same, then the authors are also the same.
  --
  -- This proof is very Galois-like, because of the way we structured
  -- our partial isos. It's actually pretty nice! :)
  member≡⇒author≡ : ∀{α β}{𝓔 : EpochConfig}
                  → (authorα : Is-just (isMember? 𝓔 α))
                  → (authorβ : Is-just (isMember? 𝓔 β))
                  → to-witness authorα ≡ to-witness authorβ
                  → α ≡ β
  member≡⇒author≡ {α} {β} {𝓔} a b prf
    with isMember? 𝓔 α | inspect (isMember? 𝓔) α
  ...| nothing | [ _ ] = ⊥-elim (maybe-any-⊥ a)
  member≡⇒author≡ {α} {β} {𝓔} (just _) b prf
     | just ra | [ RA ]
    with isMember? 𝓔 β | inspect (isMember? 𝓔) β
  ...| nothing | [ _ ] = ⊥-elim (maybe-any-⊥ b)
  member≡⇒author≡ {α} {β} {𝓔} (just _) (just _) prf
     | just ra | [ RA ]
     | just rb | [ RB ]
     = trans (sym (author-nodeid-id 𝓔 RA))
             (trans (cong (toNodeId 𝓔) prf)
                    (author-nodeid-id 𝓔 RB))

  -- The abstract model is connected to the implementaton by means of
  -- 'VoteEvidence'. The record module will be parameterized by a
  -- v of type 'VoteEvidence 𝓔 UID'; this v will provide evidence
  -- that a given author voted for a given block (identified by the UID)
  -- on the specified round.
  --
  -- When it comes time to instantiate the v above concretely, it will
  -- be something that states that we have a signature from the specified
  -- author voting for the specified block.
  record AbsVoteData (𝓔 : EpochConfig)(UID : Set) : Set where
    constructor mkAbsVoteData
    field
      abs-vRound     : Round
      abs-vMember    : EpochConfig.Member 𝓔
      abs-vBlockUID  : UID
  open AbsVoteData public

  AbsVoteData-η : ∀ {𝓔} {UID : Set} {r1 r2 : Round} {m1 m2 : EpochConfig.Member 𝓔} {b1 b2 : UID}
                → r1 ≡ r2
                → m1 ≡ m2
                → b1 ≡ b2
                → mkAbsVoteData {𝓔} {UID} r1 m1 b1 ≡ mkAbsVoteData r2 m2 b2
  AbsVoteData-η refl refl refl = refl

  VoteEvidence : EpochConfig → Set → Set₁
  VoteEvidence 𝓔 UID = AbsVoteData 𝓔 UID → Set


text:
module Thesis.Syntax where

open import Thesis.Types public
open import Thesis.Contexts public

data Const : (τ : Type) → Set where
   unit : Const unit
   lit : ℤ → Const int
   plus : Const (int ⇒ int ⇒ int)
   minus : Const (int ⇒ int ⇒ int)
   cons : ∀ {t1 t2} → Const (t1 ⇒ t2 ⇒ pair t1 t2)
   fst : ∀ {t1 t2} → Const (pair t1 t2 ⇒ t1)
   snd : ∀ {t1 t2} → Const (pair t1 t2 ⇒ t2)
   linj : ∀ {t1 t2} → Const (t1 ⇒ sum t1 t2)
   rinj : ∀ {t1 t2} → Const (t2 ⇒ sum t1 t2)
   match : ∀ {t1 t2 t3} → Const (sum t1 t2 ⇒ (t1 ⇒ t3) ⇒ (t2 ⇒ t3) ⇒ t3)

data Term (Γ : Context) :
  (τ : Type) → Set where
  -- constants aka. primitives
  const : ∀ {τ} →
    (c : Const τ) →
    Term Γ τ
  var : ∀ {τ} →
    (x : Var Γ τ) →
    Term Γ τ
  app : ∀ {σ τ}
    (s : Term Γ (σ ⇒ τ)) →
    (t : Term Γ σ) →
    Term Γ τ
  -- we use de Bruijn indices, so we don't need binding occurrences.
  abs : ∀ {σ τ}
    (t : Term (σ • Γ) τ) →
    Term Γ (σ ⇒ τ)

-- Weakening

weaken : ∀ {Γ₁ Γ₂ τ} →
  (Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
  Term Γ₁ τ →
  Term Γ₂ τ
weaken Γ₁≼Γ₂ (const c) = const c
weaken Γ₁≼Γ₂ (var x) = var (weaken-var Γ₁≼Γ₂ x)
weaken Γ₁≼Γ₂ (app s t) = app (weaken Γ₁≼Γ₂ s) (weaken Γ₁≼Γ₂ t)
weaken Γ₁≼Γ₂ (abs {σ} t) = abs (weaken (keep σ • Γ₁≼Γ₂) t)

-- Shorthands for nested applications
app₂ : ∀ {Γ α β γ} →
  Term Γ (α ⇒ β ⇒ γ) →
  Term Γ α → Term Γ β → Term Γ γ
app₂ f x = app (app f x)

app₃ : ∀ {Γ α β γ δ} →
  Term Γ (α ⇒ β ⇒ γ ⇒ δ) →
  Term Γ α → Term Γ β → Term Γ γ → Term Γ δ
app₃ f x = app₂ (app f x)

app₄ : ∀ {Γ α β γ δ ε} →
  Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε) →
  Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
  Term Γ ε
app₄ f x = app₃ (app f x)

app₅ : ∀ {Γ α β γ δ ε ζ} →
  Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ) →
  Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
  Term Γ ε → Term Γ ζ
app₅ f x = app₄ (app f x)

app₆ : ∀ {Γ α β γ δ ε ζ η} →
  Term Γ (α ⇒ β ⇒ γ ⇒ δ ⇒ ε ⇒ ζ ⇒ η) →
  Term Γ α → Term Γ β → Term Γ γ → Term Γ δ →
  Term Γ ε → Term Γ ζ → Term Γ η
app₆ f x = app₅ (app f x)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
open import Common.Reflection

macro
  round-trip : Term → Tactic
  round-trip v hole = unify v hole

module M (A : Set) where
  data D : Set where

  test : Set
  test = round-trip D

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module MissingWithClauses where

data D : Set where
  c : D

f : D -> D
f c with c


text:
module PiInSet where

Rel : Set -> Set1
Rel A = A -> A -> Set

Reflexive : {A : Set} -> Rel A -> Set
Reflexive {A} _R_ = forall x -> x R x

Symmetric : {A : Set} -> Rel A -> Set
Symmetric {A} _R_ = forall x y -> x R y -> y R x

data True : Set where
  tt : True

data False : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_==_ : Rel Nat
zero  == zero  = True
zero  == suc _ = False
suc _ == zero  = False
suc n == suc m = n == m

refl== : Reflexive _==_
refl==  zero   = tt
refl== (suc n) = refl== n

sym== : Symmetric _==_
sym==  zero    zero   tt = tt
sym==  zero   (suc _) ()
sym== (suc _)  zero   ()
sym== (suc n) (suc m) n==m = sym== n m n==m