Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid
Last active April 28, 2016 13:42
Show Gist options
  • Save larrytheliquid/3909860 to your computer and use it in GitHub Desktop.
Save larrytheliquid/3909860 to your computer and use it in GitHub Desktop.
inductive-recursive universe for dependent types
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment