text:
module OTT.Prelude where

open import Level
  renaming (Level to MetaLevel; zero to lzeroₘ; suc to lsucₘ; _⊔_ to _⊔ₘ_) using () public
open import Function public
open import Relation.Binary.PropositionalEquality as P using (_≡_)
  renaming (refl to prefl; trans to ptrans; subst to psubst; cong to pcong; cong₂ to pcong₂) public
open import Data.Empty public
open import Data.Nat.Base hiding (_⊔_; _≟_; erase) public
open import Data.Maybe.Base using (Maybe; nothing; just) public
open import Data.Product hiding (,_) renaming (map to pmap) public

open import OTT.Lib.Heteroindexed public
open import OTT.Lib.Decidable public

open import Relation.Nullary
open import Relation.Binary

infix 4  ,_

pattern ,_ y = _ , y

record ⊤ {α} : Set α where
  constructor tt

⊤₀ : Set
⊤₀ = ⊤

instance
  iprefl : ∀ {α} {A : Set α} {x : A} -> x ≡ x
  iprefl = prefl

  ,-inst : ∀ {α β} {A : Set α} {B : A -> Set β} {{x : A}} {{y : B x}} -> Σ A B
  ,-inst {{x}} {{y}} = x , y

pright : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> x ≡ z -> y ≡ z
pright prefl prefl = prefl

hpcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
        -> (f : ∀ x -> B x -> C) -> (q : x₁ ≡ x₂) -> psubst B q y₁ ≡ y₂ -> f x₁ y₁ ≡ f x₂ y₂
hpcong₂ f prefl prefl = prefl

record Apply {α β} {A : Set α} (B : A -> Set β) x : Set β where
  constructor tag
  field detag : B x
open Apply public

tag-inj : ∀ {α β} {A : Set α} {B : A -> Set β} {x} {y₁ y₂ : B x}
        -> tag {B = B} y₁ ≡ tag y₂ -> y₁ ≡ y₂
tag-inj prefl = prefl

data Match {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : Set (ι ⊔ₘ α) where
  matched : ∀ {j} -> (x′ : A j) -> [ A ] x ≅ x′ -> Match A x

match : ∀ {ι α} {I : Set ι} {i} -> (A : I -> Set α) -> (x : A i) -> Match A x
match A x = matched x irefl

data IMatch {ι α β} {I : Set ι} {i} (A : I -> Set α) {x : A i}
            (B : ∀ {i} -> A i -> Set β) (y : B x) : Set (ι ⊔ₘ α ⊔ₘ β) where
  imatched : ∀ {i} {x : A i} -> (y′ : B x) -> [ A ][ B ] y ≅ y′ -> IMatch A B y

imatch : ∀ {ι α β} {I : Set ι} {i}
       -> (A : I -> Set α) {x : A i} -> (B : ∀ {i} -> A i -> Set β) -> (y : B x) -> IMatch A B y
imatch A B y = imatched y iirefl

module _ {α} {A : Set α} where
  open import Relation.Nullary.Decidable
  open import Data.Maybe

  toPropEq : {a b : Maybe A} -> a ≡ b -> Eq _≡_ a b
  toPropEq {a = nothing} prefl = nothing
  toPropEq {a = just _ } prefl = just prefl

  fromPropEq : {a b : Maybe A} -> Eq _≡_ a b -> a ≡ b
  fromPropEq (just q) = pcong just q
  fromPropEq  nothing = prefl

  fromDecPropEq : {a b : Maybe A} -> Dec (Eq _≡_ a b) -> Dec (a ≡ b)
  fromDecPropEq = map′ fromPropEq toPropEq where

  decideMaybe : Decidable (_≡_ {A = A}) -> Decidable (_≡_ {A = Maybe A})
  decideMaybe D a b = fromDecPropEq (a ≟ b) where
    open DecSetoid (decSetoid (P.decSetoid D))

Enum : ℕ -> Set
Enum  0      = ⊥
Enum  1      = ⊤
Enum (suc n) = Maybe (Enum n)

decEnum : ∀ n -> Decidable (_≡_ {A = Enum n})
decEnum  0            () ()
decEnum  1            tt tt = yes prefl
decEnum (suc (suc n)) e₁ e₂ = decideMaybe (decEnum (suc n)) e₁ e₂

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


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

open import Algebra.Structures.Bundles.Field
import Algebra.Linear.Structures.Bundles.FiniteDimensional as FDB

module Algebra.Linear.Space.FiniteDimensional.Hom
       {k ℓᵏ} (K : Field k ℓᵏ)
       {p a₁ ℓ₁} (V₁-space : FDB.FiniteDimensional K a₁ ℓ₁ p)
       {n a₂ ℓ₂} (V₂-space : FDB.FiniteDimensional K a₂ ℓ₂ n)
       where

open import Algebra.Linear.Structures.VectorSpace K
open import Algebra.Linear.Structures.Bundles as VS
open import Algebra.Linear.Structures.FiniteDimensional K

open import Algebra.Linear.Morphism.Bundles K

open VectorSpaceField

open FDB.FiniteDimensional V₁-space
  using ()
  renaming
  ( Carrier       to V₁
  ; _≈_           to _≈₁_
  ; isEquivalence to ≈₁-isEquiv
  ; refl          to ≈₁-refl
  ; sym           to ≈₁-sym
  ; trans         to ≈₁-trans
  ; _+_           to _+₁_
  ; _∙_           to _∙₁_
  ; -_            to -₁_
  ; 0#            to 0₁
  ; +-identityˡ    to +₁-identityˡ
  ; +-identityʳ    to +₁-identityʳ
  ; +-identity    to +₁-identity
  ; +-cong        to +₁-cong
  ; +-assoc       to +₁-assoc
  ; +-comm        to +₁-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₁-compat
  ; ∙-+-distrib   to ∙₁-+₁-distrib
  ; ∙-+ᵏ-distrib  to ∙₁-+ᵏ-distrib
  ; ∙-cong        to ∙₁-cong
  ; ∙-identity    to ∙₁-identity
  ; ∙-absorbˡ      to ∙₁-absorbˡ
  ; ∙-absorbʳ      to ∙₁-absorbʳ
  ; -‿cong        to -₁‿cong
  ; -‿inverseˡ    to -₁‿inverseˡ
  ; -‿inverseʳ    to -₁‿inverseʳ
  ; vectorSpace   to vectorSpace₁
  ; embed         to embed₁
  )

open FDB.FiniteDimensional V₂-space
  using ()
  renaming
  ( Carrier       to V₂
  ; _≈_           to _≈₂_
  ; isEquivalence to ≈₂-isEquiv
  ; refl          to ≈₂-refl
  ; sym           to ≈₂-sym
  ; trans         to ≈₂-trans
  ; _+_           to _+₂_
  ; _∙_           to _∙₂_
  ; -_            to -₂_
  ; 0#            to 0₂
  ; +-identityˡ    to +₂-identityˡ
  ; +-identityʳ    to +₂-identityʳ
  ; +-identity    to +₂-identity
  ; +-cong        to +₂-cong
  ; +-assoc       to +₂-assoc
  ; +-comm        to +₂-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₂-compat
  ; ∙-+-distrib   to ∙₂-+₂-distrib
  ; ∙-+ᵏ-distrib  to ∙₂-+ᵏ-distrib
  ; ∙-cong        to ∙₂-cong
  ; ∙-identity    to ∙₂-identity
  ; ∙-absorbˡ      to ∙₂-absorbˡ
  ; ∙-absorbʳ      to ∙₂-absorbʳ
  ; -‿cong        to -₂‿cong
  ; -‿inverseˡ    to -₂‿inverseˡ
  ; -‿inverseʳ    to -₂‿inverseʳ
  ; vectorSpace   to vectorSpace₂
  ; embed         to embed₂
  )

open LinearIsomorphism embed₁
  using ()
  renaming
  ( ⟦_⟧        to ⟦_⟧₁
  ; ⟦⟧-cong    to ⟦⟧₁-cong
  ; injective  to ⟦⟧₁-injective
  ; surjective to ⟦⟧₁-surjective
  ; +-homo     to +₁-homo
  ; ∙-homo     to ∙₁-homo
  ; 0#-homo    to 0₁-homo
  )

open LinearIsomorphism embed₂
  using ()
  renaming
  ( ⟦_⟧        to ⟦_⟧₂
  ; ⟦⟧-cong    to ⟦⟧₂-cong
  ; injective  to ⟦⟧₂-injective
  ; surjective to ⟦⟧₂-surjective
  ; +-homo     to +₂-homo
  ; ∙-homo     to ∙₂-homo
  ; 0#-homo    to 0₂-homo
  )

import Algebra.Linear.Construct.HomSpace K vectorSpace₁ vectorSpace₂ as PS

open VS.VectorSpace PS.vectorSpace
  renaming
    ( refl  to ≈-refl
    ; sym   to ≈-sym
    ; trans to ≈-trans
    )

import Algebra.Linear.Construct.Vector as Vec
open Vec K
  using
    ( ++-cong
    ; ++-identityˡ
    ; +-distrib-++
    ; ∙-distrib-++
    ; 0++0≈0
    )
  renaming
    ( _≈_         to _≈v_
    ; ≈-refl      to ≈v-refl
    ; ≈-sym       to ≈v-sym
    ; ≈-trans     to ≈v-trans
    ; _+_         to _+v_
    ; _∙_         to _∙v_
    ; 0#          to 0v
    ; +-cong      to +v-cong
    ; setoid      to vec-setoid
    ; vectorSpace to vector-vectorSpace
    )

import Algebra.Linear.Construct.Matrix K as M

open import Data.Nat hiding (_+_) renaming (_*_ to _*ℕ_)

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; subst-subst-sym)
  renaming
  ( refl  to ≡-refl
  ; sym   to ≡-sym
  ; trans to ≡-trans
  )

open import Data.Vec
open import Data.Product
open import Data.Fin
open import Function

δ : ∀ {n p} -> Fin n -> Fin p -> K'
δ zero zero = 1ᵏ
δ (suc n) zero = 0ᵏ
δ zero (suc p) = 0ᵏ
δ (suc n) (suc p) = δ n p

canonicalBasis : M.Matrix n p
canonicalBasis = M.tabulate δ

module _ where
  open import Algebra.Morphism.Definitions (LinearMap vectorSpace₁ vectorSpace₂) (M.Matrix n p) M._≈_
  open import Algebra.Linear.Morphism.Definitions K (LinearMap vectorSpace₁ vectorSpace₂) (M.Matrix n p) M._≈_
  import Relation.Binary.Morphism.Definitions (LinearMap vectorSpace₁ vectorSpace₂) (M.Matrix n p) as R
  open import Relation.Binary.EqReasoning (M.setoid {n} {p})

  Mat : LinearMap vectorSpace₁ vectorSpace₂ -> M.Matrix n p
  Mat f = M.mapCols (λ u -> embed₂ LinearIsomorphism.⟪$⟫ (f LinearMap.⟪$⟫ {! embed₁ ⁻¹ ⟪$⟫ u!}))
                    canonicalBasis

-- (λ u → embed₂ LinearIsomorphism.⟪$⟫ (proj₁ (⟦⟧₂-surjective u))) canonicalBasis

  Mat-cong : R.Homomorphic₂ _≈_ M._≈_ Mat
  Mat-cong {A} {B} f =
    begin
      Mat A
    ≈⟨ M.≈-reflexive (M.mapCols-cong (λ u → {!!}) canonicalBasis) ⟩
      {!!}
    ≈⟨ {!!} ⟩
      Mat B
    ∎

{-

Mat-cong : R.Homomorphic₂ PS._≈_ _≈v_ Mat
⟦⟧-cong (r₁ , r₂) = ++-cong (⟦⟧₁-cong r₁) (⟦⟧₂-cong r₂)

+-homo : Homomorphic₂ ⟦_⟧ _+_ _+v_
+-homo (x₁ , x₂) (y₁ , y₂) =
    begin
      ⟦ (x₁ , x₂) + (y₁ , y₂) ⟧
    ≡⟨⟩
      ⟦ x₁ +₁ y₁ ⟧₁ ++ ⟦ x₂ +₂ y₂ ⟧₂
    ≈⟨ ++-cong (+₁-homo x₁ y₁) (+₂-homo x₂ y₂) ⟩
      (⟦ x₁ ⟧₁ +v ⟦ y₁ ⟧₁) ++ (⟦ x₂ ⟧₂ +v ⟦ y₂ ⟧₂)
    ≈⟨ ≈v-sym (+-distrib-++ ⟦ x₁ ⟧₁ ⟦ x₂ ⟧₂ ⟦ y₁ ⟧₁ ⟦ y₂ ⟧₂) ⟩
      (⟦ x₁ ⟧₁ ++ ⟦ x₂ ⟧₂) +v (⟦ y₁ ⟧₁ ++ ⟦ y₂ ⟧₂)
    ≈⟨ +v-cong ≈v-refl ≈v-refl ⟩
       ⟦ x₁ , x₂ ⟧ +v ⟦ y₁ , y₂ ⟧
    ∎

0#-homo : Homomorphic₀ ⟦_⟧ 0# 0v
0#-homo =
  begin
    ⟦ 0# ⟧
  ≡⟨⟩
    ⟦ 0₁ ⟧₁ ++ ⟦ 0₂ ⟧₂
  ≈⟨ ++-cong 0₁-homo 0₂-homo ⟩
    (0v {n}) ++ (0v {p})
  ≈⟨ 0++0≈0 {n} {p} ⟩
    0v {n +ℕ p}
  ∎

∙-homo : ScalarHomomorphism ⟦_⟧ _∙_ _∙v_
∙-homo c (x₁ , x₂) =
  begin
    ⟦ c ∙ (x₁ , x₂) ⟧
  ≈⟨ ++-cong (∙₁-homo c x₁) (∙₂-homo c x₂) ⟩
    (c ∙v ⟦ x₁ ⟧₁) ++ (c ∙v ⟦ x₂ ⟧₂)
  ≈⟨ ≈v-sym (∙-distrib-++ c ⟦ x₁ ⟧₁ ⟦ x₂ ⟧₂) ⟩
    c ∙v ⟦ x₁ , x₂ ⟧
  ∎

⟦⟧-injective : Injective ⟦_⟧
⟦⟧-injective {x₁ , x₂} {y₁ , y₂} r =
  let (r₁ , r₂) = ++-split r
  in ⟦⟧₁-injective r₁ , ⟦⟧₂-injective r₂

⟦⟧-surjective : Surjective ⟦_⟧
⟦⟧-surjective y =
  let (x₁ , x₂) = splitAt' n p ≡-refl y
      (u , r₁) = ⟦⟧₁-surjective x₁
      (v , r₂) = ⟦⟧₂-surjective x₂
  in  (u , v) , ≈v-trans (++-cong r₁ r₂) (++-splitAt' {n} {p} y)

embed : LinearIsomorphism PS.vectorSpace (vector-vectorSpace {n +ℕ p})
embed = record
  { ⟦_⟧ = ⟦_⟧
  ; isLinearIsomorphism = record
    { isLinearMonomorphism = record
      { isLinearMap = record
        { isAbelianGroupMorphism = record
          { gp-homo = record
            { mn-homo = record
              { sm-homo = record
                { ⟦⟧-cong = ⟦⟧-cong
                ; ∙-homo = +-homo
                }
              ; ε-homo = 0#-homo
              }
            }
          }
        ; ∙-homo = ∙-homo
        }
      ; injective = ⟦⟧-injective
      }
    ; surjective = ⟦⟧-surjective
    }
  }

isFiniteDimensional : IsFiniteDimensional _≈_ _+_ _∙_ -_ 0# (n +ℕ p)
isFiniteDimensional = record
  { isVectorSpace = isVectorSpace
  ; embed         = embed
  }
-}

ext: agda

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by join semilattices
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.JoinSemilattice
  {c ℓ₁ ℓ₂} (J : JoinSemilattice c ℓ₁ ℓ₂) where

open JoinSemilattice J

import Algebra as Alg
import Algebra.Structures as Alg
import Algebra.FunctionProperties as P; open P _≈_
open import Data.Product
open import Function using (_∘_; flip)
open import Relation.Binary
open import Relation.Binary.Properties.Poset poset

import Relation.Binary.Reasoning.PartialOrder as PoR

-- The join operation is monotonic.

∨-monotonic : _∨_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
∨-monotonic {x} {y} {u} {v} x≤y u≤v =
  let _     , _     , least  = supremum x u
      y≤y∨v , v≤y∨v , _      = supremum y v
  in least (y ∨ v) (trans x≤y y≤y∨v) (trans u≤v v≤y∨v)

∨-cong : _∨_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
∨-cong x≈y u≈v = antisym (∨-monotonic (reflexive x≈y) (reflexive u≈v))
                         (∨-monotonic (reflexive (Eq.sym x≈y))
                                      (reflexive (Eq.sym u≈v)))

-- The join operation is commutative, associative and idempotent.

∨-comm : Commutative _∨_
∨-comm x y =
  let x≤x∨y , y≤x∨y , least  = supremum x y
      y≤y∨x , x≤y∨x , least′ = supremum y x
  in antisym (least (y ∨ x) x≤y∨x y≤y∨x) (least′ (x ∨ y) y≤x∨y x≤x∨y)

∨-assoc : Associative _∨_
∨-assoc x y z =
  let x∨y≤[x∨y]∨z , z≤[x∨y]∨z   , least  = supremum (x ∨ y) z
      x≤x∨[y∨z]   , y∨z≤x∨[y∨z] , least′ = supremum x (y ∨ z)
      y≤y∨z       , z≤y∨z       , _      = supremum y z
      x≤x∨y       , y≤x∨y       , _      = supremum x y
  in antisym (least  (x ∨ (y ∨ z)) (∨-monotonic refl y≤y∨z)
                     (trans z≤y∨z y∨z≤x∨[y∨z]))
             (least′ ((x ∨ y) ∨ z) (trans x≤x∨y x∨y≤[x∨y]∨z)
                     (∨-monotonic y≤x∨y refl))

∨-idempotent : Idempotent _∨_
∨-idempotent x =
  let x≤x∨x , _ , least = supremum x x
  in antisym (least x refl refl) x≤x∨x

x≤y⇒x∨y≈y : ∀ {x y} → x ≤ y → x ∨ y ≈ y
x≤y⇒x∨y≈y {x} {y} x≤y = antisym
  (begin x ∨ y ≤⟨ ∨-monotonic x≤y refl ⟩
         y ∨ y ≈⟨ ∨-idempotent _ ⟩
         y ∎)
  (y≤x∨y _ _)
  where open PoR poset

-- Every order-theoretic semilattice can be turned into an algebraic one.

isAlgSemilattice : Alg.IsSemilattice _≈_ _∨_
isAlgSemilattice = record
  { isBand = record
    { isSemigroup = record
      { isMagma   = record
        { isEquivalence = isEquivalence
        ; ∙-cong        = ∨-cong
        }
      ; assoc  = ∨-assoc
      }
    ; idem     = ∨-idempotent
    }
  ; comm       = ∨-comm
  }

algSemilattice : Alg.Semilattice c ℓ₁
algSemilattice = record { isSemilattice = isAlgSemilattice }

-- The dual construction is a meet semilattice.

dualIsMeetSemilattice : IsMeetSemilattice _≈_ (flip _≤_) _∨_
dualIsMeetSemilattice = record
  { isPartialOrder = invIsPartialOrder
  ; infimum        = supremum
  }

dualMeetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
dualMeetSemilattice = record
  { _∧_               = _∨_
  ; isMeetSemilattice = dualIsMeetSemilattice
  }


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

interleaved mutual

  data Rec : Set
  ⟦_⟧ : Rec → Set

  constructor `Nat : Rec
  ⟦ `Nat   ⟧ = Nat

  _ : Rec
  _ = `Σ `Nat (λ _ → `Nat)

  _ : Rec → Rec
  _ = λ r → `Σ r (λ _ → `Nat)

  constructor `Σ : (r : Rec) → (⟦ r ⟧ → Rec) → Rec
  ⟦ `Σ A B ⟧ = Σ ⟦ A ⟧ λ a → ⟦ B a ⟧

_+1-Nats : Nat → Rec
zero  +1-Nats = `Nat
suc n +1-Nats = `Σ `Nat λ _ → n +1-Nats

Nats : Rec
Nats = `Σ `Nat _+1-Nats

[1] : ⟦ Nats ⟧
[1] = 0 , 1

[1⋯3] : ⟦ Nats ⟧
[1⋯3] = 2 , 1 , 2 , 3

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module Lecture4 where

import Lecture3
open Lecture3 public

-- the identity type on a type A, given a fixed basepoint x
data Id {i : Level} {A : UU i} (x : A) : A → UU i where
  refl : Id x x

_==_ : {i : Level} {A : UU i} (x y : A) → UU i
x == y = Id x y

ind-Id : {i j : Level} {A : UU i} {x : A} (B : (y : A) (p : Id x y) → UU j) →
  (B x refl) → (y : A) (p : Id x y) → B y p
ind-Id x b y refl = b

-- groupoid structure on identity types (a.k.a. paths)

inv : {i : Level} {A : UU i} {x y : A} → Id x y → Id y x
inv (refl) = refl

_⁻¹ : {i : Level} {A : UU i} {x y : A} → Id x y → Id y x
x ⁻¹ = inv x

concat : {i : Level} {A : UU i} {x z : A} (y : A) → Id x y → Id y z → Id x z
concat x refl q = q

_·_ : {i : Level} {A : UU i} {x z : A} {y : A} → Id x y → Id y z → Id x z
p · q = concat _ p q

-- equational reasoning (TODO: demonstrate this by reworking some of the proofs to use it)
infix 15 _==∎    -- \qed
infixr 10 _==⟨_⟩_    -- \< \>

_==∎ : ∀ {i : Level} {A : UU i} (a : A) → a == a
a ==∎ = refl

_==⟨_⟩_ : ∀ {i : Level} {A : UU i} (a : A) {b c : A} → a == b → b == c → a == c
a ==⟨ γ ⟩ η = γ · η
-- end equational reasoning

assoc : {i : Level} {A : UU i} {x y z w : A} (p : Id x y) (q : Id y z) (r : Id z w) → Id (concat _ p (concat _ q r)) (concat _ (concat _ p q) r)
assoc refl q r = refl

left-unit : {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (concat _ refl p) p
left-unit refl = refl

right-unit : {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (concat _ p refl) p
right-unit refl = refl

left-inv : {i : Level} {A : UU i} {x y : A} (p : Id x y) →
  Id (concat _ (inv p) p) refl
left-inv refl = refl

right-inv : {i : Level} {A : UU i} {x y : A} (p : Id x y) →
  Id (concat _ p (inv p)) refl
right-inv refl = refl

-- action on paths of a function

ap : {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A} (p : Id x y) → Id (f x) (f y)
ap f refl = refl

ap-id : {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (ap id p) p
ap-id refl = refl

ap-comp : {i j k : Level} {A : UU i} {B : UU j} {C : UU k} (g : B → C) (f : A → B) {x y : A} (p : Id x y) → Id (ap (comp g f) p) (ap g (ap f p))
ap-comp g f refl = refl

ap-refl : {i j : Level} {A : UU i} {B : UU j} (f : A → B) (x : A) →
  Id (ap f (refl {_} {_} {x})) refl
ap-refl f x = refl

ap-concat : {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y z : A} (p : Id x y) (q : Id y z) → Id (ap f (concat _ p q)) (concat _ (ap f p) (ap f q))
ap-concat f refl q = refl

ap-inv : {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A} (p : Id x y) → Id (ap f (inv p)) (inv (ap f p))
ap-inv f refl = refl

tr : {i j : Level} {A : UU i} (B : A → UU j) {x y : A} (p : Id x y) (b : B x) → B y
tr B refl b = b

apd : {i j : Level} {A : UU i} {B : A → UU j} (f : (x : A) → B x) {x y : A} (p : Id x y) → Id (tr B p (f x)) (f y)
apd f refl = refl

-- Exercises below

-- Exercise 4.1 The composition of transports is the transport of the concatenation
tr-concat : {i j : Level} {A : UU i} (B : A → UU j) {x y z : A} (p : Id x y) (q : Id y z) (b : B x) → Id (tr B q (tr B p b)) (tr B (concat _ p q) b)
tr-concat B refl refl b = refl

-- Exercise 4.2 Taking the inverse distributes contravariantly over concatenation
inv-assoc : {i : Level} {A : UU i} {x y z : A} (p : Id x y) (q : Id y z) → Id (inv (concat _ p q)) (concat _ (inv q) (inv p))
inv-assoc refl refl = refl

-- Exercise 4.3 If B is a weakened family over A (trivial bundle, not dependent), then tr is refl
tr-triv : {i j : Level} {A : UU i} {B : UU j} {x y : A} (p : Id x y) (b : B) → Id (tr (weaken A B) p b) b
tr-triv refl b = refl

-- Exercise 4.4 Transporting, using x=y and f:A → B, an identity between identities
tr-fib : {i j : Level} {A : UU i} {B : UU j} {f : A → B} {x y : A} (p : Id x y) (b : B) →
  (q : Id (f x) b) → Id (tr (λ (a : A) → Id (f a) b) p q) (concat _ (inv (ap f p)) q)
tr-fib refl b q = refl

tr-fib' : {i j : Level} {A : UU i} {B : UU j} {f : A → B} {x y : A} (p : Id x y) (b : B) →
  (q : Id b (f x)) → Id (tr (λ (a : A) → Id b (f a)) p q) (concat _ q (ap f p))
tr-fib' refl b refl = refl

-- Exercise 4.5
inv-con : {i : Level} {A : UU i} {x y z : A} (p : Id x y) (q : Id y z) (r : Id x z) → (Id (p · q) r) → (Id q ((inv p) · r))
inv-con refl refl r refl = refl

con-inv : {i : Level} {A : UU i} {x y z : A} (p : Id x y) (q : Id y z) (r : Id x z) → (Id (p · q) r) → (Id p (r · (inv q)))
con-inv refl refl r refl = refl

-- Exercise 4.6 Path lifting, from a path in the base A to a path in the total space Σ A B
lift : {i j : Level} {A : UU i} {B : A → UU j} {x y : A} (p : Id x y) (b : B x) → Id (dpair x b) (dpair y (tr B p b))
lift refl b = refl

-- Exercise 4.7 Some laws of arithmetic (follow-up from Remark 2.3.1)
right-unit-addN : (m : ℕ) → Id (m + Nzero) m
right-unit-addN Nzero = refl
right-unit-addN (Nsucc m) = ap Nsucc (right-unit-addN m)

left-unit-addN : (m : ℕ) → Id (Nzero + m) m
left-unit-addN m = refl

assoc-addN : (m n k : ℕ) → Id (m + (n + k)) ((m + n) + k)
assoc-addN Nzero n k = refl
assoc-addN (Nsucc m) n k = ap Nsucc (assoc-addN m n k)

right-succ-addN : (m n : ℕ) → Id (m + (Nsucc n)) (Nsucc (m + n))
right-succ-addN Nzero n = refl
right-succ-addN (Nsucc m) n = ap Nsucc (right-succ-addN m n)

comm-addN : (m n : ℕ) → Id (m + n) (n + m)
comm-addN Nzero Nzero = refl
comm-addN Nzero (Nsucc n) = ap Nsucc (comm-addN Nzero n)
comm-addN (Nsucc m) Nzero = ap Nsucc (comm-addN m Nzero)
comm-addN (Nsucc m) (Nsucc n) =
  ((Nsucc m) + (Nsucc n))
    ==⟨ ap Nsucc (comm-addN m (Nsucc n)) ⟩
  (Nsucc ((Nsucc n) + m))
    ==⟨ inv (right-succ-addN (Nsucc n) m) ⟩
  ((Nsucc n) + (Nsucc m))
    ==∎

left-zero-mulN : (m : ℕ) → Id (Nzero ** m) Nzero
left-zero-mulN m = refl

right-zero-mulN : (m : ℕ) → Id (m ** Nzero) Nzero
right-zero-mulN Nzero = refl
right-zero-mulN (Nsucc m) = concat (m ** Nzero) (right-unit-addN _) (right-zero-mulN m)

left-unit-mulN : (m : ℕ) → Id ((Nsucc Nzero) ** m) m
left-unit-mulN m = refl

right-unit-mulN : (m : ℕ) → Id (m ** (Nsucc Nzero)) m
right-unit-mulN Nzero = refl
right-unit-mulN (Nsucc m) =
  ((Nsucc m) ** (Nsucc Nzero))
    ==⟨ comm-addN _ (Nsucc Nzero) ⟩
  (Nsucc Nzero) + (m ** (Nsucc Nzero))
    ==⟨ ap Nsucc (right-unit-mulN m) ⟩
  (Nsucc m)
    ==∎

distr-addN-mulN : (m n k : ℕ) → Id ((m + n) ** k) ((m ** k) + (n ** k))
distr-addN-mulN Nzero n k = refl
distr-addN-mulN (Nsucc m) n k =
  ((Nsucc m) + n) ** k
    ==⟨ refl ⟩
  (Nsucc (m + n)) ** k
    ==⟨ refl ⟩
  ((m + n) ** k) + k
    ==⟨ ap (λ x → x + k) (distr-addN-mulN m n k) ⟩
  ((m ** k) + (n ** k)) + k
    ==⟨ inv (assoc-addN (m ** k) (n ** k) k) ⟩
  (m ** k) + ((n ** k) + k)
    ==⟨ ap (λ x → (m ** k) + x) (comm-addN (n ** k) k) ⟩
  (m ** k) + (k + (n ** k))
    ==⟨ assoc-addN (m ** k) k (n ** k) ⟩
  ((m ** k) + k) + (n ** k)
    ==⟨ refl ⟩
  ((Nsucc m) ** k) + (n ** k)
    ==∎

assoc-mulN : (m n k : ℕ) → Id (m ** (n ** k)) ((m ** n) ** k)
assoc-mulN Nzero n k = refl
assoc-mulN (Nsucc m) n k =
  ((Nsucc m) ** (n ** k))
    ==⟨ refl ⟩
  (m ** (n ** k)) + (n ** k)
    ==⟨ ap (λ x → x + (n ** k)) (assoc-mulN m n k) ⟩
  ((m ** n) ** k) + (n ** k)
    ==⟨ inv (distr-addN-mulN (m ** n) n k) ⟩
  ((m ** n) + n) ** k
    ==⟨ refl ⟩
  (Nsucc m ** n) ** k
    ==∎


text:
-- Testing how the pragmas are saved in the agda interface files (using
-- the program dump-agdai) when they are used from the command-line:

-- $ agda --no-termination-check OptionPragmaCommandLine.agda

-- 17 October 2012. Because the PragmaOption --no-termination-check
-- was used from the command-line it is *not* saved in the interface
-- file.

-- iPragmaOptions = []

module OptionPragmaCommandLine where

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical-compatible #-}

open import Agda.Builtin.Equality

subst :
  {A : Set} {@0 x y : A}
  (@0 P : A → Set) → x ≡ y → P x → P y
subst P refl p = p


text:
module Lists.Reverse where

open import Lists
open import Nats
open import Equality
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  -- rev$v:a=a:rev$v : ∀ {n m} {A : Set n} (a : A) (v : List A m) →
  --                 rev (v ∷ʳ a) ≡ a ∷ rev v
  -- rev$v:a=a:rev$v _ [] = refl
  -- rev$v:a=a:rev$v a (_ ∷ xs) with rev (xs ∷ʳ a) | rev$v:a=a:rev$v a xs
  -- ...                            | .(a ∷ rev xs) | refl = refl

  rev$v:a=a:rev$v : ∀ {n} {A : Set n} (a : A) (v : List A) →
                  reverse (v ∷ʳ a) ≡ a ∷ reverse v
  rev$v:a=a:rev$v _ [] = refl
  rev$v:a=a:rev$v a (_ ∷ xs)
    rewrite rev$v:a=a:rev$v a xs
            = refl

  rev∘rev=id : ∀ {n} {A : Set n} (v : List A) → reverse (reverse v) ≡ v
  rev∘rev=id [] = refl
  rev∘rev=id (x ∷ xs)
    rewrite rev$v:a=a:rev$v x $ reverse xs
          | rev∘rev=id xs
            = refl

------------------------------------------------------------------------
-- public aliases

list-rev-rev-id : ∀ {n} {A : Set n} (v : List A) → reverse (reverse v) ≡ v
list-rev-rev-id = rev∘rev=id


text:
module Structure.Operator.Monoid.Monoids.Coset where

open import Functional
open import Function.Equals
open import Function.Equals.Proofs
import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Predicate.Equiv
open import Sets.PredicateSet renaming (_≡_ to _≡ₛ_)
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function.Multi
open import Structure.Operator.Monoid
open import Structure.Operator.Monoid.Homomorphism
open import Structure.Operator.Monoid.Monoids.Function
open import Structure.Operator.Monoid.Submonoid
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ function : ∀{f : T → T} → Function(f) ⦄ {_▫_ : T → T → T} (monoid : Monoid(_▫_)) where
  cosetₗ-submonoid : Submonoid(function-monoid)(⊶(_▫_))
  Submonoid.contains-identity cosetₗ-submonoid = [∃]-intro (_) ⦃ intro(identityₗ(_▫_)(_)) ⦄
  Submonoid.operator-closure  cosetₗ-submonoid {f}{g} ⦃ [∃]-intro a ⦃ pa ⦄ ⦄ ⦃ [∃]-intro b ⦃ pb ⦄ ⦄ =
    [∃]-intro (a ▫ b) ⦃ intro (\{x} →
      ((a ▫ b) ▫ x) 🝖[ _≡ₑ_ ]-[ associativity(_▫_) ]
      (a ▫ (b ▫ x)) 🝖[ _≡ₑ_ ]-[ _⊜_.proof pa ]
      f(b ▫ x)      🝖[ _≡ₑ_ ]-[ congruence₁(f) (_⊜_.proof pb) ]
      f(g(x))       🝖[ _≡ₑ_ ]-[]
      (f ∘ g)(x)    🝖-end
    ) ⦄

  cosetᵣ-submonoid : Submonoid(function-monoid)(⊶(swap(_▫_)))
  Submonoid.contains-identity cosetᵣ-submonoid = [∃]-intro (_) ⦃ intro(identityᵣ(_▫_)(_)) ⦄
  Submonoid.operator-closure  cosetᵣ-submonoid {f}{g} ⦃ [∃]-intro a ⦃ pa ⦄ ⦄ ⦃ [∃]-intro b ⦃ pb ⦄ ⦄ =
    [∃]-intro (b ▫ a) ⦃ intro (\{x} →
      (x ▫ (b ▫ a)) 🝖[ _≡ₑ_ ]-[ associativity(_▫_) ]-sym
      ((x ▫ b) ▫ a) 🝖[ _≡ₑ_ ]-[ _⊜_.proof pa ]
      f(x ▫ b)      🝖[ _≡ₑ_ ]-[ congruence₁(f) (_⊜_.proof pb) ]
      f(g(x))       🝖[ _≡ₑ_ ]-[]
      (f ∘ g)(x)    🝖-end
    ) ⦄

  cosetₗ-homomorphism : ∃(Homomorphism monoid (Submonoid.monoid cosetₗ-submonoid))
  ∃.witness cosetₗ-homomorphism a = [∃]-intro (a ▫_) ⦃ [∃]-intro a ⦃ reflexivity(_≡ₑ_) {a ▫_} ⦄ ⦄
  _⊜_.proof (Function.congruence (Homomorphism.function (∃.proof cosetₗ-homomorphism)) ab) {x}  = congruence₂ₗ(_▫_)(x) ab
  _⊜_.proof (Preserving.proof (Homomorphism.preserve-op (∃.proof cosetₗ-homomorphism))     {x}) = associativity(_▫_)
  _⊜_.proof (Preserving.proof (Homomorphism.preserve-id (∃.proof cosetₗ-homomorphism)))    {x}  = identityₗ(_▫_)(_)

  instance
    cosetₗ-surjective : Surjective([∃]-witness cosetₗ-homomorphism)
    Surjective.proof cosetₗ-surjective {[∃]-intro f ⦃ pf ⦄} = pf

  instance
    cosetₗ-injective : Injective([∃]-witness cosetₗ-homomorphism)
    Injective.proof cosetₗ-injective {x} {y} (intro xy) =
      x                    🝖[ _≡ₑ_ ]-[ identityᵣ(_▫_)(_) ]-sym
      x ▫ Monoid.id monoid 🝖[ _≡ₑ_ ]-[ xy {Monoid.id monoid} ]
      y ▫ Monoid.id monoid 🝖[ _≡ₑ_ ]-[ identityᵣ(_▫_)(_) ]
      y                    🝖-end

  instance
    cosetₗ-bijective : Bijective([∃]-witness cosetₗ-homomorphism)
    cosetₗ-bijective = injective-surjective-to-bijective([∃]-witness cosetₗ-homomorphism)

  {-
  cosetᵣ-homomorphism : ∃(Homomorphism monoid (Submonoid.monoid cosetᵣ-submonoid))
  ∃.witness cosetᵣ-homomorphism a = [∃]-intro (_▫ a) ⦃ [∃]-intro a ⦃ reflexivity(_≡ₑ_) {_▫ a} ⦄ ⦄
  _⊜_.proof (Function.congruence (Homomorphism.function (∃.proof cosetᵣ-homomorphism)) ab) {x}  = congruence₂ᵣ(_▫_)(x) ab
  _⊜_.proof (Preserving.proof (Homomorphism.preserve-op (∃.proof cosetᵣ-homomorphism)) {a} {b}) {x} =
    (x ▫ (a ▫ b)) 🝖[ _≡ₑ_ ]-[ {!!} ]
    ((x ▫ b) ▫ a) 🝖-end
  _⊜_.proof (Preserving.proof (Homomorphism.preserve-id (∃.proof cosetᵣ-homomorphism)))    {x}  = identityᵣ(_▫_)(_)
  -}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Exponentials and closed categories
module CategoryTheory.BCCCs.Closed where
open import CategoryTheory.Categories
open import CategoryTheory.BCCCs.Cartesian

module _ {n} {ℂ : Category n} (Cℂ : Cartesian ℂ) where

    open Category ℂ
    open Cartesian Cℂ

    -- Exponential from two objects
    record Exponential (A B : obj) : Set (lsuc n) where
        field
            -- | Data
            -- Exponential object
            A⇒B : obj
            -- Evaluation map
            eval : A⇒B ⊗ A ~> B
            -- Canonical transposition morphism (currying)
            Λ : ∀{E} -> (E ⊗ A ~> B) -> (E ~> A⇒B)

            -- | Laws
            Λ-comm : ∀{E} -> {e : E ⊗ A ~> B}
                  -> eval ∘ (Λ e * id) ≈ e
            Λ-unique : ∀{E} -> {e : E ⊗ A ~> B} {m : E ~> A⇒B}
                  -> eval ∘ (m * id) ≈ e -> Λ e ≈ m
            Λ-cong : ∀{E} {f g : E ⊗ A ~> B}
                  -> f ≈ g -> Λ f ≈ Λ g

        -- Currying identity
        Λ-*id : ∀{D E} {f : E ⊗ A ~> B} {g : D ~> E}
             -> Λ (f ∘ (g * id)) ≈ Λ f ∘ g
        Λ-*id {D}{E}{f}{g} =
            begin
                Λ (f ∘ (g * id))
            ≈⟨ Λ-cong (≈-cong-left (Λ-comm [sym]) ≈> ∘-assoc) ⟩
                Λ (eval ∘ (Λ f * id) ∘ (g * id))
            ≈⟨ Λ-cong (≈-cong-right (*-idemp-dist-∘ id-left)) ⟩
                Λ (eval ∘ (Λ f ∘ g) * id)
            ≈⟨ Λ-unique r≈ ⟩
                Λ f ∘ g
            ∎

-- Type class for closed categories
-- definition using exponentials
record Closed {n} {ℂ : Category n} (Cℂ : Cartesian ℂ) : Set (lsuc n) where
    open Category ℂ
    field
        -- Exponential object for each pair of objects
        exp : ∀(A B : obj) -> Exponential Cℂ A B

    open module E {A} {B} = Exponential (exp A B) public

    -- Shorthand for exponential object
    infixr 20 _⇒_
    _⇒_ : (A B : obj) -> obj
    A ⇒ B = A⇒B {A} {B}

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
{-

Please do not move this file. Changes should only be made if
necessary.

This file contains benchmarks for the paper:

Synthetic Integral Cohomology in Cubical Agda
Guillaume Brunerie, Axel Ljungström, Anders Mörtberg
Computer Science Logic (CSL) 2022

Command to run the benchmarks and get timings:

agda -v profile.definitions:10 Benchmarks.agda

This assumes that there is no Benchmarks.agdai file. If there is one,
then it should be removed before the above command is run.

-}

{-# OPTIONS --safe #-}
module Cubical.Experiments.ZCohomology.Benchmarks where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Int
open import Cubical.HITs.Sn
open import Cubical.Algebra.Group hiding (ℤ ; Bool)
open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure hiding (_+ₕ_) renaming (_+'ₕ_ to _+ₕ_)
{- _+'ₕ_ is just (λ x y → (x +ₕ 0ₕ) +ₕ (y +ₕ 0ₕ))
   For technical reason, this gives nicer reductions and computes better in
   higher dimensions. -}
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Torus
open import Cubical.ZCohomology.Groups.KleinBottle
open import Cubical.ZCohomology.Groups.WedgeOfSpheres
open import Cubical.ZCohomology.Groups.RP2
open import Cubical.ZCohomology.Groups.CP2
open import Cubical.Data.Sigma

open import Cubical.HITs.KleinBottle
open import Cubical.HITs.RPn.Base
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Pushout
open import Cubical.HITs.Hopf
open import Cubical.HITs.Truncation
open import Cubical.HITs.Susp
open import Cubical.HITs.S1

open IsGroupHom
open Iso

-- S¹ (everything fast)
module S1-tests where

  ϕ : coHom 1 (S₊ 1) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 0))

  ϕ⁻¹ : ℤ → coHom 1 (S₊ 1)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 0))

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- <10ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 1) ≡ 1    -- <10ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0   -- <10ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 12ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 13ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ -3 +ₕ ϕ⁻¹ 4) ≡ 1    -- 37ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ -5 +ₕ ϕ⁻¹ -2) ≡ -7    -- 38ms
  test₇ = refl

-- S²
module S2-tests where

  ϕ : coHom 2 (S₊ 2) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 1))

  ϕ⁻¹ : ℤ → coHom 2 (S₊ 2)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 1))

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 13ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 1) ≡ 1    -- 17ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 1,152ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 1,235ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 1,208ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 1) ≡ 2    -- 1,153ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ 2 +ₕ ϕ⁻¹ 4) ≡ 6    -- 1,365ms
  test₇ = refl

-- S³
module S3-tests where

  ϕ : coHom 3 (S₊ 3) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 2))

  ϕ⁻¹ : ℤ → coHom 3 (S₊ 3)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 2))

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 228ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 1) ≡ 1    -- 231ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 325ms
  test₃ = refl

{-
  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- nope
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- nope
  test₅ = refl
-}

-- S⁴
module S4-tests where

  ϕ : coHom 4 (S₊ 4) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 3))

  ϕ⁻¹ : ℤ → coHom 4 (S₊ 4)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 3))

{- _+ₕ_ Fails already here...
  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- nope
  test₁ = refl
-}

-- ϕ can handle 0ₕ fast
  test₂ : ϕ (0ₕ _) ≡ 0     -- < 10ms
  test₂ = refl

{- It fails to map the generator to 1, however.
  test₂ : ϕ (∣ ∣_∣ ∣₂) ≡ 1    -- nope
  test₂ = refl
-}

module S1∨S1∨S2-tests₁ where -- everything fast

  ϕ : coHom 1 S²⋁S¹⋁S¹ → ℤ × ℤ
  ϕ = fun (fst H¹-S²⋁S¹⋁S¹)

  ϕ⁻¹ : ℤ × ℤ → coHom 1 S²⋁S¹⋁S¹
  ϕ⁻¹ = inv (fst H¹-S²⋁S¹⋁S¹)

  test₁ : ϕ (ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 11ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ (3 , 1)) ≡ (3 , 1)    -- 23ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ (0 , 0) +ₕ ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 19ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ (0 , 1) +ₕ ϕ⁻¹ (1 , 0)) ≡ (1 , 1)    -- 26ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ (3 , 2) +ₕ ϕ⁻¹ (-1 , 5)) ≡ (2 , 7)    -- 62ms
  test₅ = refl

module S1∨S1∨S2-tests₂ where

  ϕ : coHom 2 S²⋁S¹⋁S¹ → ℤ
  ϕ = fun (fst H²-S²⋁S¹⋁S¹)

  ϕ⁻¹ : ℤ → coHom 2 S²⋁S¹⋁S¹
  ϕ⁻¹ = inv (fst H²-S²⋁S¹⋁S¹)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 106ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 125ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 9,689ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 9,235ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 9,748ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 1) ≡ 2    -- 9,136ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ 2 +ₕ ϕ⁻¹ 4) ≡ 6    -- 9,557ms
  test₇ = refl

module Torus-test₁ where -- fast

  ϕ : coHom 1 (S₊ 1 × S₊ 1) → ℤ × ℤ
  ϕ = fun (fst H¹-T²≅ℤ×ℤ)

  ϕ⁻¹ : ℤ × ℤ → coHom 1 (S₊ 1 × S₊ 1)
  ϕ⁻¹ = inv (fst H¹-T²≅ℤ×ℤ)

  test₁ : ϕ (ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 11ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ (3 , 1)) ≡ (3 , 1)    -- 17ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ (0 , 0) +ₕ ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 19ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ (0 , 1) +ₕ ϕ⁻¹ (1 , 0)) ≡ (1 , 1)    -- 26ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ (-3 , 2) +ₕ ϕ⁻¹ (-1 , 5)) ≡ (-4 , 7)    -- 61ms
  test₅ = refl

module Torus-test₂ where

  ϕ : coHom 2 (S₊ 1 × S₊ 1) → ℤ
  ϕ = fun (fst H²-T²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 2 (S₊ 1 × S₊ 1)
  ϕ⁻¹ = inv (fst H²-T²≅ℤ)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 136sm
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 154ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 12,790ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 12,366ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 12,257ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 1) ≡ 2    -- 13,092ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ 2 +ₕ ϕ⁻¹ 4) ≡ 6    -- 12,528ms
  test₇ = refl

module Klein-test₁ where -- fast

  ϕ : coHom 1 KleinBottle → ℤ
  ϕ = fun (fst H¹-𝕂²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 1 KleinBottle
  ϕ⁻¹ = inv (fst H¹-𝕂²≅ℤ)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- <10ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 13ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 10ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 14ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 14ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ -3 +ₕ ϕ⁻¹ 4) ≡ 1    -- 38ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ -5 +ₕ ϕ⁻¹ -2) ≡ -7    -- 38ms
  test₇ = refl

  -- The example in the paper:
  test : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 2) ≡ 3     -- 22ms
  test = refl

module Klein-test₂ where
  ϕ : coHom 2 KleinBottle → Bool
  ϕ = fun (fst H²-𝕂²≅Bool)

  ϕ⁻¹ : Bool → coHom 2 KleinBottle
  ϕ⁻¹ = inv (fst H²-𝕂²≅Bool)

{-
  test₀ : ϕ (0ₕ _) ≡ true -- fails already here...
  test₀ = refl
-}

module RP2-test₂ where
  ϕ : coHom 2 RP² → Bool
  ϕ = fun (fst H²-RP²≅Bool)

  ϕ⁻¹ : Bool → coHom 2 RP²
  ϕ⁻¹ = inv (fst H²-RP²≅Bool)

  test₀ : ϕ (0ₕ _) ≡ true    -- 1,328ms (unlike for Klein, this works)
  test₀ = refl

{-
  test₁ : ϕ (ϕ⁻¹ true) ≡ true    -- nope
  test₁ = refl
-}

module CP2-test₂ where
  ϕ : coHom 2 CP² → ℤ
  ϕ = fun (fst H²CP²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 2 CP²
  ϕ⁻¹ = inv (fst H²CP²≅ℤ)

  -- For explicitly constructed elements g : H²CP², ϕ works well
  test₀ : ϕ (0ₕ _) ≡ 0    -- <10ms
  test₀ = refl

  generator : coHom 2 CP²
  generator = ∣ (λ { (inl x) → ∣ x ∣ ; (inr x) → 0ₖ _ ; (push a i) → p a i}) ∣₂
    where
    ind : (B : TotalHopf → Type) → ((x : _) → isOfHLevel 3 (B x)) → B (north , base) → (x : _) → B x
    ind =
      transport (λ i → (B : isoToPath IsoS³TotalHopf i → Type)
        → ((x : _) → isOfHLevel 3 (B x))
          → B (transp (λ j → isoToPath IsoS³TotalHopf (i ∨ ~ j)) i (north , base)) → (x : _) → B x)
          λ B hLev ind → sphereElim _ (λ _ → hLev _) ind

    p : (a : TotalHopf) → ∣ fst a ∣ ≡ 0ₖ 2
    p = ind _ (λ _ → isOfHLevelTrunc 4 _ _) refl

  test₁ : ϕ generator ≡ 1     -- 24ms
  test₁ = refl

  -- For _+ₕ_ too
  test₂ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0     -- 1,343ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 1) ≡ 2     -- 1,302ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 2 +ₕ ϕ⁻¹ 2) ≡ 4     -- 1,410ms
  test₄ = refl

module CP2-test₄ where
  ϕ : coHom 4 CP² → ℤ
  ϕ = fun (fst H⁴CP²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 4 CP²
  ϕ⁻¹ = inv (fst H⁴CP²≅ℤ)

{-
  test₀ : ϕ (0ₕ _) ≡ 0 -- fails already here...
  test₀ = refl
-}

max_stars_repo_name: lkstl/cubical

max_issues_repo_name: lkstl/cubical

max_forks_repo_name: lkstl/cubical


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Naturals
open import Numbers.Integers.Integers
open import Groups.Groups
open import Groups.Definition
open import Groups.Lemmas
open import Rings.Definition
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Fields.Fields
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import Sets.EquivalenceRelations

module Numbers.Rationals.Definition where

open import Fields.FieldOfFractions.Setoid ℤIntDom
open import Fields.FieldOfFractions.Addition ℤIntDom
open import Fields.FieldOfFractions.Multiplication ℤIntDom
open import Fields.FieldOfFractions.Ring ℤIntDom
open import Fields.FieldOfFractions.Field ℤIntDom
open import Fields.FieldOfFractions.Lemmas ℤIntDom
open import Fields.FieldOfFractions.Order ℤIntDom ℤOrderedRing

ℚ : Set
ℚ = fieldOfFractionsSet

ℚSetoid : Setoid ℚ
ℚSetoid = fieldOfFractionsSetoid

_+Q_ : ℚ → ℚ → ℚ
a +Q b = fieldOfFractionsPlus a b

_*Q_ : ℚ → ℚ → ℚ
a *Q b = fieldOfFractionsTimes a b

ℚRing : Ring fieldOfFractionsSetoid _+Q_ _*Q_
ℚRing = fieldOfFractionsRing

0Q : ℚ
0Q = Ring.0R ℚRing

injectionQ : ℤ → ℚ
injectionQ = embedIntoFieldOfFractions

injectionNQ : ℕ → ℚ
injectionNQ n = injectionQ (nonneg n)

injectionQInjective : Injection injectionQ
injectionQInjective {nonneg x} {nonneg .x} refl = refl
injectionQInjective {negSucc x} {negSucc .x} refl = refl

ℚField : Field ℚRing
ℚField = fieldOfFractions

_<Q_ : ℚ → ℚ → Set
_<Q_ = fieldOfFractionsComparison

_=Q_ : ℚ → ℚ → Set
a =Q b = Setoid._∼_ fieldOfFractionsSetoid a b

reflQ : {x : ℚ} → (x =Q x)
reflQ {x} = Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {x}

_≤Q_ : ℚ → ℚ → Set
a ≤Q b = (a <Q b) || (a =Q b)

negateQ : ℚ → ℚ
negateQ a = Group.inverse (Ring.additiveGroup ℚRing) a

_-Q_ : ℚ → ℚ → ℚ
a -Q b = a +Q negateQ b

a-A : (a : ℚ) → (a -Q a) =Q 0Q
a-A a = Group.invRight (Ring.additiveGroup ℚRing) {a}

ℚPartialOrder : SetoidPartialOrder fieldOfFractionsSetoid fieldOfFractionsComparison
ℚPartialOrder = fieldOfFractionsOrder

ℚTotalOrder : SetoidTotalOrder fieldOfFractionsOrder
ℚTotalOrder = fieldOfFractionsTotalOrder

ℚOrderInherited : (a b : ℤ) → a <Z b → injectionQ a <Q injectionQ b
ℚOrderInherited a b a<b = fieldOfFractionsOrderInherited a<b

open SetoidTotalOrder fieldOfFractionsTotalOrder
open SetoidPartialOrder partial
open Setoid fieldOfFractionsSetoid

negateQWellDefined : (a b : ℚ) → (a =Q b) → (negateQ a) =Q (negateQ b)
negateQWellDefined a b a=b = inverseWellDefined (Ring.additiveGroup ℚRing) {a} {b} a=b

ℚPOrdered : PartiallyOrderedRing ℚRing partial
ℚPOrdered = fieldOfFractionsPOrderedRing

ℚOrdered : TotallyOrderedRing ℚPOrdered
ℚOrdered = fieldOfFractionsOrderedRing


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax PropLog | PR

type
  * : 0-ary

term
  false : * | ⊥
  or    : *  *  ->  * | _∨_ l20
  true  : * | ⊤
  and   : *  *  ->  * | _∧_ l30
  not   : *  ->  * | ¬_ r50

theory
  (⊥U∨ᴸ) a |> or (false, a) = a
  (⊥U∨ᴿ) a |> or (a, false) = a
  (∨A) a b c |> or (or(a, b), c) = or (a, or(b, c))
  (∨C) a b |> or(a, b) = or(b, a)
  (⊤U∧ᴸ) a |> and (true, a) = a
  (⊤U∧ᴿ) a |> and (a, true) = a
  (∧A) a b c |> and (and(a, b), c) = and (a, and(b, c))
  (∧D∨ᴸ) a b c |> and (a, or (b, c)) = or (and(a, b), and(a, c))
  (∧D∨ᴿ) a b c |> and (or (a, b), c) = or (and(a, c), and(b, c))
  (⊥X∧ᴸ) a |> and (false, a) = false
  (⊥X∧ᴿ) a |> and (a, false) = false
  (¬N∨ᴸ) a |> or (not (a), a) = false
  (¬N∨ᴿ) a |> or (a, not (a)) = false
  (∧C) a b |> and(a, b) = and(b, a)
  (∨I) a |> or(a, a) = a
  (∧I) a |> and(a, a) = a
  (¬²) a |> not(not (a)) = a
  (∨D∧ᴸ) a b c |> or (a, and (b, c)) = and (or(a, b), or(a, c))
  (∨D∧ᴿ) a b c |> or (and (a, b), c) = and (or(a, c), or(b, c))
  (∨B∧ᴸ) a b |> or (and (a, b), a) = a
  (∨B∧ᴿ) a b |> or (a, and (a, b)) = a
  (∧B∨ᴸ) a b |> and (or (a, b), a) = a
  (∧B∨ᴿ) a b |> and (a, or (a, b)) = a
  (⊤X∨ᴸ) a |> or (true, a) = true
  (⊤X∨ᴿ) a |> or (a, true) = true
  (¬N∧ᴸ) a |> and (not (a), a) = false
  (¬N∧ᴿ) a |> and (a, not (a)) = false
  (DM∧) a b |> not (and (a, b)) = or  (not(a), not(b))
  (DM∨) a b |> not (or  (a, b)) = and (not(a), not(b))
-}

module PropLog.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import PropLog.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

-- Inductive term declaration
module PR:Terms (𝔛 : Familyₛ) where

  data PR : Familyₛ where
    var  : ℐ ⇾̣ PR
    mvar : 𝔛 α Π → Sub PR Π Γ → PR α Γ

    ⊥   : PR * Γ
    _∨_ : PR * Γ → PR * Γ → PR * Γ
    ⊤   : PR * Γ
    _∧_ : PR * Γ → PR * Γ → PR * Γ
    ¬_  : PR * Γ → PR * Γ

  infixl 20 _∨_
  infixl 30 _∧_
  infixr 50 ¬_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  PRᵃ : MetaAlg PR
  PRᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (falseₒ ⋮ _)     → ⊥
      (orₒ    ⋮ a , b) → _∨_ a b
      (trueₒ  ⋮ _)     → ⊤
      (andₒ   ⋮ a , b) → _∧_ a b
      (notₒ   ⋮ a)     → ¬_  a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module PRᵃ = MetaAlg PRᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : PR ⇾̣ 𝒜
    𝕊 : Sub PR Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞  ⊥        = 𝑎𝑙𝑔 (falseₒ ⋮ tt)
    𝕤𝕖𝕞 (_∨_ a b) = 𝑎𝑙𝑔 (orₒ    ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  ⊤        = 𝑎𝑙𝑔 (trueₒ  ⋮ tt)
    𝕤𝕖𝕞 (_∧_ a b) = 𝑎𝑙𝑔 (andₒ   ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (¬_  a)   = 𝑎𝑙𝑔 (notₒ   ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ PRᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ PR α Γ) → 𝕤𝕖𝕞 (PRᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (falseₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (orₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (trueₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (andₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (notₒ   ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ PR ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : PR ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ PRᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : PR α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub PR Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! ⊥ = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_∨_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! ⊤ = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_∧_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (¬_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
PR:Syn : Syntax
PR:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = PR:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open PR:Terms 𝔛 in record
    { ⊥ = PR ⋉ PRᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax PR:Syn public
open PR:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands PRᵃ public
open import SOAS.Metatheory PR:Syn public

-- Derived operations
_⟹_ : PR 𝔛 * Γ → PR 𝔛 * Γ → PR 𝔛 * Γ
p ⟹ q = ¬ p ∨ q

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Andreas, 2015-11-18 Fixing de Bruijn indices in debug print for with.

{-# OPTIONS -v tc.with.top:25 #-}  -- KEEP!

postulate
  Trash A : Set
  P : A → Set
  provokeError : Trash

-- The trash arguments should not show up in the debug printing!
-- If they do, permutations or de Bruijn indices are messed up,
-- or the debug messages are printed in the wrong context.
test : (trash1 : Trash) (b : A) (trash2 : Trash) (f : ∀ x → P x) (trash3 : Trash) → Set
test trash1 b trash2 f trash3 with f b
... | p = provokeError

-- EXPECTED:
-- ...
-- vs     = [f b]
-- as     = [P b]
-- ...
--     with arguments [f b]
--              types [P b]
-- ...
-- checkWithFunction
-- ...
--   as     = [P b]
--   vs     = [f b]
-- ...
--
-- and then a type error message.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category

module Categories.Category.Complete.Properties.Construction {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Product using (∃₂; _,_; -,_)

open import Categories.Category.Complete
open import Categories.Diagram.Equalizer C
open import Categories.Diagram.Limit as Lim
open import Categories.Object.Product.Indexed C
open import Categories.Functor

import Categories.Category.Construction.Cones as Co
import Categories.Morphism.Reasoning as MR

private
  variable
    o′ ℓ′ e′ o″ ℓ″ e″ : Level
  module C = Category C

module _ (prods : AllProductsOf (o′ ⊔ ℓ′)) (equalizer : ∀ {A B} (f g : A C.⇒ B) → Equalizer f g) where
  private
    module Prods {I} (P : I → C.Obj) = IndexedProductOf (prods P)
    open C.HomReasoning

    module _ {J : Category o′ ℓ′ e′} (F : Functor J C) where
      private
        module J  = Category J
        open Functor F
        open MR C
        module OP = Prods {Lift ℓ′ J.Obj} (λ j → F₀ (lower j))
        module MP = Prods {∃₂ J._⇒_} (λ { (_ , B , _) → F₀ B })

      src : C.Obj
      src = OP.X

      dst : C.Obj
      dst = MP.X

      ϕ⇒ : (i : ∃₂ J._⇒_) → let (_ , B , _) = i in src C.⇒ F₀ B
      ϕ⇒ (_ , B , _) = OP.π (lift B)

      ϕ : src C.⇒ dst
      ϕ = MP.⟨ ϕ⇒ ⟩

      ψ⇒ : (i : ∃₂ J._⇒_) → let (_ , B , _) = i in src C.⇒ F₀ B
      ψ⇒ (A , B , f) = F₁ f C.∘ OP.π (lift A)

      ψ : src C.⇒ dst
      ψ = MP.⟨ ψ⇒ ⟩

      module eq = Equalizer (equalizer ϕ ψ)

      ⊤ : Co.Cone F
      ⊤ = record
        { N    = eq.obj
        ; apex = record
          { ψ       = λ X → OP.π (lift X) C.∘ eq.arr
          ; commute = λ {X Y} f → begin
            F₁ f C.∘ OP.π (lift X) C.∘ eq.arr ≈˘⟨ pushˡ (MP.commute ψ⇒ _) ⟩
            (MP.π (-, -, f) C.∘ ψ) C.∘ eq.arr ≈˘⟨ pushʳ eq.equality ⟩
            MP.π (-, -, f) C.∘ ϕ C.∘ eq.arr   ≈⟨ pullˡ (MP.commute ϕ⇒ _ ) ⟩
            OP.π (lift Y) C.∘ eq.arr          ∎
          }
        }

      module _ {K : Co.Cone F} where
        private
          module K = Co.Cone F K

        K⇒ : K.N C.⇒ src
        K⇒ = OP.⟨ (λ j → K.ψ (lower j)) ⟩

        Keq : (i : ∃₂ J._⇒_) → ϕ⇒ i C.∘ K⇒ C.≈ ψ⇒ i C.∘ K⇒
        Keq i@(A , B , f) = begin
          ϕ⇒ i C.∘ K⇒    ≈⟨ OP.commute _ _ ⟩
          K.ψ B          ≈˘⟨ K.commute _ ⟩
          F₁ f C.∘ K.ψ A ≈˘⟨ pullʳ (OP.commute _ _) ⟩
          ψ⇒ i C.∘ K⇒    ∎

        !-eq : ϕ C.∘ K⇒ C.≈ ψ C.∘ K⇒
        !-eq = begin
          ϕ C.∘ K⇒                   ≈⟨ MP.⟨⟩∘ _ _ ⟩
          MP.⟨ (λ i → ϕ⇒ i C.∘ K⇒) ⟩ ≈⟨ MP.⟨⟩-cong _ _ Keq ⟩
          MP.⟨ (λ i → ψ⇒ i C.∘ K⇒) ⟩ ≈˘⟨ MP.⟨⟩∘ _ _ ⟩
          ψ C.∘ K⇒                   ∎

        ! : Co.Cones F [ K , ⊤ ]
        ! = record
          { arr     = eq.equalize {h = K⇒} !-eq
          ; commute = λ {j} → begin
            (OP.π (lift j) C.∘ eq.arr) C.∘ eq.equalize !-eq ≈˘⟨ pushʳ eq.universal ⟩
            OP.π (lift j) C.∘ K⇒                            ≈⟨ OP.commute _ _ ⟩
            K.ψ j                                           ∎
          }

        !-unique : (f : Co.Cones F [ K , ⊤ ]) → Co.Cones F [ ! ≈ f ]
        !-unique f = ⟺ (eq.unique eq)
          where module f = Co.Cone⇒ F f
                eq : K⇒ C.≈ eq.arr C.∘ f.arr
                eq = OP.unique′ _ _ λ i → begin
                  OP.π i C.∘ K⇒                 ≈⟨ OP.commute _ _ ⟩
                  K.ψ (lower i)                 ≈˘⟨ f.commute ⟩
                  (OP.π i C.∘ eq.arr) C.∘ f.arr ≈⟨ C.assoc ⟩
                  OP.π i C.∘ eq.arr C.∘ f.arr   ∎

      complete : Limit F
      complete = record
        { terminal = record
          { ⊤        = ⊤
          ; ⊤-is-terminal = record
            { !        = !
            ; !-unique = !-unique
            }
          }
        }

  AllProducts×Equalizer⇒Complete : Complete o′ ℓ′ e′ C
  AllProducts×Equalizer⇒Complete = complete

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K #-}
module Leftovers.Utils where

open import Data.String using (String)
open import Data.List as List

-- open import Reflection
open import Leftovers.Monad
open import Reflection.Term
open import Reflection.Pattern as P
-- open import Reflection.TypeChecking.Monad.Instances
open import Data.Nat
open import Data.Product
open import Data.Unit

open import Function using (_$_)

import Data.List.Categorical
open import Level
open Data.List.Categorical.TraversableM {m = Level.zero} leftoversMonad

case_of_ : ∀ {A B : Set} → A → (A → B) → B
case x of f = f x

λv_↦_  λh_↦_ : String → Term → Term
λv x ↦ body  = lam visible (abs x body)
λh x ↦ body  = lam hidden (abs x body)

identity : ∀ {ℓ} { X : Set ℓ} → X → X
identity x = x

the : ∀ {ℓ} → (T : Set ℓ) → T → T
the _ = identity

_⦂_ : Term → Type → Term
t ⦂ T = def (quote the) (vArg T ∷ vArg t ∷ [])

app : Term → Term → Term
app f x = def (quote _$_) (vArg f ∷ vArg x ∷ [])

returnTypeFor : Type → Term → Leftovers Type
returnTypeFor (pi (arg _ dom) cod) x = do
  debugPrint "returnTypeFor" 2 (strErr "Checking pattern " ∷ termErr x ∷ strErr "  against type  " ∷ termErr dom ∷ [])
  checkType x dom
  pure (app (lam visible cod) x)
returnTypeFor t x = do
  ldom ← freshMeta (quoteTerm Level)
  lcod ← freshMeta (quoteTerm Level)
  dom ← freshMeta (sort (set ldom))
  cod ← extendContext (vArg dom) (freshMeta (sort (set lcod)))
  unify t (pi (vArg dom) (abs "x" cod))
  pure (app (lam visible (abs "x" cod)) x)

--Try an action (usually unification) but continue without it
-- if it fails
try : Leftovers ⊤ → Leftovers ⊤
try x = catchLeftovers x (pure tt)

tryUnify : Term → Term → Leftovers ⊤
tryUnify x y = try (unify x y)

{- Syntactic sugar for trying a computation, if it fails then try the other one -}
-- try-fun : ∀ {a} {A : Set a} → Leftovers A → Leftovers A → Leftovers A
-- try-fun = catchLeftovers

-- syntax try-fun t f = try t or-else f

constructors : Definition → List Name
constructors (data-type pars cs) = cs
constructors _ = []

import Reflection.Show

record CtorArg : Set where
  constructor mkCtorArg
  field
    pat : Arg Pattern
    term : Arg Term
    type : Arg Type

-- Given a name, get its type
-- and generate fresh metas for each argument
-- e.g. turn (a -> b -> c -> d) into [_ , _ , _]
fully-applied-pattern : Name → Leftovers (List (CtorArg))
fully-applied-pattern nm =
  do
    nmType ← getType nm
    -- debugPrint "full-app" 2 (strErr "fullApp " ∷ nameErr nm ∷ termErr nmType ∷ [])
    pure (full-app-type nmType 0)
  where
    full-app-type : Type → ℕ → List (CtorArg)
    full-app-type (pi (arg info dom) (abs s x)) pos =
      (mkCtorArg
        (arg info (P.var pos))
        (arg info (var pos []))
        (arg info unknown)) ∷ full-app-type x (1 + pos)
      -- ((arg info (P.var pos) , arg info (var pos [])) ∷ full-app-type x (1 + pos))
    full-app-type t pos = []

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
open import Nat
open import Prelude

open import contexts
open import core
open import dynamics-core

open import lemmas-gcomplete

open import disjointness
open import dom-eq
open import holes-disjoint-checks
open import lemmas-disjointness
open import lemmas-freshness

open import finality
open import focus-formation
open import ground-decidable
open import grounding

open import lemmas-subst-ta
open import htype-decidable
open import lemmas-consistency
open import lemmas-ground
open import lemmas-matching
open import synth-unicity

open import elaborability
open import elaboration-generality
open import elaboration-unicity
open import type-assignment-unicity
open import typed-elaboration

open import canonical-boxed-forms
open import canonical-indeterminate-forms
open import canonical-value-forms

open import lemmas-progress-checks
open import preservation
open import progress
open import progress-checks

open import cast-inert
open import complete-elaboration
open import complete-preservation
open import complete-progress
open import lemmas-complete

open import contraction
open import exchange
open import weakening

open import binders-disjoint-checks

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

module lib.PathSeq where

open import lib.path-seq.Ap public
open import lib.path-seq.Concat public
open import lib.path-seq.Inversion public
open import lib.path-seq.Reasoning public
open import lib.path-seq.Rotations public
open import lib.path-seq.Split public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.IdNat {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Twk
open import Definition.Typed.EqualityRelation
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
import Definition.LogicalRelation.Weakening as Lwk
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Weakening
-- open import Definition.LogicalRelation.Substitution.Introductions.Nat
open import Definition.LogicalRelation.Substitution.Introductions.Empty
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Idlemmas
open import Definition.LogicalRelation.Substitution.Introductions.IdUniv
open import Definition.LogicalRelation.Substitution.MaybeEmbed
-- open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Product
open import Tools.Empty
import Tools.Unit as TU
import Tools.PropositionalEquality as PE
import Data.Nat as Nat

[ℕ] : ∀ {Γ l} → ⊢ Γ → Γ ⊩⟨ l ⟩ ℕ ^ [ ! , ι ⁰ ]
[ℕ] ⊢Γ = ℕᵣ (idRed:*: (univ (ℕⱼ ⊢Γ)))

[Id]ℕ : ∀ {Γ l t u}
  (⊢Γ : ⊢ Γ)
  ([t] : Γ ⊩ℕ t ∷ℕ)
  ([u] : Γ ⊩ℕ u ∷ℕ)
  → Γ ⊩⟨ l ⟩ Id ℕ t u ^ [ % , ι ⁰ ]
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .(suc m′) [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m (sucᵣ {m′} [m′])) (ℕₜ .(suc n′) [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (sucᵣ {n′} [n′])) =
  let [Idmn] = [Id]ℕ ⊢Γ [m′] [n′]
      ⊢m′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [m′]
      ⊢n′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [n′]
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ ⇨∷* IdℕSRed*Term′ ⊢m′ℕ ⊢uℕ ⊢nℕ du)
        ⇨∷* (Id-ℕ-SS ⊢m′ℕ ⊢n′ℕ ⇨ id (Idⱼ (ℕⱼ ⊢Γ) ⊢m′ℕ ⊢n′ℕ)))
  in proj₁ (redSubst* nfId [Idmn])
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .(suc m′) [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m (sucᵣ {m′} [m′])) (ℕₜ .zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ) =
  let ⊢m′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [m′]
      nfId = (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (IdℕSRed*Term′ ⊢m′ℕ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-S0 ⊢m′ℕ ⇨ id (Emptyⱼ ⊢Γ)))
  in Emptyᵣ [[ univ (Idⱼ (ℕⱼ ⊢Γ) ⊢tℕ ⊢uℕ) , univ (Emptyⱼ ⊢Γ) , univ⇒* nfId ]]
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .(suc m′) [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m (sucᵣ {m′} [m′])) (ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ nen _ n∼n))) =
  let ⊢m′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [m′]
      nfId = (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ) ⇨∷* IdℕSRed*Term′ ⊢m′ℕ ⊢uℕ ⊢nℕ du
      m′≡m′ = escapeTermEq ([ℕ] {l = ι ⁰} ⊢Γ) (reflEqTerm ([ℕ] {l = ι ⁰} ⊢Γ) [m′])
  in ne′ (Id ℕ (suc m′) n) [[ univ (Idⱼ (ℕⱼ ⊢Γ) ⊢tℕ ⊢uℕ) , univ (Idⱼ (ℕⱼ ⊢Γ) ⊢mℕ ⊢nℕ) , univ⇒* nfId ]] (IdℕSₙ nen) (~-IdℕS ⊢Γ m′≡m′ n∼n)
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .zero [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m zeroᵣ) (ℕₜ .(suc n′) [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (sucᵣ {n′} [n′])) =
  let ⊢n′ = escapeTerm ([ℕ] {l = ι ⁰} ⊢Γ) [n′]
      nfId = (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (Idℕ0Red*Term′ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-0S ⊢n′ ⇨ id (Emptyⱼ ⊢Γ)))
  in Emptyᵣ [[ univ (Idⱼ (ℕⱼ ⊢Γ) ⊢tℕ ⊢uℕ) , univ (Emptyⱼ ⊢Γ) , univ⇒* nfId ]]
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .zero [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m zeroᵣ) (ℕₜ .zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ) =
  let nfId = (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (Idℕ0Red*Term′ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-00 ⊢Γ ⇨ id (Unitⱼ ⊢Γ)))
  in proj₁ (redSubst* (univ⇒* nfId) (maybeEmb″ (UnitType ⊢Γ)))
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ .zero [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m zeroᵣ) (ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ nen _ n∼n))) =
  let nfId = (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ) ⇨∷* Idℕ0Red*Term′ ⊢uℕ ⊢nℕ du
  in ne′ (Id ℕ zero n) [[ univ (Idⱼ (ℕⱼ ⊢Γ) ⊢tℕ ⊢uℕ) , univ (Idⱼ (ℕⱼ ⊢Γ) (zeroⱼ ⊢Γ) ⊢nℕ) , univ⇒* nfId ]] (Idℕ0ₙ nen) (~-Idℕ0 ⊢Γ n∼n)
[Id]ℕ {Γ} {l} {t} {u} ⊢Γ (ℕₜ m [[ ⊢tℕ , ⊢mℕ , dt ]] m≡m (ne (neNfₜ nem _ m∼m))) [u] =
  let
    ⊢u = escapeTerm ([ℕ] {l = ι ⁰} ⊢Γ) [u]
    u≡u = escapeTermEq {l = ι ⁰} ([ℕ] ⊢Γ) (reflEqTerm ([ℕ] {l = ι ⁰} ⊢Γ) [u])
  in ne′ (Id ℕ m u) [[ univ (Idⱼ (ℕⱼ ⊢Γ) ⊢tℕ ⊢u) , univ (Idⱼ (ℕⱼ ⊢Γ) ⊢mℕ ⊢u) ,
    univ⇒* (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢u) ]] (Idℕₙ nem) (~-Idℕ ⊢Γ m∼m u≡u)

escapeEqℕ₁  : ∀ {Γ m n} → Γ ⊩ℕ m ≡ n ∷ℕ → Γ ⊢ m ∷ ℕ ^ [ ! , ι ⁰ ]
escapeEqℕ₁ (ℕₜ₌ k k′ [[ ⊢t , ⊢u , d ]] d′ k≡k′ prop) = ⊢t

escapeEqℕ₂  : ∀ {Γ m n} → Γ ⊩ℕ m ≡ n ∷ℕ → Γ ⊢ n ∷ ℕ ^ [ ! , ι ⁰ ]
escapeEqℕ₂ (ℕₜ₌ k k′ d [[ ⊢t , ⊢u , d' ]] k≡k′ prop) = ⊢t

irrelevanceEqTermℕ : ∀ {Γ A t t′ u u′ r ll l}
                        (eqt : t PE.≡ t′) (equ : u PE.≡ u′)
                        (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ])
                      → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ r , ll ] / p → Γ ⊩⟨ l ⟩ t′ ≡ u′ ∷ A ^ [ r , ll ] / p
irrelevanceEqTermℕ PE.refl PE.refl p t≡u = t≡u

[IdExt]ℕ : ∀ {Γ l t u v w}
  (⊢Γ : ⊢ Γ)
  ([t] : Γ ⊩ℕ t ∷ℕ)
  ([u] : Γ ⊩ℕ u ∷ℕ)
  ([v] : Γ ⊩ℕ v ∷ℕ)
  ([w] : Γ ⊩ℕ w ∷ℕ)
  ([t≡v] : Γ ⊩ℕ t ≡ v ∷ℕ)
  ([u≡w] : Γ ⊩ℕ u ≡ w ∷ℕ)
  →  Γ ⊩⟨ l ⟩ Id ℕ t u ≡ Id ℕ v w ^ [ % , ι ⁰ ] / [Id]ℕ ⊢Γ [t] [u]

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ
            (ℕₜ .(suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ {n} [t']))
            (ℕₜ .(suc _) [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (sucᵣ {n₂} [u']))
            (ℕₜ .(suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ {n₁} [v']))
            (ℕₜ .(suc _) [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (sucᵣ {n₃} [w']))
            (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ [t≡v']))
            (ℕₜ₌ .(suc _) .(suc _) d₅ d′₁ k≡k′₁ (sucᵣ [u≡w'])) =
  let t≡t' = suc-PE-injectivity (whrDet*Term (dt , sucₙ) (redₜ d₄ , sucₙ))
      u≡u' = suc-PE-injectivity (whrDet*Term (du , sucₙ) (redₜ d₅ , sucₙ))
      v≡v' = suc-PE-injectivity (whrDet*Term (dv , sucₙ) (redₜ d′ , sucₙ))
      w≡w' = suc-PE-injectivity (whrDet*Term (dw , sucₙ) (redₜ d′₁ , sucₙ))
      [t] = ℕₜ (suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ [t'])
      [u] = ℕₜ (suc _) [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (sucᵣ [u'])
      [v] = ℕₜ (suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ [v'])
      [w] = ℕₜ (suc _) [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (sucᵣ [w'])
      [Idmn] = [IdExt]ℕ {l = l} ⊢Γ [t'] [u'] [v'] [w'] (irrelevanceEqTermℕ {l = l} (PE.sym t≡t') (PE.sym v≡v') ([ℕ] ⊢Γ) [t≡v'])
                                               (irrelevanceEqTermℕ {l = l} (PE.sym u≡u') (PE.sym w≡w') ([ℕ] ⊢Γ) [u≡w'])
      ⊢t′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [t']
      ⊢u′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [u']
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ ⇨∷* IdℕSRed*Term′ ⊢t′ℕ ⊢uℕ ⊢nℕ du)
        ⇨∷* (Id-ℕ-SS ⊢t′ℕ ⊢u′ℕ ⇨ id (Idⱼ (ℕⱼ ⊢Γ) ⊢t′ℕ ⊢u′ℕ)))
      ⊢v′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [v']
      ⊢w′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [w']
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ ⇨∷* IdℕSRed*Term′ ⊢v′ℕ ⊢wℕ ⊢pℕ dw)
        ⇨∷* (Id-ℕ-SS ⊢v′ℕ ⊢w′ℕ ⇨ id (Idⱼ (ℕⱼ ⊢Γ) ⊢v′ℕ ⊢w′ℕ)))
      [IdA] , [IdA≡ℕ] = redSubst* {l = l} nfId ([Id]ℕ ⊢Γ [t'] [u'])
      [IdB] , [IdB≡ℕ] = redSubst* {l = l} nfId' ([Id]ℕ ⊢Γ [v'] [w'])
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Id ℕ n n₂} {l = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Id ℕ n₁ n₃} {l = l} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
  in transEq {A = Id ℕ t u} {B = Id ℕ n n₂} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) ([Id]ℕ ⊢Γ [t'] [u']) ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′
                  (transEq {A = Id ℕ n n₂} {B = Id ℕ n₁ n₃} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t'] [u']) ([Id]ℕ ⊢Γ [v'] [w']) ([Id]ℕ ⊢Γ [v] [w])
                                   [Idmn] (symEq {A = Id ℕ v w} {B = Id ℕ n₁ n₃} ([Id]ℕ ⊢Γ [v] [w]) ([Id]ℕ ⊢Γ [v'] [w']) [IdB≡ℕ]′))

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ
  (ℕₜ .(suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ {n} [t']))
  (ℕₜ .zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ)
  (ℕₜ .(suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ {m} [v']))
  (ℕₜ .zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ)
  (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x))
  (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) =
  let [t] = ℕₜ (suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ [t'])
      [u] = ℕₜ zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ
      [v] = ℕₜ (suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ [v'])
      [w] = ℕₜ zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ
      ⊢t′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [t']
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (IdℕSRed*Term′ ⊢t′ℕ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-S0 ⊢t′ℕ ⇨ id (Emptyⱼ ⊢Γ))))
      ⊢v′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [v']
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ)
        ⇨∷* (IdℕSRed*Term′ ⊢v′ℕ ⊢wℕ ⊢pℕ dw ⇨∷* (Id-ℕ-S0 ⊢v′ℕ ⇨ id (Emptyⱼ ⊢Γ))))
      [Empty] = Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Γ)))
      [IdA] , [IdA≡ℕ] = redSubst* {l = l} nfId [Empty]
      [IdB] , [IdB≡ℕ] = redSubst* {l = l} nfId' [Empty]
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Empty _} {l = l} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Empty _} {l = l} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
  in transEq {A = Id ℕ t u} {B = Empty _} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) [Empty] ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′  (symEq {A = Id ℕ v w} {B = Empty _} {l = l} {l′ = l} ([Id]ℕ ⊢Γ [v] [w]) [Empty] [IdB≡ℕ]′)

[IdExt]ℕ {Γ} {l} {u} {t} {w} {v} ⊢Γ
  (ℕₜ .zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ)
  (ℕₜ .(suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ {n} [t']))
  (ℕₜ .zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ)
  (ℕₜ .(suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ {m} [v']))
  (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ)
  (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) =
  let [t] = ℕₜ (suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ [t'])
      [u] = ℕₜ zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ
      [v] = ℕₜ (suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ [v'])
      [w] = ℕₜ zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ
      ⊢t′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [t']
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (IdℕSRed*Term′ ⊢t′ℕ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-S0 ⊢t′ℕ ⇨ id (Emptyⱼ ⊢Γ))))
      ⊢v′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [v']
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ)
        ⇨∷* (IdℕSRed*Term′ ⊢v′ℕ ⊢wℕ ⊢pℕ dw ⇨∷* (Id-ℕ-S0 ⊢v′ℕ ⇨ id (Emptyⱼ ⊢Γ))))
      [Empty] = Emptyᵣ (idRed:*: (univ (Emptyⱼ ⊢Γ)))
      [IdA] , [IdA≡ℕ] = redSubst* {l = l} nfId [Empty]
      [IdB] , [IdB≡ℕ] = redSubst* {l = l} nfId' [Empty]
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Empty _} {l = l} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Empty _} {l = l} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
   in transEq {A = Id ℕ u t} {B = Empty _} {C = Id ℕ w v} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [u] [t]) [Empty] ([Id]ℕ ⊢Γ [w] [v])
                  [IdB≡ℕ]′  (symEq {A = Id ℕ w v} {B = Empty _} {l = l} {l′ = l} ([Id]ℕ ⊢Γ [w] [v]) [Empty] [IdA≡ℕ]′)

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ (ℕₜ .zero [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ zeroᵣ) (ℕₜ .zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ)
            (ℕₜ .zero [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ zeroᵣ) (ℕₜ .zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ)
            (ℕₜ₌ .zero .zero d₄ d′ k≡k′ zeroᵣ) (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) =
  let [t] = ℕₜ zero [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ zeroᵣ
      [u] = ℕₜ zero [[ ⊢uℕ , ⊢nℕ , du ]] n≡n zeroᵣ
      [v] = ℕₜ zero [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ zeroᵣ
      [w] = ℕₜ zero [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ zeroᵣ
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ)
        ⇨∷* (Idℕ0Red*Term′ ⊢uℕ ⊢nℕ du ⇨∷* (Id-ℕ-00 ⊢Γ ⇨ id (Unitⱼ ⊢Γ))))
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ)
        ⇨∷* (Idℕ0Red*Term′ ⊢wℕ ⊢pℕ dw ⇨∷* (Id-ℕ-00 ⊢Γ ⇨ id (Unitⱼ ⊢Γ))))
      [Unit] = UnitType ⊢Γ
      [IdA] , [IdA≡ℕ] = redSubst* nfId [Unit]
      [IdB] , [IdB≡ℕ] = redSubst* nfId' [Unit]
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Unit} {l = ι ⁰} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Unit} {l = ι ⁰} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
  in transEq {A = Id ℕ t u} {B = Unit} {C = Id ℕ v w} {l = l} {l′ = ι ⁰} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) [Unit] ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′  (symEq {A = Id ℕ v w} {B = Unit} {l = l} {l′ = ι ⁰} ([Id]ℕ ⊢Γ [v] [w]) [Unit] [IdB≡ℕ]′)

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ (ℕₜ .(suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ {t'} [t'])) (ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ neKu ⊢ku k≡ku)))
         (ℕₜ .(suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ {v'} [v'])) (ℕₜ n₃ [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw)))
         (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ [t≡v'])) (ℕₜ₌ k₁ k′₁ d₅ d′₁ k≡k′₁ (ne (neNfₜ₌ neK neM K~M))) =
  let t≡t' = suc-PE-injectivity (whrDet*Term (dt , sucₙ) (redₜ d₄ , sucₙ))
      v≡v' = suc-PE-injectivity (whrDet*Term (dv , sucₙ) (redₜ d′ , sucₙ))
      u≡u' = whrDet*Term (du , ne neKu) (redₜ d₅ , ne neK)
      w≡w' = whrDet*Term (dw , ne neKw) (redₜ d′₁ , ne neM)
      [t] = ℕₜ (suc _) [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (sucᵣ [t'])
      [u] = ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ neKu ⊢ku k≡ku))
      [v] = ℕₜ (suc _) [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (sucᵣ [v'])
      [w] = ℕₜ n₃ [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw))
      [suct'] = ℕₜ (suc t') (idRedTerm:*: ⊢mℕ) n≡n₁ (sucᵣ [t'])
      [n] = ℕₜ n (idRedTerm:*: ⊢nℕ) n≡n (ne (neNfₜ neKu ⊢ku k≡ku))
      [sucv'] = ℕₜ (suc v') (idRedTerm:*: ⊢oℕ) n≡n₂ (sucᵣ [v'])
      [n₃] = ℕₜ n₃ (idRedTerm:*: ⊢pℕ) n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw))
      ⊢t′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [t']
      ⊢v′ℕ = escapeTerm {l = ι ⁰} ([ℕ] ⊢Γ) [v']
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ) ⇨∷* IdℕSRed*Term′ ⊢t′ℕ ⊢uℕ ⊢nℕ du)
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ) ⇨∷* IdℕSRed*Term′ ⊢v′ℕ ⊢wℕ ⊢pℕ dw)
      [IdA] , [IdA≡ℕ] = redSubst* nfId ([Id]ℕ ⊢Γ [suct'] [n])
      [IdB] , [IdB≡ℕ] = redSubst* nfId' ([Id]ℕ ⊢Γ [sucv'] [n₃])
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Id ℕ (suc t') n} {l = ι ⁰} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Id ℕ (suc v') n₃} {l = ι ⁰} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
      [Idneutral] : Γ ⊩⟨ l ⟩ Id ℕ (suc t') n ≡ Id ℕ (suc v') n₃ ^ [ % , ι ⁰ ] / ([Id]ℕ ⊢Γ [suct'] [n])
      [Idneutral] = ne₌ (Id ℕ (suc v') n₃) (idRed:*: (univ (Idⱼ (ℕⱼ ⊢Γ) ⊢oℕ ⊢pℕ))) (IdℕSₙ neKw)
                (~-IdℕS ⊢Γ (let X = escapeTermEq {l = l} ([ℕ] ⊢Γ) [t≡v'] in
                                PE.subst (λ X → Γ ⊢ X ≅ _ ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym t≡t') (PE.subst (λ X → Γ ⊢ _ ≅ X ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym v≡v') X) )
                           (PE.subst (λ X → Γ ⊢ X ~ _ ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym u≡u') (PE.subst (λ X → Γ ⊢ k₁ ~ X ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym w≡w') K~M)))
  in transEq {A = Id ℕ t u} {B = Id ℕ (suc t') n} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) ([Id]ℕ ⊢Γ [suct'] [n]) ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′
                  (transEq {A = Id ℕ (suc t') n} {B = Id ℕ (suc v') n₃} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [suct'] [n]) ([Id]ℕ ⊢Γ [sucv'] [n₃]) ([Id]ℕ ⊢Γ [v] [w])
                                   [Idneutral] (symEq {A = Id ℕ v w} {B = Id ℕ (suc v') n₃} {l = l} {l′ = l} ([Id]ℕ ⊢Γ [v] [w]) ([Id]ℕ ⊢Γ [sucv'] [n₃]) [IdB≡ℕ]′))

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ (ℕₜ n₁ [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (ne (neNfₜ neKt ⊢kt k≡kt))) [u] (ℕₜ n₂ [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (ne (neNfₜ neKv ⊢kv k≡kv))) [w]
            (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM K~M))) [u=w] =
  let [t] = ℕₜ n₁ [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ (ne (neNfₜ neKt ⊢kt k≡kt))
      [v] = ℕₜ n₂ [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ (ne (neNfₜ neKv ⊢kv k≡kv))
      ⊢u = escapeTerm ([ℕ] {l = ι ⁰} ⊢Γ) [u]
      ⊢w = escapeTerm ([ℕ] {l = ι ⁰} ⊢Γ) [w]
      u≡w = escapeTermEq {l = ι ⁰} ([ℕ] ⊢Γ) [u=w]
      t≡t' = whrDet*Term (dt , ne neKt) (redₜ d₄ , ne neK)
      v≡v' = whrDet*Term (dv , ne neKv) (redₜ d′ , ne neM)
      nfId = univ⇒* (IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢u)
      nfId' = univ⇒* (IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢w)
      [n₁] = ℕₜ n₁ (idRedTerm:*: ⊢mℕ) n≡n₁ (ne (neNfₜ neKt ⊢kt k≡kt))
      [n₂] = ℕₜ n₂ (idRedTerm:*: ⊢oℕ) n≡n₂ (ne (neNfₜ neKv ⊢kv k≡kv))
      [IdA] , [IdA≡ℕ] = redSubst* nfId ([Id]ℕ ⊢Γ [n₁] [u])
      [IdB] , [IdB≡ℕ] = redSubst* nfId' ([Id]ℕ ⊢Γ [n₂] [w])
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Id ℕ n₁ u} {l = ι ⁰} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Id ℕ n₂ w} {l = ι ⁰} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
      [Idneutral] : Γ ⊩⟨ l ⟩ Id ℕ n₁ u ≡ Id ℕ n₂ w ^ [ % , ι ⁰ ] / ([Id]ℕ ⊢Γ [n₁] [u])
      [Idneutral] = ne₌ (Id ℕ n₂ w) (idRed:*: (univ (Idⱼ (ℕⱼ ⊢Γ) ⊢oℕ ⊢w))) (Idℕₙ neKv)
                        (~-Idℕ ⊢Γ (PE.subst (λ X → Γ ⊢ X ~ _ ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym t≡t') (PE.subst (λ X → Γ ⊢ _ ~ X ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym v≡v') K~M)) u≡w)
  in transEq {A = Id ℕ t u} {B = Id ℕ n₁ u} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) ([Id]ℕ ⊢Γ [n₁] [u]) ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′
                  (transEq {A = Id ℕ n₁ u} {B = Id ℕ n₂ w} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [n₁] [u]) ([Id]ℕ ⊢Γ [n₂] [w]) ([Id]ℕ ⊢Γ [v] [w])
                                   [Idneutral] (symEq {A = Id ℕ v w} {B = Id ℕ n₂ w} {l = l} {l′ = l} ([Id]ℕ ⊢Γ [v] [w]) ([Id]ℕ ⊢Γ [n₂] [w]) [IdB≡ℕ]′))

[IdExt]ℕ {Γ} {l} {t} {u} {v} {w} ⊢Γ (ℕₜ .zero [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ zeroᵣ) (ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ neKu ⊢ku k≡ku)))
         (ℕₜ .zero [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ zeroᵣ) (ℕₜ n₃ [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw)))
         (ℕₜ₌ .zero .zero d₄ d′ k≡k′ zeroᵣ) (ℕₜ₌ k₁ k′₁ d₅ d′₁ k≡k′₁ (ne (neNfₜ₌ neK neM K~M))) =
  let u≡u' = whrDet*Term (du , ne neKu) (redₜ d₅ , ne neK)
      w≡w' = whrDet*Term (dw , ne neKw) (redₜ d′₁ , ne neM)
      [t] = ℕₜ zero [[ ⊢tℕ , ⊢mℕ , dt ]] n≡n₁ zeroᵣ
      [u] = ℕₜ n [[ ⊢uℕ , ⊢nℕ , du ]] n≡n (ne (neNfₜ neKu ⊢ku k≡ku))
      [v] = ℕₜ zero [[ ⊢vℕ , ⊢oℕ , dv ]] n≡n₂ zeroᵣ
      [w] = ℕₜ n₃ [[ ⊢wℕ , ⊢pℕ , dw ]] n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw))
      [n] = ℕₜ n (idRedTerm:*: ⊢nℕ) n≡n (ne (neNfₜ neKu ⊢ku k≡ku))
      [n₃] = ℕₜ n₃ (idRedTerm:*: ⊢pℕ) n≡n₃ (ne (neNfₜ neKw ⊢kw k≡kw))
      [zero] = ℕₜ zero (idRedTerm:*: (zeroⱼ ⊢Γ)) (≅ₜ-zerorefl ⊢Γ) zeroᵣ
      nfId = univ⇒* ((IdℕRed*Term′ ⊢tℕ ⊢mℕ dt ⊢uℕ) ⇨∷* Idℕ0Red*Term′ ⊢uℕ ⊢nℕ du)
      nfId' = univ⇒* ((IdℕRed*Term′ ⊢vℕ ⊢oℕ dv ⊢wℕ) ⇨∷* Idℕ0Red*Term′ ⊢wℕ ⊢pℕ dw)
      [IdA] , [IdA≡ℕ] = redSubst* nfId ([Id]ℕ ⊢Γ [zero] [n])
      [IdB] , [IdB≡ℕ] = redSubst* nfId' ([Id]ℕ ⊢Γ [zero] [n₃])
      [IdA≡ℕ]′ = irrelevanceEq {A = Id ℕ t u} {B = Id ℕ zero n} {l = ι ⁰} {l′ = l} [IdA] ([Id]ℕ ⊢Γ [t] [u]) [IdA≡ℕ]
      [IdB≡ℕ]′ = irrelevanceEq {A = Id ℕ v w} {B = Id ℕ zero n₃} {l = ι ⁰} {l′ = l} [IdB] ([Id]ℕ ⊢Γ [v] [w]) [IdB≡ℕ]
      [Idneutral] : Γ ⊩⟨ l ⟩ Id ℕ zero n ≡ Id ℕ zero n₃ ^ [ % , ι ⁰ ] / ([Id]ℕ ⊢Γ [zero] [n])
      [Idneutral] = ne₌ (Id ℕ zero n₃) (idRed:*: (univ (Idⱼ (ℕⱼ ⊢Γ) ⊢oℕ ⊢pℕ))) (Idℕ0ₙ neKw)
                (~-Idℕ0 ⊢Γ (PE.subst (λ X → Γ ⊢ X ~ _ ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym u≡u') (PE.subst (λ X → Γ ⊢ k₁ ~ X ∷ ℕ ^ [ ! , ι ⁰ ]) (PE.sym w≡w') K~M)))
  in transEq {A = Id ℕ t u} {B = Id ℕ zero n} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t] [u]) ([Id]ℕ ⊢Γ [zero] [n]) ([Id]ℕ ⊢Γ [v] [w])
                  [IdA≡ℕ]′
                  (transEq {A = Id ℕ zero n} {B = Id ℕ zero n₃} {C = Id ℕ v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [zero] [n]) ([Id]ℕ ⊢Γ [zero] [n₃]) ([Id]ℕ ⊢Γ [v] [w])
                                   [Idneutral] (symEq {A = Id ℕ v w} {B = Id ℕ zero n₃} {l = l} {l′ = l} ([Id]ℕ ⊢Γ [v] [w]) ([Id]ℕ ⊢Γ [zero] [n₃]) [IdB≡ℕ]′))

-- refuting cases

[IdExt]ℕ ⊢Γ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ _ _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) _ = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d₄ , sucₙ)))
[IdExt]ℕ ⊢Γ (ℕₜ n₁ d₁ n≡n₁ (ne (neNfₜ neK ⊢k k≡k))) _ _ _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) _ = ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d₄ , sucₙ) (redₜ d₁ , ne neK)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ .zero d₂ n≡n₂ zeroᵣ) _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) _ = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₂ , zeroₙ) (redₜ d′ , sucₙ)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ n₂ d₂ n≡n₂ (ne (neNfₜ neK ⊢k k≡k))) _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) _ = ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d′ , sucₙ) (redₜ d₂ , ne neK)))

[IdExt]ℕ ⊢Γ _ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ _ _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d₄ , sucₙ)))
[IdExt]ℕ ⊢Γ _ (ℕₜ n₁ d₁ n≡n₁ (ne (neNfₜ neK ⊢k k≡k))) _ _ _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) = ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d₄ , sucₙ) (redₜ d₁ , ne neK)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ .zero d₂ n≡n₂ zeroᵣ) _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₂ , zeroₙ) (redₜ d′ , sucₙ)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ n₂ d₂ n≡n₂ (ne (neNfₜ neK ⊢k k≡k))) _ (ℕₜ₌ .(suc _) .(suc _) d₄ d′ k≡k′ (sucᵣ x)) = ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d′ , sucₙ) (redₜ d₂ , ne neK)))

[IdExt]ℕ ⊢Γ (ℕₜ .(suc _) d n≡n (sucᵣ x₃)) _ _ _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) _ = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₅ , zeroₙ) (redₜ d , sucₙ)))
[IdExt]ℕ ⊢Γ (ℕₜ n d n≡n (ne (neNfₜ neK ⊢k k≡k))) _ _ _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) _ = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d₅ , zeroₙ) (redₜ d , ne neK)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ .(suc _) d₃ n≡n₃ (sucᵣ x₃)) _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) _ = ⊥-elim (zero≢suc (whrDet*Term (redₜ d′₁ , zeroₙ) (redₜ d₃ , sucₙ)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ n₃ d₃ n≡n₃ (ne (neNfₜ neK ⊢k k≡k))) _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) _ = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d′₁ , zeroₙ) (redₜ d₃ , ne neK)))

[IdExt]ℕ ⊢Γ _ (ℕₜ .(suc _) d n≡n (sucᵣ x₃)) _ _ _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) = ⊥-elim (zero≢suc (whrDet*Term (redₜ d₅ , zeroₙ) (redₜ d , sucₙ)))
[IdExt]ℕ ⊢Γ _ (ℕₜ n d n≡n (ne (neNfₜ neK ⊢k k≡k))) _ _ _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d₅ , zeroₙ) (redₜ d , ne neK)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ .(suc _) d₃ n≡n₃ (sucᵣ x₃)) _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) = ⊥-elim (zero≢suc (whrDet*Term (redₜ d′₁ , zeroₙ) (redₜ d₃ , sucₙ)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ n₃ d₃ n≡n₃ (ne (neNfₜ neK ⊢k k≡k))) _ (ℕₜ₌ .zero .zero d₅ d′₁ k≡k′₁ zeroᵣ) = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d′₁ , zeroₙ) (redₜ d₃ , ne neK)))

[IdExt]ℕ ⊢Γ (ℕₜ .(suc _) d₁ n≡n₁ (sucᵣ x₁)) _ _ _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) _ =  ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d₄ , ne neK)))
[IdExt]ℕ ⊢Γ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ _ _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) _ = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d₄ , ne neK)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ .(suc _) d₁ n≡n₁ (sucᵣ x₁)) _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) _ =  ⊥-elim (suc≢ne neM (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d′ , ne neM)))
[IdExt]ℕ ⊢Γ _ _ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) _ = ⊥-elim (zero≢ne neM (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d′ , ne neM)))

[IdExt]ℕ ⊢Γ _ (ℕₜ .(suc _) d₁ n≡n₁ (sucᵣ x₁)) _ _ _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) =  ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d₄ , ne neK)))
[IdExt]ℕ ⊢Γ _ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ _ _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) = ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d₄ , ne neK)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ .(suc _) d₁ n≡n₁ (sucᵣ x₁)) _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) =  ⊥-elim (suc≢ne neM (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d′ , ne neM)))
[IdExt]ℕ ⊢Γ _ _ _ (ℕₜ .zero d₁ n≡n₁ zeroᵣ) _ (ℕₜ₌ k k′ d₄ d′ k≡k′ (ne (neNfₜ₌ neK neM k≡m))) = ⊥-elim (zero≢ne neM (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d′ , ne neM)))

[Id]ℕGen : ∀ {Γ l A t u}
  (⊢Γ : ⊢ Γ)
  ([A] : Γ ⊩ℕ A)
  ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
  ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
  → Γ ⊩⟨ l ⟩ Id A t u ^ [ % , ι ⁰ ]

[Id]ℕGen ⊢Γ [[ ⊢A , ⊢B , D ]] (ℕₜ n d n≡n prop) (ℕₜ n₁ d₁ n≡n₁ prop₁) =
  let
    [[ ⊢tℕ , _ , _ ]] = d
    [[ ⊢uℕ , _ , _ ]] = d₁
  in proj₁ (redSubst* (IdRed* (conv ⊢tℕ (sym (subset* D))) (conv ⊢uℕ (sym (subset* D))) D)
    ([Id]ℕ ⊢Γ (ℕₜ n d n≡n prop) (ℕₜ n₁ d₁ n≡n₁ prop₁)))

[IdExt]ℕGen : ∀ {A B t v u w Γ l l'}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩ℕ A)
         ([B] : Γ ⊩ℕ B)
         ([A≡B] : Γ ⊩⟨ l ⟩ A ≡ B ^ [ ! , ι ⁰ ] / ℕᵣ [A])
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
         ([v] : Γ ⊩⟨ l' ⟩ v ∷ B ^ [ ! , ι ⁰ ] / ℕᵣ [B])
         ([t≡v] : Γ ⊩⟨ l ⟩ t ≡ v ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
         ([w] : Γ ⊩⟨ l' ⟩ w ∷ B ^ [ ! , ι ⁰ ] / ℕᵣ [B])
         ([u≡w] : Γ ⊩⟨ l ⟩ u ≡ w ∷ A ^ [ ! , ι ⁰ ] / ℕᵣ [A])
       → Γ ⊩⟨ l ⟩ Id A t u ≡ Id B v w ^ [ % , ι ⁰ ] / [Id]ℕGen ⊢Γ [A] [t] [u]

[IdExt]ℕGen {A} {B} {t} {v} {u} {w} {Γ} {l} {l'} ⊢Γ [[ ⊢A , ⊢B , D ]] [[ ⊢A₁ , ⊢B₁ , D₁ ]] [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  let [A] = [[ ⊢A , ⊢B , D ]]
      [B] = [[ ⊢A₁ , ⊢B₁ , D₁ ]]
      [ℕ]' = [ℕ] {l = l} ⊢Γ
      [A]' , [Aeq] = redSubst* D [ℕ]'
      [B]' , [Beq] = redSubst* D₁ [ℕ]'
      [t]′ = convTerm₁ {t = t} [A]' [ℕ]' [Aeq] (irrelevanceTerm {l = l} (ℕᵣ [A]) [A]' [t])
      [u]′ = convTerm₁ {t = u} [B]' [ℕ]' [Beq] (irrelevanceTerm {l = l} (ℕᵣ [B]) [B]' [u])
      [v]′ = convTerm₁ {t = v} [A]' [ℕ]' [Aeq] (irrelevanceTerm {l = l} (ℕᵣ [A]) [A]' [v])
      [w]′ = convTerm₁ {t = w} [B]' [ℕ]' [Beq] (irrelevanceTerm {l = l} (ℕᵣ [B]) [B]' [w])
      [t≡v]′ = convEqTerm₁ {t = t} {u = v} [A]' [ℕ]' [Aeq] (irrelevanceEqTerm {l = l} (ℕᵣ [A]) [A]' [t≡v])
      [u≡w]′ = convEqTerm₁ {t = u} {u = w} [B]' [ℕ]' [Beq] (irrelevanceEqTerm {l = l} (ℕᵣ [B]) [B]' [u≡w])
      X = irrelevanceEq {A = Id ℕ t u} {B = Id ℕ v w} {l = l} ([Id]ℕ ⊢Γ [t] [u]) ([Id]ℕ ⊢Γ [t]′ [u]′) ([IdExt]ℕ ⊢Γ [t]′ [u]′ [v]′ [w]′ [t≡v]′ [u≡w]′)
      [IdA] , [IdA≡U] = redSubst* {l = l} (IdRed* (escapeTerm {l = l} (ℕᵣ [A]) [t]) (escapeTerm {l = l} (ℕᵣ [A]) [u]) D) ([Id]ℕ ⊢Γ [t]′ [u]′)
      [IdB] , [IdB≡U] = redSubst* (IdRed* (escapeTerm {l = l} (ℕᵣ [B]) [v]) (escapeTerm {l = l} (ℕᵣ [B]) [w]) D₁) ([Id]ℕ ⊢Γ [v]′ [w]′)
      [IDAtu] = [Id]ℕGen ⊢Γ [A] [t] [u]
      [IDBvw] = [Id]ℕGen ⊢Γ [B] [v] [w]
      [IdA≡U]′ = irrelevanceEq {A = Id A t u} {B = Id ℕ t u} [IdA] [IDAtu] [IdA≡U]
      [IdB≡U]′ = irrelevanceEq {A = Id B v w} {B = Id ℕ v w} {l = l} {l′ = l}  [IdB] [IDBvw] [IdB≡U]
  in  transEq {A = Id A t u} {B = Id ℕ t u} {C = Id B v w} {l = l} {l′ = l} {l″ = l} [IDAtu] ([Id]ℕ ⊢Γ [t]′ [u]′) [IDBvw]
              [IdA≡U]′
              (transEq {A = Id ℕ t u} {B = Id ℕ v w} {C = Id B v w} {l = l} {l′ = l} {l″ = l} ([Id]ℕ ⊢Γ [t]′ [u]′) ([Id]ℕ ⊢Γ [v]′ [w]′) [IDBvw]
                       X (symEq {A = Id B v w} {B = Id ℕ v w} [IDBvw] ([Id]ℕ ⊢Γ [v]′ [w]′) [IdB≡U]′))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module Control.WellFounded where

open import Prelude
open import Prelude.Nat.Properties using (suc-inj)

data Acc {a} {A : Set a} (_<_ : A → A → Set a) (x : A) : Set a where
  acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x

-- LessNat is well-founded --

private
  wfNatSlow : (n : Nat) → Acc _<_ n

  wfNatSlow′ : (n j y : Nat) → n ≡ suc (j + y) → Acc _<_ y
  wfNatSlow′ (suc n)  zero  .n refl = wfNatSlow n
  wfNatSlow′ (suc n) (suc j) y eq   = wfNatSlow′ n j y (suc-inj eq)
  wfNatSlow′ zero     zero   y ()
  wfNatSlow′ zero    (suc j) y ()

  wfNatSlow n = acc λ { y (diff j eq) → wfNatSlow′ n j y eq }

  -- Need to match on n to avoid unfolding on neutral argument!
  wfNatFast : {k : Nat} → (n : Nat) → Acc _<_ n
  wfNatFast {zero}     n    = wfNatSlow n
  wfNatFast {suc k}  zero   = wfNatSlow zero
  wfNatFast {suc k} (suc n) = acc λ m _ → wfNatFast {k} m

wfNat : (n : Nat) → Acc _<_ n
wfNat n = wfNatFast {1000000000} n

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

module Contract where

open import Basic_Types
open import Identity
open import Homotopy_Equivalence

-- a contractable space means there is a point which is path-connected to any
-- other point in the same space

is_contr : Set → Set
is_contr A = Σ a ∶ A , (∀ (x : A) → a ≡ x)


text:
{-# OPTIONS --cubical-compatible #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data Fin : Nat → Set where
  zero : {n : Nat} → Fin (suc n)
  suc  : {n : Nat} (i : Fin n) → Fin (suc n)

-- From Data.Fin.Properties in the standard library (2016-12-30).
suc-injective : ∀ {o} {m n : Fin o} → Fin.suc m ≡ suc n → m ≡ n
suc-injective refl = refl


text:
-- Andreas, 2016-11-03, issue #2292
-- Internal error when debugging the coverage checker.

{-# OPTIONS -v tc.cover.top:10 #-} -- KEEP!

data ⊥ : Set where

⊥-elim : ∀{A : Set} → ⊥ → A
⊥-elim ()


text:
-- Some theorems about operations on non-deterministic values

module nondet-thms where

open import bool
open import bool-thms
open import nat
open import eq
open import nat-thms
open import functions
open import nondet

----------------------------------------------------------------------
-- Theorems about values contained in non-deterministic values:

-- A proof that x is value of the non-deterministic tree y:
-- either it is equal to a deterministic value (ndrefl)
-- or it is somewhere in the tree.
-- If it is in the tree then we need to construct both branches of the tree,
-- and a proof that x is in one of the branches
-- A consequence of this is that any proof that x ∈ y contains the path
-- to x in the tree.
--
-- Example:
-- hInCoin : H ∈ coin
-- hInCoin = left (Val H) (Val T) ndrefl
--
-- Since H is on the left side of coin, we use the left constructor
-- The branches of the tree are (Val H) and (Val T),
-- and since H is identically equal to H this completes the proof.
data _∈_ {A : Set} (x : A) : (y : ND A) → Set where
  ndrefl : x ∈ (Val x)
  left   : (l : ND A) → (r : ND A) → x ∈ l → x ∈ (l ?? r)
  right  : (l : ND A) → (r : ND A) → x ∈ r → x ∈ (l ?? r)

-- A basic inductive lemma that shows that ∈ is closed under function
-- application. That is, if x ∈ nx, then f x ∈ f $* nx
--
-- Example:
-- ndCons : ... → xs ∈ nxs → (x :: xs) ∈ (_::_ x) $* nxs
∈-$* : {A B : Set} → (f : A → B) → (x : A) → (nx : ND A)
        → x ∈ nx → (f x) ∈ (f $* nx)
∈-$* f x (Val .x) ndrefl = ndrefl
∈-$* f x (l ?? r) (left  .l .r k) =
  left  (f $* l) (f $* r) (∈-$* f x l k)
∈-$* f x (l ?? r) (right .l .r k) =
  right (f $* l) (f $* r) (∈-$* f x r k)

-- This is a similar result as ∈-$* but for non-deterministic application:
∈-*$* : {A B : Set} → (x : A) → (nx : ND A) → (f : A → B)
        → (nf : A → ND B) → x ∈ nx → f x ∈ nf x → f x ∈ (nf *$* nx)
∈-*$* x (Val .x) f nf ndrefl pf = pf
∈-*$* x (l ?? r) f nf (left  .l .r p) pf =
  left (nf *$* l) (nf *$* r) (∈-*$* x l f nf p pf)
∈-*$* x (l ?? r) f nf (right .l .r p) pf =
  right (nf *$* l) (nf *$* r) (∈-*$* x r f nf p pf)

----------------------------------------------------------------------
-- Theorems about '$*':

-- Combine two $* applications into one:
$*-$* : ∀ {A B C : Set} → (f : B → C) (g : A → B) (xs : ND A)
            → f $* (g $* xs) ≡ (f ∘ g) $* xs
$*-$* f g (Val x) = refl
$*-$* f g (t1 ?? t2) rewrite $*-$* f g t1 | $*-$* f g t2 = refl

----------------------------------------------------------------------
-- Theorems about 'always':

-- Extend validity of a function with a deterministic argument to validity of
-- the corresponding non-deterministic function:
always-$* : ∀ {A : Set} → (p : A → 𝔹) (xs : ND A)
          → ((y : A) → p y ≡ tt)
          → always (p $* xs) ≡ tt
always-$* _ (Val y) prf = prf y
always-$* p (t1 ?? t2) prf
  rewrite always-$* p t1 prf
        | always-$* p t2 prf = refl

-- Extend validity of a function with a deterministic argument to validity of
-- the corresponding non-deterministic function:
always-*$* : ∀ {A : Set} → (p : A → ND 𝔹) (xs : ND A)
               → ((y : A) → always (p y) ≡ tt)
               → always (p *$* xs) ≡ tt
always-*$* _ (Val y) prf = prf y
always-*$* p (t1 ?? t2) prf
  rewrite always-*$* p t1 prf
        | always-*$* p t2 prf = refl

-- Extend validity of a deterministic function to validity of
-- corresponding function with non-deterministic result:
always-toND : ∀ {A : Set} → (p : A → 𝔹) (x : A)
          → (p x) ≡ tt → always (toND p x) ≡ tt
always-toND _ _ p = p

----------------------------------------------------------------------
-- Theorems about 'satisfy':

-- A theorem like filter-map in functional programming:
satisfy-$* : ∀ {A B : Set} → (f : A → B) (xs : ND A) (p : B → 𝔹)
             → (f $* xs) satisfy p ≡ xs satisfy (p ∘ f)
satisfy-$* _ (Val x) _ = refl
satisfy-$* f (t1 ?? t2) p
 rewrite satisfy-$* f t1 p
       | satisfy-$* f t2 p = refl

-- Extend validity of function with deterministic argument to validity of
-- non-deterministic function:
satisfy-*$* : ∀ {A B : Set} → (p : B → 𝔹) (f : A → ND B) (xs : ND A)
               → ((y : A) → (f y) satisfy p ≡ tt)
               → (f *$* xs) satisfy p ≡ tt
satisfy-*$* _ _ (Val y) prf = prf y
satisfy-*$* p f (t1 ?? t2) prf
  rewrite satisfy-*$* p f t1 prf
        | satisfy-*$* p f t2 prf = refl

----------------------------------------------------------------------
-- Theorems about 'every':

every-$* : ∀ (f : ℕ → ℕ) (v : ℕ) (x : ND ℕ) →
         every _=ℕ_ v x ≡ tt → every _=ℕ_ (f v) (f $* x) ≡ tt
every-$* f v (Val x) u rewrite =ℕ-to-≡ {v} {x} u | =ℕ-refl (f x) = refl
every-$* f v (t1 ?? t2) u
  rewrite every-$* f v t1 (&&-fst u)
        | every-$* f v t2 (&&-snd {every _=ℕ_ v t1} {every _=ℕ_ v t2} u) = refl

----------------------------------------------------------------------
-- This theorms allows to weaken a predicate which is always satisfied:
weak-always-predicate : ∀ {A : Set} → (p p1 : A → 𝔹) (xs : ND A)
                → xs satisfy p ≡ tt
                → xs satisfy (λ x → p1 x || p x) ≡ tt
weak-always-predicate p p1 (Val x) u rewrite u | ||-tt (p1 x) = refl
weak-always-predicate p p1 (t1 ?? t2) u
  rewrite weak-always-predicate p p1 t1 (&&-fst u)
        | weak-always-predicate p p1 t2 (&&-snd {t1 satisfy p} {t2 satisfy p} u)
  = refl

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
-- A minor variant of code reported by Andreas Abel. The code below
-- should be rejected.

open import Agda.Builtin.Size

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  size : (j : Size< i) → SizeLt i

<∞ : SizeLt ∞
<∞ = size ∞

data D (i : Size) : SizeLt i → Set where
  c : ∀ {i' : Size< i} → ((j : SizeLt i') → D i' j) → D i (size i')

f : D ∞ <∞ → ⊥
f (c h) = f (h <∞)

d : ∀ i s → D i s
d i (size j) = c (d j)

loop : ⊥
loop = f (d ∞ <∞)

max_forks_repo_name: Agda-zh/agda


text:
module Vec where

open import SHE-Prelude

data Nat : Set where
  z : Nat
  s : Nat -> Nat

data Vec (X : Set) : Nat -> Set where
  vNil : Vec X z
  _:-_ : forall {n} ->
         X -> Vec X n -> Vec X (s n)

_+N_ : Nat -> Nat -> Nat
z  +N n = n
s m +N n = s (m +N n)

_vappend_ : forall {X m n} -> Vec X m -> Vec X n -> Vec X (m +N n)
vNil vappend ys = ys
(x :- xs) vappend ys = x :- (xs vappend ys)

vec : forall {n X} -> X -> Vec X n
vec {z} x = vNil
vec {s n} x = x :- vec x

_N>=_ : Nat -> Nat -> Set
m N>= z = One
z N>= s n  = Zero
s m N>= s n = m N>= n

vtake : {X : Set}{m : Nat}(n : Nat) -> m N>= n -> Vec X m -> Vec X n
vtake (s n) () vNil
vtake z p xs = vNil
vtake (s n) p (x :- xs) = x :- (vtake n p xs)

VecApp : forall {n} -> Applicative \X -> Vec X n
VecApp {n} = record
  { pure  = vec
  ; _<*>_ = vapp
  } where
    vapp : forall {n X Y} ->
       Vec (X -> Y) n -> Vec X n -> Vec Y n
    vapp vNil vNil = vNil
    vapp (f :- fs) (x :- xs) = f x :- vapp fs xs

v1 : Vec Nat (s (s (s z)))
v1 = Applicative.pure VecApp z

v2 : Vec Nat (s z)
v2 = vtake (s z) <> v1

v3 : Vec Nat (s z)
v3 = vec {s z} z

v5 : Vec Nat (s z)
v5 = vtake (s z) <> (z :- (z :- vNil))

v6 : Vec Nat (s z)
v6 = vtake (s z) <> (z :- (z :- vNil))

max_stars_repo_name: iain-logan/she

max_issues_repo_name: iain-logan/she

max_forks_repo_name: iain-logan/she