module Cat.CartesianClosed.Lambda

# Simply-typed lambda calculusπ

{o β} (C : Precategory o β) (fp : has-products C) (term : Terminal C) (cc : Cartesian-closed C fp term) where open Binary-products C fp hiding (uniqueβ) open Cartesian-closed cc open Cat.Reasoning C

The **simply typed
$Ξ»-calculus$**
(STLC) is a very small typed programming language very strongly
associated with Cartesian closed
categories. In this module, we define the syntax for STLC with base
types, and inhabitants of these, given by the objects and morphisms of
an arbitrary CCC. This syntax can be used to *reflect* morphisms
of a CCC, making the βstructuralβ morphisms explicit. We then build a
*normalisation* procedure, which can be used to effectively
compare morphisms in the CCC.

The types of STLC are generated by function types `a `β b`

and product types `a `Γ b`

, along with an inclusion of
objects from the target category to serve as βbase typesβ, e.g.Β the
natural numbers. The contexts are simply lists of types.

data Ty : Type o where _`Γ_ : Ty β Ty β Ty _`β_ : Ty β Ty β Ty `_ : Ob β Ty data Cx : Type o where β : Cx _,_ : Cx β Ty β Cx

To use contexts, we introduce *variables*. A variable
$v:ΞβΟ$
gives an index in
$Ξ$
where something of type
$Ο$
can be found. It can either be right here, in which case we `stop`

, or it can be
further back in the context, and we must `pop`

the top
variable off to get to it.

data Var : Cx β Ty β Type o where stop : Var (Ξ , Ο) Ο pop : Var Ξ Ο β Var (Ξ , Ο) Ο

We can now write down the type of expressions, or, really, of
*typing judgements*. An inhabitant of `Expr Ξ Ο`

is a
tree representing a complete derivation of something of type
`Ο`

. We insist on the name *expression* rather than
*term* since there are more expressions than there are terms: For
example, in the context
$β,a:Ο,$
the expressions
$(Ξ»bβb)a$
and
$a$
denote the same term.

data Expr Ξ where `var : Var Ξ Ο β Expr Ξ Ο `Οβ : Expr Ξ (Ο `Γ Ο) β Expr Ξ Ο `Οβ : Expr Ξ (Ο `Γ Ο) β Expr Ξ Ο `β¨_,_β© : Expr Ξ Ο β Expr Ξ Ο β Expr Ξ (Ο `Γ Ο) `Ξ» : Expr (Ξ , Ο) Ο β Expr Ξ (Ο `β Ο) `$ : Expr Ξ (Ο `β Ο) β Expr Ξ Ο β Expr Ξ Ο `_ : Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β Expr Ξ Ο

Using the Cartesian closed structure, we can interpret types,
contexts, variables and expressions in terms of the structural
morphisms: For example, the empty context is interpreted by the terminal
object, and^{1} the zeroth variable is given by the
second projection map
$ΞΓAβA.$

β¦ X `Γ Y β§α΅ = β¦ X β§α΅ ββ β¦ Y β§α΅ β¦ X `β Y β§α΅ = Exp.B^A β¦ X β§α΅ β¦ Y β§α΅ β¦ ` X β§α΅ = X β¦ Ξ , Ο β§αΆ = β¦ Ξ β§αΆ ββ β¦ Ο β§α΅ β¦ β β§αΆ = Terminal.top term β¦_β§βΏ : Var Ξ Ο β Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β¦ stop β§βΏ = Οβ β¦ pop x β§βΏ = β¦ x β§βΏ β Οβ β¦_β§α΅ : Expr Ξ Ο β Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β¦ `var x β§α΅ = β¦ x β§βΏ β¦ `Οβ p β§α΅ = Οβ β β¦ p β§α΅ β¦ `Οβ p β§α΅ = Οβ β β¦ p β§α΅ β¦ `β¨ a , b β© β§α΅ = β¨ β¦ a β§α΅ , β¦ b β§α΅ β© β¦ `Ξ» e β§α΅ = Ζ β¦ e β§α΅ β¦ `$ f x β§α΅ = ev β β¨ β¦ f β§α΅ , β¦ x β§α΅ β© β¦ ` x β§α΅ = x

The type of expressions could (and, to some extent, *should*)
be higher-inductive-recursive, with path constructors expressing the
$Ξ²/$$Ξ·$
rules β the universal properties that we want to capture. However, this
would significantly complicate the development of the rest of this
module. We choose to work with raw derivations, instead, for
convenience. Equality of `Expr`

being coarser than that of
`Hom`

does not significantly affect our application, which is
metaprogramming.

## Context inclusionsπ

We will implement our semantics using *normalisation by
evaluation*, by embedding our expressions into a domain where the
judgemental equalities of the object-level are also judgemental at the
meta-level. We choose presheaves on a category of *inclusions*,
where the objects are contexts and the maps
$ΞβΞ$
indicate that, starting from
$Ξ,$
you can get to
$Ξ$
by *dropping* some of the variables, and keeping everything else
in-order.

data Ren : Cx β Cx β Type (o β β) where stop : Ren Ξ Ξ drop : Ren Ξ Ξ β Ren (Ξ , Ο) Ξ keep : Ren Ξ Ξ β Ren (Ξ , Ο) (Ξ , Ο)

Here we must confess to another crime: Since our (types, hence our)
contexts include objects of the base category, they do not form a set:
therefore, neither does the type `Ren`

of context inclusions. This
means that we can not use `Ren`

as the morphisms in a
(pre)category. This could be remedied by instead working relative to a
given set of base types, which are equipped with a map into semantic
objects. This does not significantly alter the development, but it would
be an additional inconvenience.

Regardless, we can define composition of context inclusions by recursion, and, if necessary, we could prove that this is associative and unital. However, since we are not building an actual category of presheaves (only gesturing towards one), we omit these proofs.

_βΚ³_ : β {Ξ Ξ Ξ} β Ren Ξ Ξ β Ren Ξ Ξ β Ren Ξ Ξ stop βΚ³ Ο = Ο drop Ο βΚ³ Ο = drop (Ο βΚ³ Ο) keep Ο βΚ³ stop = keep Ο keep Ο βΚ³ drop Ο = drop (Ο βΚ³ Ο) keep Ο βΚ³ keep Ο = keep (Ο βΚ³ Ο)

If we fix a type $Ο,$ then the family $ββΟ$ which sends a context to the variables in that context is actually a presheaf. Put less pretentiously, renamings act on variables:

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)

Finally, we can define an interpretation of renamings into our model CCC. Note that this interpretation lands in monomorphisms.

β¦_β§Κ³ : Ren Ξ Ξ β Hom β¦ Ξ β§αΆ β¦ Ξ β§αΆ β¦ stop β§Κ³ = id β¦ drop r β§Κ³ = β¦ r β§Κ³ β Οβ β¦ keep r β§Κ³ = β¦ r β§Κ³ ββ id

## Normals and neutralsπ

To define evaluation, we need a type of normal forms: In our setting,
these include lambda abstractions and pairs, along with morphisms of the
base category. However, we are not working with evaluation, rather with
*normalisation*, where reduction takes place in arbitrary
contexts. Therefore, there are expressions that we can not *give a
value to*, but for which no further normalisation can happen: for
example, applying a variable. Therefore, we define mutually inductive
types of **normal forms** and **neutral
forms**.

data Nf : Cx β Ty β Type (o β β) data Ne : Cx β Ty β Type (o β β)

A **normal form** is indeed one for which no more
reduction is possible: lambda expressions and pairs. A neutral form is
also normal. These come primarily from non-empty contexts. Neutral forms
are, essentially, variables together with a stack of *pending
eliminations* (applications or projections that will be reduced in
the future). However, in our setting, we also consider the base terms as
neutral *at base types*.

data Nf where lam : Nf (Ξ , Ο) Ο β Nf Ξ (Ο `β Ο) pair : Nf Ξ Ο β Nf Ξ Ο β Nf Ξ (Ο `Γ Ο) ne : β {x} β Ne Ξ (` x) β Nf Ξ (` x) data Ne where var : Var Ξ Ο β Ne Ξ Ο app : Ne Ξ (Ο `β Ο) β Nf Ξ Ο β Ne Ξ Ο fstβ : Ne Ξ (Ο `Γ Ο) β Ne Ξ Ο sndβ : Ne Ξ (Ο `Γ Ο) β Ne Ξ Ο hom : β {o} β Hom β¦ Ξ β§αΆ o β Ne Ξ (` o)

By a fairly obvious recursion, renamings act on neutrals and normals, thus making these, too, into presheaves.

ren-ne : β {Ξ Ξ Ο} β Ren Ξ Ξ β Ne Ξ Ο β Ne Ξ Ο ren-nf : β {Ξ Ξ Ο} β Ren Ξ Ξ β Nf Ξ Ο β Nf Ξ Ο

This is the only case that requires attention: to rename a morphism
of the base category, we must reify the renaming into its denotation,
and compose with the morphism. The alternative here would be to keep a
stack of pending renamings at each `hom`

, which could
then be optimised before composing at the end.

ren-ne Ο (hom h) = hom (h β β¦ Ο β§Κ³)

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)

Normals and neutrals also have a straightforward denotation given by the Cartesian closed structure.

β¦_β§β : Nf Ξ Ο β Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β¦_β§β : Ne Ξ Ο β Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β¦ lam h β§β = Ζ β¦ h β§β β¦ pair a b β§β = β¨ β¦ a β§β , β¦ b β§β β© β¦ ne x β§β = β¦ x β§β β¦ var x β§β = β¦ x β§βΏ β¦ app f x β§β = ev β β¨ β¦ f β§β , β¦ x β§β β© β¦ fstβ h β§β = Οβ β β¦ h β§β β¦ sndβ h β§β = Οβ β β¦ h β§β β¦ hom h β§β = h

We also have to prove a few hateful lemmas about how renamings, and its action on variables, neutrals and normals, interact with the denotation brackets. These lemmas essentially say that $[[f[Ο]]]=[[f]][[Ο]],$ so that it doesnβt matter whether we first pass to the semantics in $C$ or apply a renaming.

β¦β§-βΚ³ : (Ο : 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 β§β β β¦ Ο β§Κ³

##
If you want, you can choose to read the proofs of these substitution
correctness lemmas by clicking on this `<details>`

tag.

β¦β§-βΚ³ stop Ο = intror refl β¦β§-βΚ³ (drop Ο) Ο = pushl (β¦β§-βΚ³ Ο Ο) β¦β§-βΚ³ (keep Ο) stop = introl refl β¦β§-βΚ³ (keep Ο) (drop Ο) = pushl (β¦β§-βΚ³ Ο Ο) β sym (pullr Οβββ¨β©) β¦β§-βΚ³ (keep Ο) (keep Ο) = sym $ Product.unique (fp _ _) (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) = refl 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

## Normalizationπ

We would like to write a map of type `Expr Ξ Ο β Nf Ξ Ο`

.
However, *by design*, this is not straightforward: the type of
normal forms isβ¦
$Ξ²-normal.$^{2} However, note that, since both
`Nf`

and `Ne`

are βpresheavesβ on the βcategory of
renamingsβ, we can use the Cartesian closed structure *of
presheaves* to interpret the lambda calculus. The idea here is that
presheaves, being functors into
$Sets,$
have a computational structure on the relevant connectives that closely
matches that of
$Sets$
itself: for example, composing the first projection with a pairing, in
the category of presheaves, is (componentwise) definitionally equal to
the first component of the pair. Itβs a boosted up version of exactly
the same idea used for the category
solver.

Then, as long as we can *reify* these presheaves back to
normal forms, we have a normalisation procedure! Expressions are
interpreted as sections of the relevant presheaves, then reified into
normal forms. And, to be clear, we only need to reflect the presheaves
that actually represent types: these can be built by recursion (on the
type!) so that they are very easy to reify.

However, that still leaves the question of *correctness* for
the NbE algorithm. Given an expression
$Ξβ’e:Ο,$
we will have two wildly different approaches to interpreting
$e$
as a morphism
$[[Ξ]]β[[Ο]].$
Thereβs the naΓ―ve denotation `β¦_β§α΅`

, which interprets
an expression directly using the relevant connections; But now we can
also interpret an expression
$Ξβ’e:Ο$
into a section
$v:R_{Ο}(Ξ),$
then reify that to a normal form
$n:Nf(Ξ,Ο),$
and take the denotation
$[[n]]:[[Ξ]]β[[Ο]].$
Normalisation *should* compute a
$Ξ²-normal$
form, and
$Ξ²$
is validated by CCCs, so
$[[n]]$
and
$[[e]]$
should be the same. How do we ensure this?

It would be totally possible to do this in two passes - first define
the algorithm, then prove it correct. But the proof of correctness would
mirror the structure of the algorithm almost 1:1! Can we define the
algorithm in a way that is *forced* into correctness? It turns
out that we can! The idea here is an adaptation of the
**gluing** method in the semantics of type theory. Rather
than have a mere presheaf
$R_{Ο}(β)$
to represent the semantic values in
$Ο,$
our full construction `Tyα΅`

has *three*
arguments: The type
$Ο,$
the context
$Ξ$
(over which it is functorial), and a *denotation*
$h:[[Ξ]]β[[Ο]]$
β and in prose, weβll write `Tyα΅`

as
$R_{h}(Ξ);$
we say that
$s$
**tracks**
$h$
when
$s:R_{h}(Ξ).$

Since all our operations on semantic values will be written against a
type *indexed by* their denotations, the core of the algorithm
will *have to* be written in a way that evidently preserves
denotations β the type checker is doing most of the work. Our only
actual correctness theorem boils down to showing that, given
$s:R_{h}(Ξ),$
we have
$[[reifys]]=h$
in
$Hom([[Ξ]],[[Ο]]).$

To summarize all the parts, we have:

**Expressions**$Ξβ’e:Ο$ β the user writes these, and they may have redices.**Denotations**$[[e]]:[[Ξ]]β[[Ο]].$ Since a CCC has βstructuralβ morphisms corresponding to each kind of expression, we can directly read off a morphism from an expression.**Neutrals**$n:Ne(Ξ,Ο)$ and**normals**$n:Nf(Ξ,Ο).$ A neutral is something that wants to reduce but canβt (e.g.Β a projection applied to a variable), and a normal is something that definitely wonβt reduce anymore (e.g.Β a lambda expression). Normals and neutrals also have denotations, so we may also write $[[n]]$ when $n:Nf(β,β)$ or $n:Ne(β,β).$**Semantic values**, $R_{h}(Ξ).$ The presheaf $R_{h}(Ξ)$ is computed by recursion on $Ο$ so that its sections have a good computational representation. As mentioned above, itβs indexed by a denotation $h:[[Ξ]]β[[Ο]],$ forcing the core of the algorithm to preserve denotations.The

**reification and reflection**transformations $reify:R_{β}(Ξ)βNf(Ξ,Ο),$ which turns a semantic value into a normal form, and $reflect:Ne(Ξ,Ο)βR_{β}(Ξ)$ which witnesses that the semantic values include the neutrals.

Our main objective is a normalisation function $expr$ that maps expressions $Ξβ’e:Ο$ to semantic values $expr(e):R_{[[e]]}(Ξ).$ Letβs get started.

While we have been talking about presheaves above, the actual code
does *not* actually set up a presheaf category to work in. The
reason for this is parsimony. Referring to presheaves for the
motivation, but working with simpler type families, lends itself better
to formalisation; many of the details, e.g.Β functoriality of
$R_{β}(β),$
are not used, and would simply be noise.

### Semantic valuesπ

Tyα΅ : (Ο : Ty) (Ξ : Cx) β Hom β¦ Ξ β§αΆ β¦ Ο β§α΅ β Type (o β β)

We define $R_{β}(β)$ by recursion on $Ο,$ and its definition is mostly unsurprising: at each case, we use the Cartesian closed structure of presheaf categories to interpret the given type into a presheaf that has the right universal property, but is βdefinitionally nicerβ. Letβs go through it case-by-case. When faced with a product type in the object language, we can simply return a meta-language product type. However, we must also preserve the tracking information: if a section of a product type is to track $h,$ what should each component track? Well, we know that $h=β¨Ο_{1}h,Ο_{2}hβ©,$ by the uniqueness property of Cartesian products. So the first component should track $Ο_{1}h,$ and the second $Ο_{2}h!$

Tyα΅ (Ο `Γ Ο) Ξ h = Tyα΅ Ο Ξ (Οβ β h) Γ Tyα΅ Ο Ξ (Οβ β h)

For a function type, we once again appeal to the construction in presheaves. The components of the exponential $(Q_{P})(Ξ)$ are defined to be the natural transformations $γ(Ξ)ΓPβQ,$ which, at the component, are given by maps $Hom(Ξ,Ξ)ΓP(Ξ)βQ(Ξ).$ A function value must preserve tracking information: A function which tracks $h,$ if given an argument tracking $a,$ it must return a value which tracks the application of $h$ to $a,$ relative to the renaming $Ο.$ In a CCC, thatβs given by

$evβ¨hβΟ,aβ©,$which is precisely what we require.

Tyα΅ (Ο `β Ο) Ξ h = β {Ξ} (Ο : Ren Ξ Ξ) {a} β Tyα΅ Ο Ξ a β Tyα΅ Ο Ξ (ev β β¨ h β β¦ Ο β§Κ³ , a β©)

Finally, we have the case of base types, for which the corresponding presheaf is that of neutral forms. Here, we can finally discharge the tracking information: a neutral $n$ tracks $h$ iff. $[[n]]=h.$

Tyα΅ (` x) Ξ h = Ξ£ (Ne Ξ (` x)) Ξ» n β β¦ n β§β β‘ h

To work on open contexts, we can define (now by induction), the
presheaf of *parallel substitutions*, which are decorated
sequences of terms. These also have a morphism of
$C$
attached, but keep in mind that a parallel substitution
$ΞβΞ$
interprets as an element of
$Hom(Ξ,Ξ),$
hence that is what they are indexed over.

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 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

As always, we must show that these have an action by renamings. Renamings act on the semantic component, too: if $v$ tracks $h,$ then $v[Ο]$ tracks $h[[Ο]].$

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-subα΅ r β = β ren-subα΅ r (c , x) = subα΅β¨ sym (assoc _ _ _) β©subα΅ (ren-subα΅ r c) , tyα΅β¨ sym (assoc _ _ _) β©tyα΅ (ren-tyα΅ r x)

### Reification and reflectionπ

We can now define the reification and reflection functions. Reflection embeds a neutral form into semantic values; Reification turns semantic values into normal forms. Since we have defined the semantic values by recursion, we can exploit the good computational behaviour of Agda types in our reification/reflection functions: for example, when reifying at a product type, we know that we have an honest-to-god product of semantic values at hand.

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) 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

The interesting cases deal with function types: To reify a lambda β
which is semantically represented by a *function* that operates
on (a renaming and) the actual argument β we produce a `lam`

constructor,
but we must then somehow reify βall possible bodiesβ.

However, since the semantic value of a function takes arguments and
returns results in an arbitrary extension of the given context, we can
introduce a new variable β thus a new neutral β and apply the body
*to that*. Evaluation keeps going, but anything that actually
depends on the body will be blocked on this new neutral!

Conversely, reflection starts from a neutral, and must build a semantic value that captures all the pending applications. At the case of a lambda, we have a neutral $n:Ξβ’AβB,$ a renaming $Ο:ΞβΞ,$ and an argument $a:Ξβ’A.$ We can thus build the stuck application $n[Ο]a:Ξβ’B.$

This is also where we encounter the only correctness lemma that is
not forced on us by the types involved, since the type of normal forms
$Nf(Ξ,Ο)$
is not indexed by a denotation in
$C.$
We must write an external function `reifyα΅-correct`

, actually
establishing that
$[[reifyv]]=h$
when
$v$
tracks
$h.$

reifyα΅-correct {Ο = Ο `Γ Ο} (a , b) = sym $ Product.unique (fp _ _) (sym (reifyα΅-correct a)) (sym (reifyα΅-correct b)) reifyα΅-correct {Ο = Ο `β Ο} {h = h} Ξ½ = let p : β¦ reifyα΅ (Ξ½ (drop stop) (reflectα΅ (var stop))) β§β β‘ ev β β¨ h β id β Οβ , Οβ β© p = reifyα΅-correct (Ξ½ (drop stop) (reflectα΅ (var stop))) in ap Ζ p β sym (unique _ (apβ _β_ refl (apβ β¨_,_β© (sym (pulll (elimr refl))) (eliml refl)))) reifyα΅-correct {Ο = ` x} d = d .snd

β¦_β§Λ’ : β {Ξ Ξ h} β Subα΅ Ξ Ξ h β Hom β¦ Ξ β§αΆ β¦ Ξ β§αΆ β¦_β§Λ’ β = Terminal.! term β¦_β§Λ’ (c , x) = β¨ β¦ c β§Λ’ , β¦ reifyα΅ x β§β β© β¦β§Λ’-correct : β {Ξ Ξ h} (Ο : Subα΅ Ξ Ξ h) β β¦ Ο β§Λ’ β‘ h β¦β§Λ’-correct β = Terminal.!-unique term _ β¦β§Λ’-correct (Ο , x) = sym (Product.unique (fp _ _) (sym (β¦β§Λ’-correct Ο)) (sym (reifyα΅-correct x)))

### Interpreting expressionsπ

With our semantic values carefully chosen to allow reflection and
reification, we can set out to build an `Expr`

-algebra. To work in open
contexts, an expression
$Ξβ’e:Ο$
will be interpreted as a natural transformation from parallel
substitutions to types: the parallel substitution acts as our
βenvironmentβ, so is used in the interpretation of variables:

varα΅ : β {Ο} (Ο : Var Ξ Ο) β Subα΅ Ξ Ξ Ο β Tyα΅ Ο Ξ (β¦ Ο β§βΏ β Ο) varα΅ stop (_ , x) = x varα΅ (pop v) (c , _) = tyα΅β¨ assoc _ _ _ β©tyα΅ (varα΅ v c)

We must interpret morphisms from the model category in a
type-directed way, and eta-expand as we go. Thatβs because we made the
decision to only have morphisms as neutrals *at base type*.
Therefore, if a morphism from the base category lands in (e.g.)
products, we must interpret it as the semantic product of its
projections:

baseα΅ : β {h'} (h : Hom β¦ Ξ β§αΆ β¦ Ο β§α΅) β Subα΅ Ξ Ξ h' β Tyα΅ Ο Ξ (h β h') baseα΅ {Ο = Ο `Γ Οβ} x c = tyα΅β¨ sym (assoc _ _ _) β©tyα΅ (baseα΅ (Οβ β x) c) , tyα΅β¨ sym (assoc _ _ _) β©tyα΅ (baseα΅ (Οβ β x) c) baseα΅ {Ο = Ο `β Ο} {h' = h'} h c Ο {Ξ±} a = tyα΅β¨ pullr (Product.unique (fp _ _) (pulll Οβββ¨β© β extendr Οβββ¨β©) (pulll Οβββ¨β© β Οβββ¨β©)) β©tyα΅ (baseα΅ (ev β β¨ h β Οβ , Οβ β©) ( subα΅β¨ sym Οβββ¨β© β©subα΅ (ren-subα΅ Ο c), tyα΅β¨ sym Οβββ¨β© β©tyα΅ a)) baseα΅ {Ο = ` t} x c = hom (x β β¦ c β§Λ’) , ap (x β_) (β¦β§Λ’-correct c)

Those are the hard bits, we can now interpret everything else by a
simple recursion! Note that, when interpreting a lambda expression, we
return a function which evaluates the body, and when eliminating it, we
apply it to the value of its argument^{3}.

exprα΅ : β {h} (e : Expr Ξ Ο) (Ο : Subα΅ Ξ Ξ h) β Tyα΅ Ο Ξ (β¦ e β§α΅ β h) exprα΅ (`var x) c = varα΅ x c exprα΅ (`Οβ p) c = tyα΅β¨ assoc _ _ _ β©tyα΅ (exprα΅ p c .fst) exprα΅ (`Οβ p) c = tyα΅β¨ assoc _ _ _ β©tyα΅ (exprα΅ p c .snd) exprα΅ `β¨ a , b β© c = tyα΅β¨ sym (pulll Οβββ¨β©) β©tyα΅ (exprα΅ a c) , tyα΅β¨ sym (pulll Οβββ¨β©) β©tyα΅ (exprα΅ b c) exprα΅ {h = h} (`$ f a) c = tyα΅β¨ ap (ev β_) (apβ β¨_,_β© (idr _) refl β sym (β¨β©β h)) β assoc _ _ _ β©tyα΅ (exprα΅ f c stop (exprα΅ a c)) exprα΅ (` x) c = baseα΅ x c exprα΅ {h = h} (`Ξ» f) Ο Ο {m} a = tyα΅β¨ fixup β©tyα΅ (exprα΅ f ( subα΅β¨ sym Οβββ¨β© β©subα΅ (ren-subα΅ Ο Ο) , tyα΅β¨ sym Οβββ¨β© β©tyα΅ a ))

where abstract fixup : β¦ f β§α΅ β β¨ h β β¦ Ο β§Κ³ , m β© β‘ ev β β¨ (β¦ `Ξ» f β§α΅ β h) β β¦ Ο β§Κ³ , m β© fixup = sym $ ev β β¨ (β¦ `Ξ» f β§α΅ β h) β β¦ Ο β§Κ³ , m β© β‘Λβ¨ apβ _β_ refl (Product.unique (fp _ _) (pulll Οβββ¨β© β extendr Οβββ¨β©) (pulll Οβββ¨β© Β·Β· pullr Οβββ¨β© Β·Β· eliml refl)) β©β‘Λ ev β β¦ `Ξ» f β§α΅ ββ id β β¨ h β β¦ Ο β§Κ³ , m β© β‘β¨ pulll (is-exponential.commutes has-is-exp _) β©β‘ β¦ f β§α΅ β β¨ h β β¦ Ο β§Κ³ , m β© β

If we apply the semantic value of an expression to the βidentity parallel substitutionβ, a context where all the variables are given a neutral value, we get a normal form!

id-subα΅ : β Ξ β Subα΅ Ξ Ξ id id-subα΅ β = β id-subα΅ (Ξ , x) = subα΅β¨ idl _ Β·Β· idl _ Β·Β· sym (idr _) β©subα΅ (ren-subα΅ (drop stop) (id-subα΅ Ξ)) , tyα΅β¨ sym (idr _) β©tyα΅ (reflectα΅ (var stop)) nf : Expr Ξ Ο β Nf Ξ Ο nf x = reifyα΅ (exprα΅ x (id-subα΅ _))

Moreover, we can appeal to our key correctness theorem to conclude the correctness of the entire normalisation procedure. Thatβs the only explicit theorem we proved, with the rest of the pieces being threaded through the definitions of the various transformations.

opaque nf-sound : (e : Expr Ξ Ο) β β¦ nf e β§β β‘ β¦ e β§α΅ nf-sound {Ξ = Ξ} e = reifyα΅-correct (exprα΅ e (id-subα΅ Ξ)) β elimr refl

As a demonstration, we can normalise the expression

$a:A,b:Bβ’e=Ο_{1}β¨((Ξ»cβc)a),bβ©:A$which lets Agda reduce it away to be simply the variable $a$ (which is the second in the context). Moreover, by appeal to the correctness theorem, we can prove that the complicated morphism that $e$ denotes is equal to the much simpler $Ο_{2}Ο_{1}.$

module _ {a b : Ob} where private e1 : Expr ((β , ` a) , ` b) _ e1 = `Οβ `β¨ `$ (`Ξ» (`var stop)) (`var (pop stop)) , `var stop β© _ : nf e1 β‘ ne (var (pop stop)) _ = refl _ : Οβ β Οβ β‘ Οβ β β¨ ev β β¨ Ζ Οβ , Οβ β Οβ β© , Οβ β© _ = nf-sound e1 -- An attempt to normalise this proof produced 4 MiB of garbage, and -- ran for over an hour before our patience ran out.

solve : (e e' : Expr Ξ Ο) β nf e β‘ nf e' β β¦ e β§α΅ β‘ β¦ e' β§α΅ solve e e' prf = sym (nf-sound e) Β·Β· ap β¦_β§β prf Β·Β· nf-sound e'

## An applicationπ

The normalisation algorithm serves to decide the semantic equality of
expressions in the simply-typed lambda calculus, but Iβll freely admit
thatβs not a task that comes up every day. We can also use this
algorithm to prove things about the simply-typed lambda calculus! As an
example, we have **canonicity**: every term in a base type
denotes an actual element of the base type. In our categorical setting,
that means that, given
$Ξβ’e:A,$
where
$A$
is one of the non-pair, non-function types we have included from the
category
$C,$
then there is a global element
$h:Hom(β€,A)$
which
$e$
denotes.

canonicity : β {a} β (e : Expr β (` a)) β Ξ£ (Hom (Terminal.top term) a) Ξ» h β β¦ e β§α΅ β‘ h canonicity {a = a} e = go (nf e) (nf-sound e) where no-functions : β {a b} β Ne β (a `β b) β β₯ no-pairs : β {a b} β Ne β (a `Γ b) β β₯ no-functions (app f _) = no-functions f no-functions (fstβ x) = no-pairs x no-functions (sndβ x) = no-pairs x no-pairs (app f _) = no-functions f no-pairs (fstβ x) = no-pairs x no-pairs (sndβ x) = no-pairs x go : (nf : Nf β (` a)) β β¦ nf β§β β‘ β¦ e β§α΅ β Ξ£ (Hom (Terminal.top term) a) Ξ» h β β¦ e β§α΅ β‘ h go (ne (app f _)) p = absurd (no-functions f) go (ne (fstβ x)) p = absurd (no-pairs x) go (ne (sndβ x)) p = absurd (no-pairs x) go (ne (hom x)) p = x , sym p