itt.ka

   1 data Empty : * => { }
   2
   3 absurd [A : *] [x : Empty] : A => (
   4   Empty-Elim x (\_ => A)
   5 )
   6
   7 neg [A : *] : * => (A -> Empty)
   8
   9 record Unit : * => tt { }
  10
  11 record Prod : [A : *] [B : A -> *] -> * =>
  12   prod {fst : A, snd : B fst}
  13
  14 data Bool : * => { true : Bool | false : Bool }
  15
  16 -- The if_then_else_ is provided by Bool-Elim
  17