rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add misc.coherence

Browse source
This commit is contained in:
rhiannon morris 2023-08-27 18:34:19 +02:00
parent 2340b14407
commit 387d44431a
1 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
examples/misc.quox
View file

@ -9,11 +9,18 @@ def void : 0.(A : ★) → 0.False → A =
def0 All : (A : ★) → (0.A → ★) → ★¹ = def0 All : (A : ★) → (0.A → ★) → ★¹ =
λ A P ⇒ (x : A) → P x λ A P ⇒ (x : A) → P x
def cong : def0 cong :
0.(A : ★) → 0.(P : 0.A → ★) → (p : All A P) → (A : ★) → (P : 0.A → ★) → (p : All A P) →
0.(x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) = (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖) λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
def0 coherence :
(A B : ★) → (AB : A ≡ B : ★) → (x : A) →
Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
λ A B AB x ⇒
δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
def0 eq-f : def0 eq-f :
0.(A : ★) → 0.(P : 0.A → ★) → 0.(A : ★) → 0.(P : 0.A → ★) →
0.(p : All A P) → 0.(q : All A P) → 0.(p : All A P) → 0.(q : All A P) →
@ -35,29 +42,29 @@ def trans : 0.(A : ★) → 0.(x y z : A) →
def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] = def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] =
λ A B f x ⇒ λ A B f x ⇒
case x return [ω.B] of { [x'] ⇒ [f x'] }; case x return [ω.B] of { [x'] ⇒ [f x'] }
def0 Sing : (A : ★) → A → ★ = def0 Sing : (A : ★) → A → ★ =
λ A x ⇒ (val : A) × [0. val ≡ x : A]; λ A x ⇒ (val : A) × [0. val ≡ x : A]
namespace sing { namespace sing {
def val : 0.(A : ★) → 0.(x : A) → Sing A x → A = def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
λ A _ sg ⇒ λ A _ sg ⇒
case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } }; case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } }
def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A = def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
λ A x sg ⇒ λ A x sg ⇒
case sg return sg' ⇒ val A x sg' ≡ x : A of { (x', eq) ⇒ case sg return sg' ⇒ val A x sg' ≡ x : A of { (x', eq) ⇒
case eq return eq' ⇒ val A x (x', eq') ≡ x : A of { [eq'] ⇒ eq' } case eq return eq' ⇒ val A x (x', eq') ≡ x : A of { [eq'] ⇒ eq' }
}; }
def app : 0.(A B : ★) → 0.(x : A) → def app : 0.(A B : ★) → 0.(x : A) →
(f : A → B) → Sing A x → Sing B (f x) = (f : A → B) → Sing A x → Sing B (f x) =
λ A B x f sg ⇒ λ A B x f sg ⇒
case sg return Sing B (f x) of { (x_, eq) ⇒ case sg return Sing B (f x) of { (x_, eq) ⇒
case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) } case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
}; }
} }