inductive-recursive universe for dependent types

gistfile1.txt

open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
  renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
    renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
module IRDTT where

{-
Solution to question posed by Larry Diehl here:
https://twitter.com/larrytheliquid/status/257262281358983168

Idea based on Conor McBride's:
https://personal.cis.strath.ac.uk/conor.mcbride/pub/Hmm/Hier.agda
Similar constructions also exist here:
http://red.cs.nott.ac.uk/~dwm/univ.agda
http://code.haskell.org/~dolio/agda-share/universes/Hierarchy.agda

Huge thank you to the following people for helpful suggestions:
Conor McBride, Darin Morrison, Daniel Peebles, and Andrea Vezzosi.
-}


data Type′ (U : Set) (El : U → Set) : Set
⟦_⟧′ : {U : Set} {El : U → Set} → Type′ U El → Set

data Type′ U El where
  `Type : Type′ U El
  `⟦_⟧ : U → Type′ U El
  `⊥ `⊤ `Bool : Type′ U El
  `Π `Σ : (τ : Type′ U El) (τ′ : ⟦ τ ⟧′ → Type′ U El) → Type′ U El

⟦_⟧′ {U = U} `Type = U
⟦_⟧′ {El = El} `⟦ τ ⟧ = El τ
⟦ `⊥ ⟧′ = ⊥
⟦ `⊤ ⟧′ = ⊤
⟦ `Bool ⟧′ = Bool
⟦ `Π τ τ′ ⟧′ = (v : ⟦ τ ⟧′) → ⟦ τ′ v ⟧′
⟦ `Σ τ τ′ ⟧′ = Σ ⟦ τ ⟧′ λ v → ⟦ τ′ v ⟧′

----------------------------------------------------------------------

_`→_ : ∀{U El} (τ τ′ : Type′ U El) → Type′ U El
τ `→ τ′ = `Π τ λ _ → τ′

_`×_ : ∀{U El} (τ τ′ : Type′ U El) → Type′ U El
τ `× τ′ = `Π `Bool λ b → if b then τ else τ′

_`⊎_ : ∀{U El} (τ τ′ : Type′ U El) → Type′ U El
τ `⊎ τ′ = `Σ `Bool λ b → if b then τ else τ′

----------------------------------------------------------------------

Type : {n : ℕ} → Set
_⟦_⟧ : (n : ℕ) → Type {n} → Set

Type {zero} = Type′ ⊥ ⊥-elim
Type {suc n} = Type′ Type (_⟦_⟧ n)

_⟦_⟧ (zero) e = ⟦ e ⟧′
_⟦_⟧ (suc n) e = ⟦ e ⟧′

----------------------------------------------------------------------

and : ∀{n} → suc n ⟦ `Bool `→ (`Bool `→ `Bool) ⟧
and true b = b
and false b = false

id : ∀{n} → suc n ⟦ `Π `Type (λ A → `⟦ A ⟧ `→ `⟦ A ⟧) ⟧
id A x = x