inductive-recursive universe for dependent types (no unicode)

gistfile1.hs

module IRDTT where
open import Level
open import Data.Product using ( _,_ )
  renaming ( Σ to Sigma ; proj₁ to proj1 ; proj₂ to proj2  )
open import Data.Sum
  renaming ( _⊎_ to Sum ; inj₁ to inj1 ; inj₂ to inj2 )

record Unit {a} : Set a where
  constructor tt

data Type {a} : Set (suc a)
El : forall{a} -> Type {a} -> Set a

data Type {a} where
  `[_] : Set a -> Type
  `Unit : Type
  `Sum : (A B : Type) -> Type
  `Sigma `Pi : (A : Type) (B : El A -> Type) -> Type

El `[ A ] = A
El `Unit = Unit
El (`Sum A B) = Sum (El A) (El B)
El (`Sigma A B) = Sigma (El A) \ x -> El (B x)
El (`Pi A B) = (x : El A) -> El (B x)

Id : Type
Id = `Pi `[ Set ] \ A -> `Pi `[ Lift A ] \ _ -> `[ Lift A ]

id : El Id
id A x = x

{-
El Id = (A : Set) -> Lift A -> Lift A
can we make it (A : Set) -> A -> A ?
-}