itt.ka

   1 ------------------------------------------------------------
   2 -- Core ITT (minus W)
   3
   4 data Empty : ⋆ ⇒ { }
   5
   6 absurd [A : ⋆] [x : Empty] : A ⇒ (
   7   Empty-Elim x (λ _ ⇒ A)
   8 )
   9
  10 neg [A : ⋆] : ⋆ ⇒ (A → Empty)
  11
  12 record Unit : ⋆ ⇒ tt { }
  13
  14 record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
  15   prod {fst : A, snd : B fst}
  16
  17 data Bool : ⋆ ⇒ { true : Bool | false : Bool }
  18
  19 -- The if_then_else_ is provided by Bool-Elim
  20
  21 -- A large eliminator, for convenience
  22 ITE [b : Bool] [A B : ⋆] : ⋆ ⇒ (
  23   Bool-Elim b (λ _ ⇒ ⋆) A B
  24 )
  25
  26 ------------------------------------------------------------
  27 -- Examples →
  28
  29 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
  30
  31 gt [n : Nat] : Nat → ⋆ ⇒ (
  32   Nat-Elim
  33     n
  34     (λ _ ⇒ Nat → ⋆)
  35     (λ _ ⇒ Empty)
  36     (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Unit (λ m' _ ⇒ f m'))
  37 )
  38
  39 data List : [A : ⋆] → ⋆ ⇒
  40   { nil : List A | cons : A → List A → List A }
  41
  42 length [A : ⋆] [xs : List A] : Nat ⇒ (
  43     List-Elim xs (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
  44 )
  45
  46 head [A : ⋆] [xs : List A] : gt (length A xs) zero → A ⇒ (
  47     List-Elim
  48       xs
  49       (λ xs ⇒ gt (length A xs) zero → A)
  50       (λ p ⇒ absurd A p)
  51       (λ x _ _ _ ⇒ x)
  52 )
  53
  54 ------------------------------------------------------------
  55 -- Examples ×
  56
  57 data Parity : ⋆ ⇒ { even : Parity | odd : Parity }
  58
  59 flip [p : Parity] : Parity ⇒ (
  60   Parity-Elim p (λ _ ⇒ Parity) odd even
  61 )
  62
  63 parity [n : Nat] : Parity ⇒ (
  64   Nat-Elim n (λ _ ⇒ Parity) even (λ _ ⇒ flip)
  65 )
  66
  67 even [n : Nat] : ⋆ ⇒ (Parity-Elim (parity n) (λ _ ⇒ ⋆) Unit Empty)
  68
  69 one   : Nat ⇒ (suc zero)
  70 two   : Nat ⇒ (suc one)
  71 three : Nat ⇒ (suc two)
  72 four  : Nat ⇒ (suc three)
  73 five  : Nat ⇒ (suc four)
  74 six   : Nat ⇒ (suc five)
  75
  76 even-6 : even six ⇒ tt
  77
  78 even-5-neg : neg (even five) ⇒ (λ z ⇒ z)
  79
  80 there-is-an-even-number : Prod Nat even ⇒ (prod six even-6)
  81
  82 Or [A B : ⋆] : ⋆ ⇒ (Prod Bool (λ b ⇒ ITE b A B))
  83
  84 left  [A B : ⋆] [x : A] : Or A B ⇒ (prod true  x)
  85 right [A B : ⋆] [x : B] : Or A B ⇒ (prod false x)
  86
  87 case [A B C : ⋆] [f : A → C] [g : B → C] [x : Or A B] : C ⇒ (
  88   (Bool-Elim (fst x) (λ b ⇒ ITE b A B → C) f g) (snd x)
  89 )