------------------------------------------------------------
-- Naturals

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

one   : Nat ⇒ (suc zero)
two   : Nat ⇒ (suc one)
three : Nat ⇒ (suc two)

------------------------------------------------------------
-- Binary trees

data Tree : [A : ⋆] → ⋆ ⇒
  { leaf : Tree A | node : Tree A → A → Tree A → Tree A }

------------------------------------------------------------
-- Empty types

data Empty : ⋆ ⇒ { }

------------------------------------------------------------
-- Ordered lists

record Unit : ⋆ ⇒ tt { }

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

data Lift : ⋆ ⇒
  { bot : Lift | lift : Nat → Lift | top : Lift }

le' [l1 : Lift] : Lift → ⋆ ⇒ (
  Lift-Elim
    l1
    (λ _ ⇒ Lift → ⋆)
    (λ _     ⇒ Unit)
    (λ n1 l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ n2 ⇒ le n1 n2) Unit)
    (λ l2    ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ _  ⇒ Empty)    Unit)
)

data OList : [low upp : Lift] → ⋆ ⇒
  { onil  : le' low upp → OList low upp
  | ocons : [n : Nat] → OList (lift n) upp → le' low (lift n) → OList low upp
  }

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

------------------------------------------------------------
-- Dependent products

record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
  prod {fst : A, snd : B fst}