+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