let bool: Type = Sum { True | False };
-- Each constructor have only one argument
-- Capitalized names are constructors so constructor calls are lexically
-- recognizable

let not: bool -> bool = split
 { True => False
 | False => True
 };
-- Pattern matching

let boolean_id: bool -> bool = \lambda n . n;
-- Simple functions can be defined with lambdas

let and: bool -> bool -> bool = split
 { True => boolean_id
 | False => \lambda _. False
 };
-- Nested functions

let elimBool
  : \Pi c : bool → Type
  . \Pi _ : c False
  . \Pi _ : c True
  . \Pi b : bool
  . c b

  = λ c . λ h0 . λ h1 . split
  { True => h1
  | False => h0
  };