data Empty : * => { }

absurd [A : *] [x : Empty] : A => (
  Empty-Elim x (\_ => A)
)

neg [A : *] : * => (A -> Empty)

record Unit : * => tt { }

record Prod : [A : *] [B : A -> *] -> * =>
  prod {fst : A, snd : B fst}

data Bool : * => { true : Bool | false : Bool }

-- The if_then_else_ is provided by Bool-Elim