module universe where

data Bool : Set where
  tt : Bool
  ff : Bool

data ⊤ : Set where
  true : ⊤ 


data ⊥ : Set where


data ℕ : Set where
  Z : ℕ 
  S : ℕ -> ℕ 


data Σ (A : Set) (B : A -> Set ) : Set where
  p : (a : A) -> B a -> Σ A B


data Π (A : Set) (B : A -> Set ) : Set where
  lambda : ((a : A) -> B a) -> Π A B

data _+_ (A B : Set) : Set where
  inl : A -> A + B
  inr : B -> A + B


mutual
  data U : Set where
     tophat  : U
     ⊥hat    : U
     Boolhat : U
     ℕhat    : U
     _+hat_  : U -> U -> U
     Σhat    : ( a : U) -> (T a -> U ) -> U
     Πhat    : ( a : U) -> (T a -> U ) -> U

  T : U -> Set
  T tophat      = ⊤ 
  T ⊥hat        = ⊥ 
  T Boolhat     = Bool
  T ℕhat        = ℕ
  T (a +hat b)  = T a + T b
  T (Σhat a b)  = Σ (T a) (\x -> T (b x))
  T (Πhat a b)  = Π (T a) (\x -> T (b x))