open import Cat.CartesianClosed.Free.Signature using (module types)
open import Cat.Diagram.Exponential
open import Cat.Cartesian
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor

module Cat.CartesianClosed.Solver

Solver for Cartesian closed categoriesπŸ”—

  {o β„“} {C : Precategory o β„“} (cart : Cartesian-category C) (cc : Cartesian-closed C cart)
        where

open Cartesian-category cart
open Cartesian-closed cc
open types Ob public

We can write a solver for a Cartesian closed category β€” a metaprogram which identifies two morphisms when they differ only by applications of the CCC laws β€” by re-using the idea for our implementation of normalisation by evaluation for free Cartesian closed categories: in order to identify two morphisms in it suffices to identify their β€œquoted” versions in the free CCC on which we can do automatically by normalising them.

The reason we don’t directly re-use the implementation is that the underlying graph of an arbitrary CCC does not form a -signature unless the category is strict, which is too limiting an assumption. In turn, the requirement that the objects form a set is necessary to obtain proper presheaves of normals and neutrals. Instead, this module takes a slightly β€œwilder” approach, omitting a lot of unnecessary coherence. We also work with an unquotiented representation of morphisms.

First, recall the definition of simple types: they are generated from the objects of by freely adding product types, function types, and a unit type. We define contexts as lists of simple types.

data Cx : Type o where
  βˆ…   : Cx
  _,_ : Cx β†’ Ty β†’ Cx

private variable
  Ξ“ Ξ” Θ : Cx
  Ο„ Οƒ ρ : Ty

Using the Cartesian closed structure of we can interpret types and contexts in terms of the structural morphisms: for example, the empty context is interpreted by the terminal object.

⟦_βŸ§α΅— : Ty β†’ Ob
⟦_⟧ᢜ : Cx β†’ Ob

⟦ X `Γ— Y βŸ§α΅— = ⟦ X βŸ§α΅— βŠ—β‚€ ⟦ Y βŸ§α΅—
⟦ X `β‡’ Y βŸ§α΅— = [ ⟦ X βŸ§α΅— , ⟦ Y βŸ§α΅— ]
⟦ `⊀  βŸ§α΅—    = top
⟦ ` X βŸ§α΅—    = X

⟦ Ξ“ , Ο„ ⟧ᢜ = ⟦ Ξ“ ⟧ᢜ βŠ—β‚€ ⟦ Ο„ βŸ§α΅—
⟦ βˆ… ⟧ᢜ     = top

The idea is then to write a faithful representation of the way morphisms in a CCC appear in equational goals (in terms of identities, compositions, the evaluation morphism, and so on), then define a sound normalisation function for these. Note that since this is a metaprogram, our syntax for morphisms does not need to actually respect the laws of a CCC (i.e. it does not need to be a higher inductive type). It’s just a big indexed inductive type with constructors for all the β€˜primitive’ morphism formers for a terminal object, products, and exponential objects, with an additional constructor for morphisms from the base category.

data Mor : Ty β†’ Ty β†’ Type (o βŠ” β„“) where
  -- Generators:
  `_   : βˆ€ {x y} β†’ Hom ⟦ x βŸ§α΅— ⟦ y βŸ§α΅— β†’ Mor x y

  -- A CCC is a category:
  `id  : Mor Οƒ Οƒ
  _`∘_ : Mor Οƒ ρ β†’ Mor Ο„ Οƒ β†’ Mor Ο„ ρ

  -- A CCC has a terminal object:
  `!   : Mor Ο„ `⊀

  -- A CCC has products:
  `π₁  : Mor (Ο„ `Γ— Οƒ) Ο„
  `Ο€β‚‚  : Mor (Ο„ `Γ— Οƒ) Οƒ
  _`,_ : Mor Ο„ Οƒ β†’ Mor Ο„ ρ β†’ Mor Ο„ (Οƒ `Γ— ρ)

  -- A CCC has exponentials:
  `ev  : Mor ((Ο„ `β‡’ Οƒ) `Γ— Ο„) Οƒ
  `Ζ›   : Mor (Ο„ `Γ— Οƒ) ρ β†’ Mor Ο„ (Οƒ `β‡’ ρ)

infixr 20 _`∘_
infixr 19 _`,_ _`βŠ—β‚_
infix 25 `_

pattern _`βŠ—β‚_ f g = f `∘ `π₁ `, g `∘ `Ο€β‚‚
pattern `unlambda f = `ev `∘ (f `βŠ—β‚ `id)

We can interpret a formal morphism from to as a map in and this interpretation definitionally sends each constructor to its corresponding operation.

⟦_⟧ᡐ : Mor Ο„ Οƒ β†’ Hom ⟦ Ο„ βŸ§α΅— ⟦ Οƒ βŸ§α΅—
⟦ ` x     ⟧ᡐ = x
⟦ `id     ⟧ᡐ = id
⟦ m `∘ m₁ ⟧ᡐ = ⟦ m ⟧ᡐ ∘ ⟦ m₁ ⟧ᡐ
⟦ `π₁     ⟧ᡐ = π₁
⟦ `Ο€β‚‚     ⟧ᡐ = Ο€β‚‚
⟦ m `, m₁ ⟧ᡐ = ⟨ ⟦ m ⟧ᡐ , ⟦ m₁ ⟧ᡐ ⟩
⟦ `ev     ⟧ᡐ = ev
⟦ `Ζ› m    ⟧ᡐ = Ζ› ⟦ m ⟧ᡐ
⟦ `!      ⟧ᡐ = !
The bulk of this module is the implementation of normalisation by evaluation for the representation of morphisms above. We refer the reader to the same construction for free Cartesian closed categories over a for more details. 
data Var : Cx β†’ Ty β†’ Type o where
  stop : Var (Ξ“ , Ο„) Ο„
  pop  : Var Ξ“ Ο„ β†’ Var (Ξ“ , Οƒ) Ο„

⟦_⟧ⁿ : Var Ξ“ Ο„ β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ο„ βŸ§α΅—
⟦ stop ⟧ⁿ  = Ο€β‚‚
⟦ pop x ⟧ⁿ = ⟦ x ⟧ⁿ ∘ π₁

data Ren : Cx β†’ Cx β†’ Type (o βŠ” β„“) where
  stop : Ren Ξ“ Ξ“
  drop : Ren Ξ“ Ξ” β†’ Ren (Ξ“ , Ο„) Ξ”
  keep : Ren Ξ“ Ξ” β†’ Ren (Ξ“ , Ο„) (Ξ” , Ο„)

_∘ʳ_ : βˆ€ {Ξ“ Ξ” Θ} β†’ Ren Ξ“ Ξ” β†’ Ren Ξ” Θ β†’ Ren Ξ“ Θ
stop   ∘ʳ ρ      = ρ
drop Οƒ ∘ʳ ρ      = drop (Οƒ ∘ʳ ρ)
keep Οƒ ∘ʳ stop   = keep Οƒ
keep Οƒ ∘ʳ drop ρ = drop (Οƒ ∘ʳ ρ)
keep Οƒ ∘ʳ keep ρ = keep (Οƒ ∘ʳ ρ)

ren-var : βˆ€ {Ξ“ Ξ” Ο„} β†’ Ren Ξ“ Ξ” β†’ Var Ξ” Ο„ β†’ Var Ξ“ Ο„
ren-var stop     v       = v
ren-var (drop Οƒ) v       = pop (ren-var Οƒ v)
ren-var (keep Οƒ) stop    = stop
ren-var (keep Οƒ) (pop v) = pop (ren-var Οƒ v)

⟦_⟧ʳ : Ren Ξ“ Ξ” β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ξ” ⟧ᢜ
⟦ stop   ⟧ʳ = id
⟦ drop r ⟧ʳ = ⟦ r ⟧ʳ ∘ π₁
⟦ keep r ⟧ʳ = ⟦ r ⟧ʳ βŠ—β‚ id

data Nf           : Cx β†’ Ty β†’ Type (o βŠ” β„“)
data Ne           : Cx β†’ Ty β†’ Type (o βŠ” β„“)
data Sub (Ξ“ : Cx) : Cx β†’ Type (o βŠ” β„“)

data Nf where
  lam  : Nf (Ξ“ , Ο„) Οƒ       β†’ Nf Ξ“ (Ο„ `β‡’ Οƒ)
  pair : Nf Ξ“ Ο„ β†’ Nf Ξ“ Οƒ    β†’ Nf Ξ“ (Ο„ `Γ— Οƒ)
  unit :                      Nf Ξ“ `⊀
  ne   : βˆ€ {x} β†’ Ne Ξ“ (` x) β†’ Nf Ξ“ (` x)

data Ne where
  var  : Var Ξ“ Ο„ β†’ Ne Ξ“ Ο„
  app  : Ne Ξ“ (Ο„ `β‡’ Οƒ) β†’ Nf Ξ“ Ο„ β†’ Ne Ξ“ Οƒ
  fstβ‚™ : Ne Ξ“ (Ο„ `Γ— Οƒ) β†’ Ne Ξ“ Ο„
  sndβ‚™ : Ne Ξ“ (Ο„ `Γ— Οƒ) β†’ Ne Ξ“ Οƒ
  hom  : βˆ€ {Ξ” a} β†’ Hom ⟦ Ξ” ⟧ᢜ a β†’ Sub Ξ“ Ξ” β†’ Ne Ξ“ (` a)

data Sub Ξ“ where
  βˆ…   : Sub Ξ“ βˆ…
  _,_ : Sub Ξ“ Ξ” β†’ Nf Ξ“ Ο„ β†’ Sub Ξ“ (Ξ” , Ο„)

ren-ne  : βˆ€ {Ξ“ Ξ” Ο„} β†’ Ren Ξ” Ξ“ β†’ Ne  Ξ“ Ο„ β†’ Ne  Ξ” Ο„
ren-nf  : βˆ€ {Ξ“ Ξ” Ο„} β†’ Ren Ξ” Ξ“ β†’ Nf  Ξ“ Ο„ β†’ Nf  Ξ” Ο„
ren-sub : βˆ€ {Ξ“ Ξ” Θ} β†’ Ren Ξ” Ξ“ β†’ Sub Ξ“ Θ β†’ Sub Ξ” Θ

ren-ne Οƒ (hom h a) = hom h (ren-sub Οƒ a)

ren-ne Οƒ (var v)   = var  (ren-var Οƒ v)
ren-ne Οƒ (app f a) = app  (ren-ne Οƒ f) (ren-nf Οƒ a)
ren-ne Οƒ (fstβ‚™ a)  = fstβ‚™ (ren-ne Οƒ a)
ren-ne Οƒ (sndβ‚™ a)  = sndβ‚™ (ren-ne Οƒ a)

ren-nf Οƒ (lam n)    = lam  (ren-nf (keep Οƒ) n)
ren-nf Οƒ (pair a b) = pair (ren-nf Οƒ a) (ren-nf Οƒ b)
ren-nf Οƒ (ne x)     = ne   (ren-ne Οƒ x)
ren-nf Οƒ unit       = unit

ren-sub ρ βˆ…       = βˆ…
ren-sub ρ (Οƒ , x) = ren-sub ρ Οƒ , ren-nf ρ x

⟦_βŸ§β‚™  : Nf  Ξ“ Ο„ β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ο„ βŸ§α΅—
⟦_βŸ§β‚›  : Ne  Ξ“ Ο„ β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ο„ βŸ§α΅—
⟦_⟧ᡣ  : Sub Ξ“ Ξ” β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ξ” ⟧ᢜ

⟦ lam h    βŸ§β‚™ = Ζ› ⟦ h βŸ§β‚™
⟦ pair a b βŸ§β‚™ = ⟨ ⟦ a βŸ§β‚™ , ⟦ b βŸ§β‚™ ⟩
⟦ ne x     βŸ§β‚™ = ⟦ x βŸ§β‚›
⟦ unit     βŸ§β‚™ = !

⟦ var x   βŸ§β‚› = ⟦ x ⟧ⁿ
⟦ app f x βŸ§β‚› = ev ∘ ⟨ ⟦ f βŸ§β‚› , ⟦ x βŸ§β‚™ ⟩
⟦ fstβ‚™ h  βŸ§β‚› = π₁ ∘ ⟦ h βŸ§β‚›
⟦ sndβ‚™ h  βŸ§β‚› = Ο€β‚‚ ∘ ⟦ h βŸ§β‚›
⟦ hom h a βŸ§β‚› = h ∘ ⟦ a ⟧ᡣ

⟦ βˆ…     ⟧ᡣ = !
⟦ Οƒ , n ⟧ᡣ = ⟨ ⟦ Οƒ ⟧ᡣ , ⟦ n βŸ§β‚™ ⟩

⟦⟧-∘ʳ   : (ρ : Ren Ξ“ Ξ”) (Οƒ : Ren Ξ” Θ) β†’ ⟦ ρ ∘ʳ Οƒ ⟧ʳ ≑ ⟦ Οƒ ⟧ʳ ∘ ⟦ ρ ⟧ʳ

ren-⟦⟧ⁿ : (ρ : Ren Ξ” Ξ“) (v : Var Ξ“ Ο„) β†’ ⟦ ren-var ρ v ⟧ⁿ ≑ ⟦ v ⟧ⁿ ∘ ⟦ ρ ⟧ʳ
ren-βŸ¦βŸ§β‚› : (ρ : Ren Ξ” Ξ“) (t : Ne Ξ“ Ο„)  β†’ ⟦ ren-ne ρ t  βŸ§β‚› ≑ ⟦ t βŸ§β‚› ∘ ⟦ ρ ⟧ʳ
ren-βŸ¦βŸ§β‚™ : (ρ : Ren Ξ” Ξ“) (t : Nf Ξ“ Ο„)  β†’ ⟦ ren-nf ρ t  βŸ§β‚™ ≑ ⟦ t βŸ§β‚™ ∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ᡣ : (ρ : Ren Ξ” Ξ“) (Οƒ : Sub Ξ“ Θ) β†’ ⟦ ren-sub ρ Οƒ ⟧ᡣ ≑ ⟦ Οƒ ⟧ᡣ ∘ ⟦ ρ ⟧ʳ

⟦⟧-∘ʳ stop Οƒ = intror refl
⟦⟧-∘ʳ (drop ρ) Οƒ = pushl (⟦⟧-∘ʳ ρ Οƒ)
⟦⟧-∘ʳ (keep ρ) stop = introl refl
⟦⟧-∘ʳ (keep ρ) (drop Οƒ) = pushl (⟦⟧-∘ʳ ρ Οƒ) βˆ™ sym (pullr Ο€β‚βˆ˜βŸ¨βŸ©)
⟦⟧-∘ʳ (keep ρ) (keep Οƒ) = sym $ ⟨⟩-unique
  (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pulll (sym (⟦⟧-∘ʳ ρ Οƒ)))
  (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ idl _)

ren-⟦⟧ⁿ stop v           = intror refl
ren-⟦⟧ⁿ (drop ρ) v       = pushl (ren-⟦⟧ⁿ ρ v)
ren-⟦⟧ⁿ (keep ρ) stop    = sym (Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ idl _)
ren-⟦⟧ⁿ (keep ρ) (pop v) = pushl (ren-⟦⟧ⁿ ρ v) βˆ™ sym (pullr Ο€β‚βˆ˜βŸ¨βŸ©)

ren-βŸ¦βŸ§β‚› ρ (var x) = ren-⟦⟧ⁿ ρ x
ren-βŸ¦βŸ§β‚› ρ (app f x) = apβ‚‚ _∘_ refl
  (apβ‚‚ ⟨_,_⟩ (ren-βŸ¦βŸ§β‚› ρ f) (ren-βŸ¦βŸ§β‚™ ρ x) βˆ™ sym (⟨⟩∘ _))
  βˆ™ pulll refl
ren-βŸ¦βŸ§β‚› ρ (fstβ‚™ t) = pushr (ren-βŸ¦βŸ§β‚› ρ t)
ren-βŸ¦βŸ§β‚› ρ (sndβ‚™ t) = pushr (ren-βŸ¦βŸ§β‚› ρ t)
ren-βŸ¦βŸ§β‚› ρ (hom x a) = pushr (ren-⟦⟧ᡣ ρ a)

ren-βŸ¦βŸ§β‚™ ρ (lam t) =
    ap Ζ› (ren-βŸ¦βŸ§β‚™ (keep ρ) t)
  βˆ™ sym (unique _ (apβ‚‚ _∘_ refl rem₁ βˆ™ pulll (commutes ⟦ t βŸ§β‚™)))
  where
  rem₁ : (⟦ lam t βŸ§β‚™ ∘ ⟦ ρ ⟧ʳ) βŠ—β‚ id ≑ (⟦ lam t βŸ§β‚™ βŠ—β‚ id) ∘ ⟦ ρ ⟧ʳ βŠ—β‚ id
  rem₁ = Bifunctor.first∘first Γ—-functor

ren-βŸ¦βŸ§β‚™ ρ (pair a b) = apβ‚‚ ⟨_,_⟩ (ren-βŸ¦βŸ§β‚™ ρ a) (ren-βŸ¦βŸ§β‚™ ρ b) βˆ™ sym (⟨⟩∘ _)
ren-βŸ¦βŸ§β‚™ ρ (ne x) = ren-βŸ¦βŸ§β‚› ρ x
ren-βŸ¦βŸ§β‚™ ρ unit   = !-unique _

ren-⟦⟧ᡣ ρ βˆ…       = !-unique _
ren-⟦⟧ᡣ ρ (Οƒ , n) = apβ‚‚ ⟨_,_⟩ (ren-⟦⟧ᡣ ρ Οƒ) (ren-βŸ¦βŸ§β‚™ ρ n) βˆ™ sym (⟨⟩∘ _)

Tyα΅– : (Ο„ : Ty) (Ξ“ : Cx) β†’ Hom ⟦ Ξ“ ⟧ᢜ ⟦ Ο„ βŸ§α΅— β†’ Type (o βŠ” β„“)
Tyα΅– (Ο„ `Γ— Οƒ) Ξ“ h = Tyα΅– Ο„ Ξ“ (π₁ ∘ h) Γ— Tyα΅– Οƒ Ξ“ (Ο€β‚‚ ∘ h)
Tyα΅– `⊀ Ξ“ h = Lift _ ⊀
Tyα΅– (Ο„ `β‡’ Οƒ) Ξ“ h =
  βˆ€ {Ξ”} (ρ : Ren Ξ” Ξ“) {a}
  β†’ Tyα΅– Ο„ Ξ” a
  β†’ Tyα΅– Οƒ Ξ” (ev ∘ ⟨ h ∘ ⟦ ρ ⟧ʳ , a ⟩)
Tyα΅– (` x)    Ξ“ h = Ξ£ (Ne Ξ“ (` x)) Ξ» n β†’ ⟦ n βŸ§β‚› ≑ h

data Subα΅– : βˆ€ Ξ“ Ξ” β†’ Hom ⟦ Ξ” ⟧ᢜ ⟦ Ξ“ ⟧ᢜ β†’ Type (o βŠ” β„“) where
  βˆ…   : βˆ€ {i} β†’ Subα΅– βˆ… Ξ” i
  _,_ : βˆ€ {h} β†’ Subα΅– Ξ“ Ξ” (π₁ ∘ h) β†’ Tyα΅– Οƒ Ξ” (Ο€β‚‚ ∘ h) β†’ Subα΅– (Ξ“ , Οƒ) Ξ” h

tyα΅–βŸ¨_⟩ : βˆ€ {Ο„ Ξ“ h h'} β†’ h ≑ h' β†’ Tyα΅– Ο„ Ξ“ h β†’ Tyα΅– Ο„ Ξ“ h'
tyα΅–βŸ¨_⟩ {Ο„ `Γ— Οƒ} p (a , b)   = tyα΅–βŸ¨ ap (π₁ ∘_) p ⟩tyα΅– a , tyα΅–βŸ¨ ap (Ο€β‚‚ ∘_) p ⟩tyα΅– b
tyα΅–βŸ¨_⟩ {Ο„ `β‡’ Οƒ} p Ξ½ ρ x     = tyα΅–βŸ¨ ap (Ξ» e β†’ ev ∘ ⟨ e ∘ ⟦ ρ ⟧ʳ , _ ⟩) p ⟩tyα΅– (Ξ½ ρ x)
tyα΅–βŸ¨_⟩ {` x} p (n , q) .fst = n
tyα΅–βŸ¨_⟩ {` x} p (n , q) .snd = q βˆ™ p
tyα΅–βŸ¨_⟩ {`⊀}  p (lift tt)    = lift tt

subα΅–βŸ¨_⟩ : βˆ€ {Ξ“ Ξ” h h'} β†’ h ≑ h' β†’ Subα΅– Ξ“ Ξ” h β†’ Subα΅– Ξ“ Ξ” h'
subα΅–βŸ¨_⟩ p βˆ…       = βˆ…
subα΅–βŸ¨_⟩ p (r , x) = subα΅–βŸ¨ ap (π₁ ∘_) p ⟩subα΅– r , tyα΅–βŸ¨ ap (Ο€β‚‚ ∘_) p ⟩tyα΅– x

ren-tyα΅–  : βˆ€ {Ξ” Ξ“ Ο„ m} (ρ : Ren Ξ” Ξ“) β†’ Tyα΅– Ο„ Ξ“ m  β†’ Tyα΅–  Ο„ Ξ” (m ∘ ⟦ ρ ⟧ʳ)
ren-subα΅– : βˆ€ {Ξ” Ξ“ Θ m} (ρ : Ren Θ Ξ”) β†’ Subα΅– Ξ“ Ξ” m β†’ Subα΅– Ξ“ Θ (m ∘ ⟦ ρ ⟧ʳ)

ren-tyα΅– {Ο„ = Ο„ `Γ— Οƒ} r (a , b)   =
    tyα΅–βŸ¨ sym (assoc _ _ _) ⟩tyα΅– (ren-tyα΅– r a)
  , tyα΅–βŸ¨ sym (assoc _ _ _) ⟩tyα΅– (ren-tyα΅– r b)
ren-tyα΅– {Ο„ = Ο„ `β‡’ Οƒ} r t {Θ} ρ {Ξ±} a =
  tyα΅–βŸ¨ ap (Ξ» e β†’ ev ∘ ⟨ e , Ξ± ⟩) (pushr (⟦⟧-∘ʳ ρ r)) ⟩tyα΅– (t (ρ ∘ʳ r) a)
ren-tyα΅– {Ο„ = ` x} r (f , p) = ren-ne r f , ren-βŸ¦βŸ§β‚› r f βˆ™ apβ‚‚ _∘_ p refl
ren-tyα΅– {Ο„ = `⊀} r (lift tt) = lift tt

ren-subα΅– r βˆ…       = βˆ…
ren-subα΅– r (c , x) =
    subα΅–βŸ¨ sym (assoc _ _ _) ⟩subα΅– (ren-subα΅– r c)
  , tyα΅–βŸ¨ sym (assoc _ _ _) ⟩tyα΅– (ren-tyα΅– r x)

reifyα΅–         : βˆ€ {h}                 β†’ Tyα΅– Ο„ Ξ“ h β†’ Nf Ξ“ Ο„
reflectα΅–       : (n : Ne Ξ“ Ο„)          β†’ Tyα΅– Ο„ Ξ“ ⟦ n βŸ§β‚›
reifyα΅–-correct : βˆ€ {h} (v : Tyα΅– Ο„ Ξ“ h) β†’ ⟦ reifyα΅– v βŸ§β‚™ ≑ h

reifyα΅– {Ο„ = Ο„ `Γ— s} (a , b) = pair (reifyα΅– a) (reifyα΅– b)
reifyα΅– {Ο„ = Ο„ `β‡’ s} f       = lam (reifyα΅– (f (drop stop) (reflectα΅– (var stop))))
reifyα΅– {Ο„ = ` x} d          = ne (d .fst)
reifyα΅– {Ο„ = `⊀} d           = unit

reflectα΅– {Ο„ = Ο„ `Γ— Οƒ} n     = reflectα΅– (fstβ‚™ n) , reflectα΅– (sndβ‚™ n)
reflectα΅– {Ο„ = Ο„ `β‡’ Οƒ} n ρ a = tyα΅–βŸ¨ apβ‚‚ (Ξ» e f β†’ ev ∘ ⟨ e , f ⟩) (ren-βŸ¦βŸ§β‚› ρ n) (reifyα΅–-correct a) ⟩tyα΅–
  (reflectα΅– (app (ren-ne ρ n) (reifyα΅– a)))
reflectα΅– {Ο„ = ` x}    n     = n , refl
reflectα΅– {Ο„ = `⊀}     _     = lift tt

reifyα΅–-correct {Ο„ = Ο„ `Γ— Οƒ} (a , b) = sym $
  ⟨⟩-unique (sym (reifyα΅–-correct a)) (sym (reifyα΅–-correct b))
reifyα΅–-correct {Ο„ = Ο„ `β‡’ Οƒ} {h = h} Ξ½ =
  Ζ› ⟦ reifyα΅– (Ξ½ (drop stop) (reflectα΅– (var stop))) βŸ§β‚™
    β‰‘βŸ¨ ap Ζ› (reifyα΅–-correct (Ξ½ (drop stop) (reflectα΅– (var stop)))) βŸ©β‰‘
  Ζ› (ev ∘ ⟨ h ∘ id ∘ π₁ , Ο€β‚‚ ⟩)
    β‰‘βŸ¨ apβ‚‚ (Ξ» a b β†’ Ζ› (ev ∘ ⟨ a , b ⟩)) (pulll (elimr refl)) (introl refl) βŸ©β‰‘
  Ζ› (unlambda h)
    β‰‘Λ˜βŸ¨ unique _ refl βŸ©β‰‘Λ˜
  h ∎
reifyα΅–-correct {Ο„ = ` x} d = d .snd
reifyα΅–-correct {Ο„ = `⊀}  d = !-unique _

private
  tickα΅– : βˆ€ {x y h} (m : Hom ⟦ x βŸ§α΅— ⟦ y βŸ§α΅—) β†’ Tyα΅– x Ξ“ h β†’ Tyα΅– y Ξ“ (m ∘ h)
  tickα΅– {x = x} {y = `⊀}  m a = lift tt
  tickα΅– {x = x} {y = ` Ο„} m a =
    hom {Ξ” = βˆ… , x} (m ∘ Ο€β‚‚) (βˆ… , reifyα΅– a) ,
    pullr Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ ap (m ∘_) (reifyα΅–-correct a)

  tickα΅– {y = Ο„ `Γ— Οƒ} m a =
      tyα΅–βŸ¨ pullr refl ⟩tyα΅– (tickα΅– (π₁ ∘ m) a)
    , tyα΅–βŸ¨ pullr refl ⟩tyα΅– (tickα΅– (Ο€β‚‚ ∘ m) a)

  tickα΅– {x = x} {y = Ο„ `β‡’ Οƒ} m a ρ y =
    tyα΅–βŸ¨ pullr (⟨⟩-unique (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ extendr Ο€β‚βˆ˜βŸ¨βŸ©) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©)) ⟩tyα΅–
    (tickα΅– {x = x `Γ— Ο„} (ev ∘ ⟨ m ∘ π₁ , Ο€β‚‚ ⟩)
      (tyα΅–βŸ¨ sym Ο€β‚βˆ˜βŸ¨βŸ© ⟩tyα΅– (ren-tyα΅– ρ a) , tyα΅–βŸ¨ sym Ο€β‚‚βˆ˜βŸ¨βŸ© ⟩tyα΅– y))

  morα΅– : βˆ€ {h} (e : Mor Ο„ Οƒ) (ρ : Tyα΅– Ο„ Ξ“ h) β†’ Tyα΅– Οƒ Ξ“ (⟦ e ⟧ᡐ ∘ h)
  morα΅– (` x) = tickα΅– x

  morα΅– `id      ρ = tyα΅–βŸ¨ introl refl ⟩tyα΅– ρ
  morα΅– (f `∘ g) ρ = tyα΅–βŸ¨ pulll refl ⟩tyα΅– (morα΅– f (morα΅– g ρ))

  morα΅– `!       ρ = lift tt
  morα΅– `π₁      ρ = ρ .fst
  morα΅– `Ο€β‚‚      ρ = ρ .snd
  morα΅– (e `, f) ρ = record
    { fst = tyα΅–βŸ¨ sym (pulll Ο€β‚βˆ˜βŸ¨βŸ©) ⟩tyα΅– (morα΅– e ρ)
    ; snd = tyα΅–βŸ¨ sym (pulll Ο€β‚‚βˆ˜βŸ¨βŸ©) ⟩tyα΅– (morα΅– f ρ)
    }

  morα΅– `ev (f , x) = tyα΅–βŸ¨ ap (ev ∘_) (sym (⟨⟩-unique (intror refl) refl)) ⟩tyα΅–
    (f stop x)

  morα΅– {h = h} (`Ζ› e) t r {h'} a = tyα΅–βŸ¨ sym p ⟩tyα΅– (morα΅– e
      ( tyα΅–βŸ¨ sym Ο€β‚βˆ˜βŸ¨βŸ© ⟩tyα΅– (ren-tyα΅– r t)
      , tyα΅–βŸ¨ sym Ο€β‚‚βˆ˜βŸ¨βŸ© ⟩tyα΅– a ))
    where
    p =
      ev ∘ ⟨ ((Ζ› ⟦ e ⟧ᡐ) ∘ h) ∘ ⟦ r ⟧ʳ , h' ⟩
        β‰‘βŸ¨ ap (ev ∘_) (sym (⟨⟩-unique (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pulll refl) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ idl _))) βŸ©β‰‘
      ev ∘ (Ζ› ⟦ e ⟧ᡐ βŠ—β‚ id) ∘ ⟨ h ∘ ⟦ r ⟧ʳ , h' ⟩
        β‰‘βŸ¨ pulll (commutes _) βŸ©β‰‘
      ⟦ e ⟧ᡐ ∘ ⟨ h ∘ ⟦ r ⟧ʳ , h' ⟩
        ∎

Putting the NbE pieces together, we get a normalisation function together with a proof of soundness, which allows us to write a solve function.

  mor-nf : Mor Ο„ Οƒ β†’ Nf (βˆ… , Ο„) Οƒ
  mor-nf m = reifyα΅– (morα΅– m (reflectα΅– (var stop)))

  mor-nf-sound : (m : Mor Ο„ Οƒ) β†’ ⟦ m ⟧ᡐ ≑ ⟦ mor-nf m βŸ§β‚™ ∘ ⟨ ! , id ⟩
  mor-nf-sound m = sym $
    ⟦ mor-nf m βŸ§β‚™ ∘ ⟨ ! , id ⟩ β‰‘βŸ¨ pushl (reifyα΅–-correct (morα΅– m (reflectα΅– (var stop)))) βŸ©β‰‘
    ⟦ m ⟧ᡐ ∘ Ο€β‚‚ ∘ ⟨ ! , id ⟩   β‰‘βŸ¨ elimr Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
    ⟦ m ⟧ᡐ                     ∎

abstract
  solve : (m n : Mor Ο„ Οƒ) β†’ mor-nf m ≑ mor-nf n β†’ ⟦ m ⟧ᡐ ≑ ⟦ n ⟧ᡐ
  solve m n p =
    ⟦ m ⟧ᡐ                     β‰‘βŸ¨ mor-nf-sound m βŸ©β‰‘
    ⟦ mor-nf m βŸ§β‚™ ∘ ⟨ ! , id ⟩ β‰‘βŸ¨ apβ‚‚ _∘_ (ap ⟦_βŸ§β‚™ p) refl βŸ©β‰‘
    ⟦ mor-nf n βŸ§β‚™ ∘ ⟨ ! , id ⟩ β‰‘βŸ¨ sym (mor-nf-sound n) βŸ©β‰‘
    ⟦ n ⟧ᡐ                     ∎

private module _ {W X Y Z} (f : Hom X Y) (g : Hom X Z) (h : Hom W X) where
  `W `X `Y `Z : Ty
  `W = ` W ; `X = ` X ; `Y = ` Y ; `Z = ` Z

  `f : Mor `X `Y
  `f = ` f

  `g : Mor `X `Z
  `g = ` g

  `h : Mor `W `X
  `h = ` h

We can then test that the solver subsumes the solver for products, handles for the terminal object, and can handle both and when it comes to the Cartesian closed structure.

  test-πη : (pair : Hom X (Y βŠ—β‚€ Z)) β†’ pair ≑ ⟨ π₁ ∘ pair , Ο€β‚‚ ∘ pair ⟩
  test-πη p = solve {Ο„ = `X} {`Y `Γ— `Z} `p (`π₁ `∘ `p `, `Ο€β‚‚ `∘ `p) refl
    where `p = ` p

  test-πβ₁ : π₁ ∘ ⟨ f , g ⟩ ≑ f
  test-πβ₁ = solve (`π₁ `∘ (`f `, `g)) `f refl

  test-πβ₂ : Ο€β‚‚ ∘ ⟨ f , g ⟩ ≑ g
  test-πβ₂ = solve (`Ο€β‚‚ `∘ (`f `, `g)) `g refl

  test-⟨⟩∘ : ⟨ f ∘ h , g ∘ h ⟩ ≑ ⟨ f , g ⟩ ∘ h
  test-⟨⟩∘ = solve (`f `∘ `h `, `g `∘ `h) ((`f `, `g) `∘ `h) refl

  test-Ζ›Ξ² : (f : Hom X [ Y , Z ]) β†’ f ≑ Ζ› (unlambda f)
  test-Ζ›Ξ² fn = solve `fn (`Ζ› (`unlambda `fn)) refl
    where `fn : Mor `X (`Y `β‡’ `Z) ; `fn = ` fn

  test-Ζ›h : (o : Hom (X βŠ—β‚€ Y) Z) β†’ o ≑ unlambda (Ζ› o)
  test-Ζ›h o = solve `o (`unlambda (`Ζ› `o)) refl
    where `o : Mor (`X `Γ— `Y) `Z ; `o = ` o

  test-!Ξ· : (f g : Hom X top) β†’ f ≑ g
  test-!Ξ· f g = solve {Ο„ = `X} {Οƒ = `⊀} (` f) (` g) refl