------------------------------------------------------------
-- Core ITT (minus W)

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

-- A large eliminator, for convenience
ITE [b : Bool] [A B : ⋆] : ⋆ ⇒ (
  Bool-Elim b (λ _ ⇒ ⋆) A B
)

------------------------------------------------------------
-- Examples →

data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }

gt [n : Nat] : Nat → ⋆ ⇒ (
  Nat-Elim
    n
    (λ _ ⇒ Nat → ⋆)
    (λ _ ⇒ Empty)
    (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Unit (λ m' _ ⇒ f m'))
)

data List : [A : ⋆] → ⋆ ⇒
  { nil : List A | cons : A → List A → List A }

length [A : ⋆] [xs : List A] : Nat ⇒ (
    List-Elim xs (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
)

head [A : ⋆] [xs : List A] : gt (length A xs) zero → A ⇒ (
    List-Elim
      xs
      (λ xs ⇒ gt (length A xs) zero → A)
      (λ p ⇒ absurd A p)
      (λ x _ _ _ ⇒ x)
)

------------------------------------------------------------
-- Examples ×

data Parity : ⋆ ⇒ { even : Parity | odd : Parity }

flip [p : Parity] : Parity ⇒ (
  Parity-Elim p (λ _ ⇒ Parity) odd even
)

parity [n : Nat] : Parity ⇒ (
  Nat-Elim n (λ _ ⇒ Parity) even (λ _ ⇒ flip)
)

even [n : Nat] : ⋆ ⇒ (Parity-Elim (parity n) (λ _ ⇒ ⋆) Unit Empty)

one   : Nat ⇒ (suc zero)
two   : Nat ⇒ (suc one)
three : Nat ⇒ (suc two)
four  : Nat ⇒ (suc three)
five  : Nat ⇒ (suc four)
six   : Nat ⇒ (suc five)

even-6 : even six ⇒ tt

even-5-neg : neg (even five) ⇒ (λ z ⇒ z)

there-is-an-even-number : Prod Nat even ⇒ (prod six even-6)

Or [A B : ⋆] : ⋆ ⇒ (Prod Bool (λ b ⇒ ITE b A B))

left  [A B : ⋆] [x : A] : Or A B ⇒ (prod true  x)
right [A B : ⋆] [x : B] : Or A B ⇒ (prod false x)

case [A B C : ⋆] [f : A → C] [g : B → C] [x : Or A B] : C ⇒ (
  (Bool-Elim (fst x) (λ b ⇒ ITE b A B → C) f g) (snd x)
)