quox/examples/misc.quox

37 lines
1.2 KiB
Text
Raw Normal View History

2023-05-21 14:33:42 -04:00
def0 True : ★ = {true};
2023-04-18 18:42:40 -04:00
2023-05-21 14:33:42 -04:00
def0 False : ★ = {};
def0 Not : 0.★ → ★ = λ 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-04-18 18:42:40 -04:00
λ A v ⇒ case0 v return A of { };
2023-05-21 14:33:42 -04:00
def0 Pred : 0.★ → ★¹ = λ A ⇒ 0.A → ★;
2023-04-03 10:07:51 -04:00
2023-05-21 14:33:42 -04:00
def0 All : 0.(A : ★) → 0.(Pred A) → ★¹ =
2023-04-03 10:07:51 -04:00
λ A P ⇒ 1.(x : A) → P x;
2023-04-18 18:42:40 -04:00
def cong :
2023-05-21 14:33:42 -04:00
0.(A : ★) → 0.(P : Pred A) → 1.(p : All A P) →
0.(x y : A) → 1.(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
2023-04-18 18:42:40 -04:00
λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖);
2023-04-03 10:07:51 -04:00
def0 eq-f :
2023-05-21 14:33:42 -04:00
0.(A : ★) → 0.(P : Pred 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-04-03 10:07:51 -04:00
λ A P p q x ⇒ p x ≡ q x : P x;
2023-04-18 18:42:40 -04:00
def funext :
2023-05-21 14:33:42 -04:00
0.(A : ★) → 0.(P : Pred A) → 0.(p q : All A P) →
1.(All A (eq-f A P p q)) → p ≡ q : All A P =
2023-04-18 18:42:40 -04:00
λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖;
2023-04-15 09:13:01 -04:00
2023-05-21 14:33:42 -04:00
def sym : 0.(A : ★) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
λ 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 ⇒ δ 𝑖
comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };