inductive-recursive universe for dependent types

gistfile1.hs

module IRDTT where
open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )
open import Data.Sum public using ( _⊎_ ; inj₁ ; inj₂ )

record ⊤ {a} : Set a where
  constructor tt

data Type {a} : Set (suc a)
⟦_⟧ : ∀{a} → Type {a} → Set a

data Type {a} where
  `[_] : Set a → Type
  `⊤ : Type
  _`⊎_ : (τ τ′ : Type) → Type
  `Σ `Π : (τ : Type) (τ′ : ⟦ τ ⟧ → Type) → Type

⟦ `[ A ]  ⟧ = A
⟦ `⊤ ⟧ = ⊤
⟦ τ `⊎ τ′ ⟧ = ⟦ τ ⟧ ⊎ ⟦ τ′ ⟧
⟦ `Σ τ τ′ ⟧ = Σ ⟦ τ ⟧ λ ρ → ⟦ τ′ ρ ⟧
⟦ `Π τ τ′ ⟧ = (ρ : ⟦ τ ⟧) → ⟦ τ′ ρ ⟧

Id : Type
Id = `Π `[ Set ] λ A → `Π `[ Lift A ] λ _ → `[ Lift A ]

id : ⟦ Id ⟧
id A x = x

{-
⟦ Id ⟧ = (A : Set) → Lift A → Lift A
can we make it (A : Set) → A → A ?
-}