X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=itt.ka;h=9545a557fe2645b846c5a13fa4d2874860942b9f;hb=HEAD;hp=e9decf6bb4a19d72bdfd3de644adc9827246afa4;hpb=220ca85e4c690269298b9e8c1ef1752fad285855;p=bitonic-mengthesis.git

diff --git a/itt.ka b/itt.ka
index e9decf6..9545a55 100644
--- a/itt.ka
+++ b/itt.ka
@@ -1,17 +1,89 @@
-data Empty : * => { }
+------------------------------------------------------------
+-- Core ITT (minus W)
 
-absurd [A : *] [x : Empty] : A => (
-  Empty-Elim x (\_ => A)
+data Empty : ⋆ ⇒ { }
+
+absurd [A : ⋆] [x : Empty] : A ⇒ (
+  Empty-Elim x (λ _ ⇒ A)
 )
 
-neg [A : *] : * => (A -> Empty)
+neg [A : ⋆] : ⋆ ⇒ (A → Empty)
 
-record Unit : * => tt { }
+record Unit : ⋆ ⇒ tt { }
 
-record Prod : [A : *] [B : A -> *] -> * =>
+record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
   prod {fst : A, snd : B fst}
 
-data Bool : * => { true : Bool | false : Bool }
+data Bool : ⋆ ⇒ { true : Bool | false : Bool }
 
 -- The if_then_else_ is provided by Bool-Elim
 
+-- A large eliminator, for convenience
+ITE [b : Bool] [A B : ⋆] : ⋆ ⇒ (
+  Bool-Elim b (λ _ ⇒ ⋆) A B
+)
+
+------------------------------------------------------------
+-- Examples →
+
+data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
+
+gt [n : Nat] : Nat → ⋆ ⇒ (
+  Nat-Elim
+    n
+    (λ _ ⇒ Nat → ⋆)
+    (λ _ ⇒ Empty)
+    (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Unit (λ m' _ ⇒ f m'))
+)
+
+data List : [A : ⋆] → ⋆ ⇒
+  { nil : List A | cons : A → List A → List A }
+
+length [A : ⋆] [xs : List A] : Nat ⇒ (
+    List-Elim xs (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
+)
+
+head [A : ⋆] [xs : List A] : gt (length A xs) zero → A ⇒ (
+    List-Elim
+      xs
+      (λ xs ⇒ gt (length A xs) zero → A)
+      (λ p ⇒ absurd A p)
+      (λ x _ _ _ ⇒ x)
+)
+
+------------------------------------------------------------
+-- Examples ×
+
+data Parity : ⋆ ⇒ { even : Parity | odd : Parity }
+
+flip [p : Parity] : Parity ⇒ (
+  Parity-Elim p (λ _ ⇒ Parity) odd even
+)
+
+parity [n : Nat] : Parity ⇒ (
+  Nat-Elim n (λ _ ⇒ Parity) even (λ _ ⇒ flip)
+)
+
+even [n : Nat] : ⋆ ⇒ (Parity-Elim (parity n) (λ _ ⇒ ⋆) Unit Empty)
+
+one   : Nat ⇒ (suc zero)
+two   : Nat ⇒ (suc one)
+three : Nat ⇒ (suc two)
+four  : Nat ⇒ (suc three)
+five  : Nat ⇒ (suc four)
+six   : Nat ⇒ (suc five)
+
+even-6 : even six ⇒ tt
+
+even-5-neg : neg (even five) ⇒ (λ z ⇒ z)
+
+there-is-an-even-number : Prod Nat even ⇒ (prod six even-6)
+
+Or [A B : ⋆] : ⋆ ⇒ (Prod Bool (λ b ⇒ ITE b A B))
+
+left  [A B : ⋆] [x : A] : Or A B ⇒ (prod true  x)
+right [A B : ⋆] [x : B] : Or A B ⇒ (prod false x)
+
+case [A B C : ⋆] [f : A → C] [g : B → C] [x : Or A B] : C ⇒ (
+  (Bool-Elim (fst x) (λ b ⇒ ITE b A B → C) f g) (snd x)
+)
\ No newline at end of file