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

some example stuff

Browse source
This commit is contained in:
rhiannon morris 2023-09-17 14:41:29 +02:00
parent 8221d71416
commit 7bd959e919
2 changed files with 21 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
examples/misc.quox
View file

@ -44,6 +44,9 @@ 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 HEq : (A B : ★) → A → B → ★¹ =
λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y
def0 Sing : (A : ★) → A → ★ = def0 Sing : (A : ★) → A → ★ =
λ A x ⇒ (val : A) × [0. val ≡ x : A] λ A x ⇒ (val : A) × [0. val ≡ x : A]

25
examples/pair.quox
View file

@ -1,15 +1,15 @@
namespace pair { namespace pair {
def0 Σ : (A : ★) → (0.A → ★) → ★ = λ A B ⇒ (x : A) × B x; def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x;
def fst : 0.(A : ★) → 0.(B : 0.A → ★) → ω.(Σ A B) → A = def fst : 0.(A : ★) → 0.(B : A → ★) → ω.(Σ A B) → A =
λ A B p ⇒ caseω p return A of { (x, _) ⇒ x }; λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
def snd : 0.(A : ★) → 0.(B : 0.A → ★) → ω.(p : Σ A B) → B (fst A B p) = def snd : 0.(A : ★) → 0.(B : A → ★) → ω.(p : Σ A B) → B (fst A B p) =
λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y }; λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y };
def uncurry : def uncurry :
0.(A : ★) → 0.(B : 0.A → ★) → 0.(C : 0.(x : A) → 0.(B x) → ★) → 0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) →
(f : (x : A) → (y : B x) → C x y) → (f : (x : A) → (y : B x) → C x y) →
(p : Σ A B) → C (fst A B p) (snd A B p) = (p : Σ A B) → C (fst A B p) (snd A B p) =
λ A B C f p ⇒ λ A B C f p ⇒
@ -20,7 +20,7 @@ def uncurry' :
λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C); λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C);
def curry : def curry :
0.(A : ★) → 0.(B : 0.A → ★) → 0.(C : 0.(Σ A B) → ★) → 0.(A : ★) → 0.(B : A → ★) → 0.(C : (Σ A B) → ★) →
(f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) = (f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) =
λ A B C f x y ⇒ f (x, y); λ A B C f x y ⇒ f (x, y);
@ -29,16 +29,27 @@ def curry' :
λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C); λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
def0 fst-snd : def0 fst-snd :
(A : ★) → (B : 0.A → ★) → (A : ★) → (B : A → ★) →
(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B = (p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
λ A B p ⇒ λ A B p ⇒
case p case p
return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) }; of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
def0 fst-eq :
(A : ★) → (B : A → ★) →
(p q : Σ A B) → p ≡ q : Σ A B → fst A B p ≡ fst A B q : A =
λ A B p q eq ⇒ δ 𝑖 ⇒ fst A B (eq @𝑖);
def0 snd-eq :
(A : ★) → (B : A → ★) →
(p q : Σ A B) → (eq : p ≡ q : Σ A B) →
Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd A B p) (snd A B q) =
λ A B p q eq ⇒ δ 𝑖 ⇒ snd A B (eq @𝑖);
def map : def map :
0.(A A' : ★) → 0.(A A' : ★) →
0.(B : 0.A → ★) → 0.(B' : 0.A' → ★) → 0.(B : A → ★) → 0.(B' : A' → ★) →
(f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) → (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
(Σ A B) → Σ A' B' = (Σ A B) → Σ A' B' =
λ A A' B B' f g p ⇒ λ A A' B B' f g p ⇒