-- 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 →
------------------------------------------------------------
-- 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