quox/examples/misc.quox

74 lines
2.3 KiB
Text
Raw Normal View History

2023-07-16 21:52:12 -04:00
def0 True : ★ = {true}
2023-04-18 18:42:40 -04:00
2023-07-16 21:52:12 -04:00
def0 False : ★ = {}
def0 Not : ★ → ★ = λ A ⇒ ω.A → False
2023-04-18 18:42:40 -04:00
2023-05-21 14:33:42 -04:00
def void : 0.(A : ★) → 0.False → A =
2023-07-16 21:52:12 -04:00
λ A v ⇒ case0 v return A of { }
2023-04-18 18:42:40 -04:00
def0 All : (A : ★) → (0.A → ★) → ★ =
λ A P ⇒ (x : A) → P x
2023-04-03 10:07:51 -04:00
2023-08-27 12:34:19 -04:00
def0 cong :
(A : ★) → (P : 0.A → ★) → (p : All A P) →
(x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
2023-07-16 21:52:12 -04:00
λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
2023-04-03 10:07:51 -04:00
2023-08-27 12:34:19 -04:00
def0 coherence :
(A B : ★) → (AB : A ≡ B : ★) → (x : A) →
Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
λ A B AB x ⇒
δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x
2023-04-03 10:07:51 -04:00
def0 eq-f :
0.(A : ★) → 0.(P : 0.A → ★) →
2023-04-03 10:07:51 -04:00
0.(p : All A P) → 0.(q : All A P) →
2023-05-21 14:33:42 -04:00
0.A → ★ =
2023-07-16 21:52:12 -04:00
λ A P p q x ⇒ p x ≡ q x : P x
2023-04-03 10:07:51 -04:00
2023-04-18 18:42:40 -04:00
def funext :
0.(A : ★) → 0.(P : 0.A → ★) → 0.(p q : All A P) →
(All A (eq-f A P p q)) → p ≡ q : All A P =
2023-07-16 21:52:12 -04:00
λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
2023-04-15 09:13:01 -04:00
def sym : 0.(A : ★) → 0.(x y : A) → (x ≡ y : A) → y ≡ x : A =
2023-07-16 21:52:12 -04:00
λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
2023-04-17 15:44:16 -04:00
2023-05-21 14:33:42 -04:00
def trans : 0.(A : ★) → 0.(x y z : A) →
2023-04-18 18:42:40 -04:00
ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
λ A x y z eq1 eq2 ⇒ δ 𝑖
2023-07-16 21:52:12 -04:00
comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }
2023-07-22 15:26:20 -04:00
def appω : 0.(A B : ★) → ω.(f : A → B) → [ω.A] → [ω.B] =
λ A B f x ⇒
2023-08-27 12:34:19 -04:00
case x return [ω.B] of { [x'] ⇒ [f x'] }
2023-07-22 15:26:20 -04:00
2023-09-17 08:41:29 -04:00
def0 HEq : (A B : ★) → A → B → ★¹ =
λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
2023-07-22 15:26:20 -04:00
def0 Sing : (A : ★) → A → ★ =
2023-08-27 12:34:19 -04:00
λ A x ⇒ (val : A) × [0. val ≡ x : A]
2023-07-22 15:26:20 -04:00
namespace sing {
def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
λ A _ sg ⇒
2023-08-27 12:34:19 -04:00
case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } }
2023-07-22 15:26:20 -04:00
def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
λ A x sg ⇒
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' }
2023-08-27 12:34:19 -04:00
}
2023-07-22 15:26:20 -04:00
def app : 0.(A B : ★) → 0.(x : A) →
(f : A → B) → Sing A x → Sing B (f x) =
λ A B x f sg ⇒
case sg return Sing B (f x) of { (x_, eq) ⇒
case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
2023-08-27 12:34:19 -04:00
}
2023-07-22 15:26:20 -04:00
}