dvach.ctt

module dvach where

data nat
  = zero
  | succ (n : nat)

name : U = undefined

-- визначення 39
data Forall (lang : U)
  = fibrant (n : nat)
  | variable (x : name) (l : nat)
  | pi (x : name) (l : nat) (f : lang)
  | lambda (x : name) (l : nat) (f : lang)
  | application (f a : lang)

-- визначення 42
data Sigma (lang : U)
  = sigma (n : name) (a b : lang)
  | pair (a b : lang)
  | fst (p : lang)
  | snd (p : lang)

-- ↓↓↓ тут ↓↓↓
maxim (lang : U) : Forall lang -> Sigma lang =
  ?
-- ↑↑↑ тут ↑↑↑