1 ------------------------------------------------------------
4 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
8 three : Nat ⇒ (suc two)
10 ------------------------------------------------------------
13 data Tree : [A : ⋆] → ⋆ ⇒
14 { leaf : Tree A | node : Tree A → A → Tree A → Tree A }
16 ------------------------------------------------------------
21 ------------------------------------------------------------
24 record Unit : ⋆ ⇒ tt { }
26 le [n : Nat] : Nat → ⋆ ⇒ (
31 (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Empty (λ m' _ ⇒ f m'))
35 { bot : Lift | lift : Nat → Lift | top : Lift }
37 le' [l1 : Lift] : Lift → ⋆ ⇒ (
42 (λ n1 l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ n2 ⇒ le n1 n2) Unit)
43 (λ l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ _ ⇒ Empty) Unit)
46 data OList : [low upp : Lift] → ⋆ ⇒
47 { onil : le' low upp → OList low upp
48 | ocons : [n : Nat] → OList (lift n) upp → le' low (lift n) → OList low upp
51 data List : [A : ⋆] → ⋆ ⇒
52 { nil : List A | cons : A → List A → List A }
54 ------------------------------------------------------------
57 record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
58 prod {fst : A, snd : B fst}