NbE for CCC

CCCNbE.agda

open import Data.Unit
open import Data.Product

infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_

data Obj : Set where
  ∙    : Obj
  base : Obj
  _*_  : Obj → Obj → Obj
  _⇒_  : Obj → Obj → Obj

variable
 x y z z' : Obj

data Hom : Obj → Obj → Set where
  id    : Hom x x
  _∘_   : Hom y z → Hom x y → Hom x z
  !     : Hom x ∙
  ⟨_,_⟩ : Hom x y → Hom x z → Hom x (y * z)
  π₁    : Hom (x * y) x
  π₂    : Hom (x * y) y
  lam   : Hom (x * y) z → Hom x (y ⇒ z)
  app   : Hom x (y ⇒ z) → Hom (x * y) z

infix 5 _∘π₁ _∘π₂

data Var : Obj → Obj → Set where
  id∙    : Var ∙ ∙
  id⇒    : Var (x ⇒ y) (x ⇒ y)
  idbase : Var base base
  _∘π₁   : Var x y → Var (x * z) y
  _∘π₂   : Var x y → Var (z * x) y

Ren : Obj → Obj → Set
Ren x y = ∀ z → Var y z → Var x z

idᵣ : Ren x x
idᵣ z f = f

_∘ᵣ_ : Ren y z → Ren x y → Ren x z; infixr 4 _∘ᵣ_
f ∘ᵣ g = λ z h → g z (f z h)

π₁ᵣ : Ren (x * y) x
π₁ᵣ _ = _∘π₁

π₂ᵣ : Ren (x * y) y
π₂ᵣ _ = _∘π₂

⟨_,ᵣ_⟩ : Ren x y → Ren x z → Ren x (y * z)
⟨_,ᵣ_⟩ f g a (h ∘π₁) = f a h
⟨_,ᵣ_⟩ f g a (h ∘π₂) = g a h

data Nf : Obj → Obj → Set
data Ne : Obj → Obj → Set

data Nf where
  lam   : Nf (x * y) z → Nf x (y ⇒ z)
  ⟨_,_⟩ : Nf x y → Nf x z → Nf x (y * z)
  !     : Nf x ∙
  ne    : Ne x base → Nf x base

data Ne where
  var : Var x y → Ne x y
  π₁∘ : Ne x (y * z) → Ne x y
  π₂∘ : Ne x (y * z) → Ne x z
  app : Ne x (y ⇒ z) → Nf x y → Ne x z

Nfᵣ  : Ren z z' → Nf z' x → Nf z x
Neᵣ  : Ren z z' → Ne z' x → Ne z x
Nfᵣ f (lam g)   = lam (Nfᵣ ⟨ f ∘ᵣ π₁ᵣ ,ᵣ π₂ᵣ ⟩ g)
Nfᵣ f ⟨ g , h ⟩ = ⟨ Nfᵣ f g , Nfᵣ f h ⟩
Nfᵣ f !         = !
Nfᵣ f (ne g)    = ne (Neᵣ f g)
Neᵣ f (var g)   = var (f _ g)
Neᵣ f (π₁∘ g)   = π₁∘ (Neᵣ f g)
Neᵣ f (π₂∘ g)   = π₂∘ (Neᵣ f g)
Neᵣ f (app g h) = app (Neᵣ f g) (Nfᵣ f h)

⟦_⟧ᵒ : Obj → Obj → Set
⟦ ∙     ⟧ᵒ = λ _ → ⊤
⟦ base  ⟧ᵒ = λ x → Nf x base
⟦ x * y ⟧ᵒ = λ z → ⟦ x ⟧ᵒ z × ⟦ y ⟧ᵒ z
⟦ x ⇒ y ⟧ᵒ = λ z → (∀ z' → Ren z' z → ⟦ x ⟧ᵒ z' → ⟦ y ⟧ᵒ z')

⟦⟧ᵒʳ : Ren z z' → ∀ x → ⟦ x ⟧ᵒ z' → ⟦ x ⟧ᵒ z
⟦⟧ᵒʳ f (∙    ) x̂       = tt
⟦⟧ᵒʳ f (base ) x̂       = Nfᵣ f x̂
⟦⟧ᵒʳ f (x * y) (x̂ , ŷ) = ⟦⟧ᵒʳ f x x̂ , ⟦⟧ᵒʳ f y ŷ
⟦⟧ᵒʳ f (x ⇒ y) f̂       = λ z' g → f̂ z' (f ∘ᵣ g)

⟦_⟧ʰ : Hom x y → (∀ {z} → ⟦ x ⟧ᵒ z → ⟦ y ⟧ᵒ z)
⟦ id        ⟧ʰ x̂       = x̂
⟦ f ∘ g     ⟧ʰ x̂       = ⟦ f ⟧ʰ (⟦ g ⟧ʰ x̂)
⟦ !         ⟧ʰ x̂       = tt
⟦ ⟨ f , g ⟩ ⟧ʰ x̂       = ⟦ f ⟧ʰ x̂ , ⟦ g ⟧ʰ x̂
⟦ π₁        ⟧ʰ (x̂ , ŷ) = x̂
⟦ π₂        ⟧ʰ (x̂ , ŷ) = ŷ
⟦ lam {x} f ⟧ʰ x̂       = λ _ g ŷ → ⟦ f ⟧ʰ (⟦⟧ᵒʳ g x x̂ , ŷ)
⟦ app f     ⟧ʰ (x̂ , ŷ) = ⟦ f ⟧ʰ x̂ _ idᵣ ŷ


-- NOTE: the general identity morphism is *not* neutral,
-- hence we have to define the unquoting of the identity
-- morphism separately as "uId"

uId : ⟦ x ⟧ᵒ x
q   : ⟦ x ⟧ᵒ y → Nf y x
u   : ∀ {x y} → Ne y x → ⟦ x ⟧ᵒ y

uId {∙}           = u (var id∙)
uId {base}        = u (var idbase)
uId {x ⇒ y}       = u (var id⇒)
uId {x * y}       = ⟦⟧ᵒʳ π₁ᵣ x (uId {x}) , ⟦⟧ᵒʳ π₂ᵣ y (uId {y})

q {∙}     x̂       = !
q {base}  x̂       = x̂
q {x * y} (x̂ , ŷ) = ⟨ q x̂ , q ŷ ⟩
q {x ⇒ y} {z} f̂   = lam (q {y} (f̂ _ π₁ᵣ (⟦⟧ᵒʳ π₂ᵣ x (uId {x}))))

u {∙}     f       = tt
u {base}  f       = ne f
u {x * y} f       = u (π₁∘ f) , u (π₂∘ f)
u {x ⇒ y} f       = λ z g x̂ → u {y} (app (Neᵣ g f) (q {x} x̂))

nf : Hom x y → Nf x y
nf {x} f = q (⟦ f ⟧ʰ (uId {x}))