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 ------------------------------------------------------------
  22 -- Examples →
  23
  24 data Nat : * => { zero : Nat | suc : Nat -> Nat }
  25
  26 gt [n : Nat] : Nat -> * => (
  27   Nat-Elim
  28     n
  29     (\_ => Nat -> *)
  30     (\_ => Empty)
  31     (\n f m => Nat-Elim m (\_ => *) Unit (\m' _ => f m'))
  32 )
  33
  34 data List : [A : *] -> * =>
  35   { nil : List A | cons : A -> List A -> List A }
  36
  37 length [A : *] [xs : List A] : Nat => (
  38     List-Elim xs (\_ => Nat) zero (\_ _ n => suc n)
  39 )
  40
  41 head [A : *] [xs : List A] : gt (length A xs) zero -> A => (
  42     List-Elim
  43       xs
  44       (\xs => gt (length A xs) zero -> A)
  45       (\p => absurd A p)
  46       (\x _ _ _ => x)
  47 )
  48
  49 ------------------------------------------------------------
  50 -- Examples ×
  51