\section*{\Large Introduction}

Normalisation by evaluation for typed lambda calculus was first considered by
Berger and Schwichtenberg~\cite{BS} from a type and proof theoretic viewpoint,
and later investigated from the point of view of logic~\cite{Berger}, type
theory~\cite{CCoquand}, category theory~\cite{AHS,CDS,Reynolds}, and partial
evaluation~\cite{Danvy,Filinski99}.  This work gives a new categorical and
algebraic perspective on the topic.  

\paragraph{Outline.}
Normalisation by evaluation will be broadly viewed as the technique of giving
semantics in (metalanguages for) non-standard models from which normalisation
information can be extracted~({\it cf.}~\cite{MartinLof}). 
In this light, we will investigate the following problems.
\begin{enumerate}
\item[I.]\Rem{Extensional normalisation problem}: To define normal terms and
  establish that every term \mbox{$\beta\eta$-equals} one in normal form.

  That is, writing $\TermPSh\tau(\Gamma)$ for the set of terms of type~$\tau$
  in context $\Gamma$, to identify a set of normal terms 
  $\NFPSh\tau(\Gamma) \subseteq \TermPSh\tau(\Gamma)$ and show that for every 
  term $t\in\TermPSh\tau(\Gamma)$ there exists a normal term 
  $N\in\NFPSh\tau(\Gamma)$ such that $t =_{\beta\eta} N$.

\item[II.]\Rem{Intensional normalisation problem}: To define, and prove the
  correctness of, a normalisation function associating normal forms to terms.

  More precisely, to construct functions
  $$
  \simplenf{\tau,\Gamma}:
     \TermPSh\tau(\Gamma) \rightarrow \NFPSh\tau(\Gamma)
  $$
  satisfying the following three properties.
  \begin{enumerate}
  \item[(1)]For all normal terms $N\in\NFPSh\tau(\Gamma)$, the syntactic
    equality $\simplenf{\tau,\Gamma}(N)$ $= N$ holds. 

  \item[(2)]For all terms $t\in\TermPSh\tau(\Gamma)$, the semantic equality
    $\simplenf{\tau,\Gamma}(t) =_{\beta\eta} t$ holds. 

  \item[(3)]For all pair of 
    terms $t,t'\in\TermPSh\tau(\Gamma)$, if $t=_{\beta\eta} t'$ then 
    $\simplenf{\tau,\Gamma}(t) = \simplenf{\tau,\Gamma}(t')$.
  \end{enumerate}
  
  In the context of normalisation by evaluation, the correctness
  condition~(1) has seldom been considered ---the exception
  being~\cite{Reynolds}.  However, it is both natural and interesting.  
  For instance, together with the correctness condition~(3) it implies that
  $\beta\eta$-equal normal terms are syntactically equal, which in turn,
  together with the correctness condition~(2), entails the stronger version
  of extensional normalisation that every term \mbox{$\beta\eta$-equals} a
  unique normal term.  
\end{enumerate}

These problems will be respectively dealt with in Parts~I and~II of the paper.  
Part~I provides a unifying view of definability and normalisation leading to
an extensional normalisation result.  This analysis, besides unifying the two
hitherto unrelated problems of definability and normalisation, motivates and
elucidates the notions of neutral and normal terms, which are here distilled
from semantic considerations.  
Part~II shows that an intensional view of Part~I amounts to the traditional
technique of normalisation by evaluation.  This development leads to a
treatment of normalisation by evaluation via the Artin-Wraith glueing
construction, finally formalising the observation that normalisation by
evaluation is \Rem{closely related} to categorical
glueing~\cite{CoquandDybjer}. 

More in detail, the paper is organised as follows.
Section~I.1 briefly recalls the syntax and categorical semantics of the
typed lambda calculus.  
Section~I.2 presents an analysis of the lambda definability result of Jung
and Tiuryn via Kripke logical relations~\cite{JungTiuryn} leading to an
extensional normalisation result.
Section~II.1 describes the rudiments of a theory of typed abstract syntax
with variable binding which is used to put the typed lambda calculus in an
algebraic framework.
This algebraic view is exploited in Section~II.2 to structure the development
of an intensional version of Section~I.2 culminating in the technique of
normalisation by evaluation.

\paragraph{Related work.}
The treatment of extensional normalisation presented here is similar to Tait's
approach to strong normalisation via computability
predicates~\cite{Tait,Girard} for the typed lambda calculus, and also to
Krivine's approach to normalisation~\cite[Chapter~III]{Krivine} for the
untyped lambda calculus.  The precise relationships need to be investigated.  

The analysis of normalisation by evaluation pursued here is categorical and,
as such, is related to~\cite{AHS,CDS,Reynolds,ADHS}.   

The approach of \u{C}ubri\'c, Dybjer, and Scott~\cite{CDS} is in the context
of so-called $\mathcal{P}$-category theory; which is, roughly, a version of
category theory equipped with an intensional notion of equality formalised by
partial equivalence relations.  The intensional information needed for the
purpose of normalisation will be captured here in the context of traditional
category theory via Artin-Wraith glueing.

In Altenkirch, Hofmann, and Streicher~\cite{AHS}, normalisation by evaluation
is reconstructed categorically in a model obtained via an ad~hoc 
\Rem{twisted-glueing} construction.  This model embodies objects with both
syntactic and semantic components, and translations between them essentially
encoding a correctness predicate.  In contrast, we adopt a purely semantic
view, working with intensional logical relations in models given by the
traditional categorical-glueing construction~\cite{Wraith}.

Another important point of departure between this work and the other
categorical ones is the algebraic treatment of the subject, which led to a
deeper understanding of the normalisation function.  

\section*{\Large Part~I}

\subsection*{I.1\quad Typed lambda calculus}

For the purpose of establishing notation, we briefly recall the syntax and
semantics of the typed lambda calculus.  For details
see,~{\it e.g.},~\cite{LambekScott,Crole,Taylor}.

\paragraph{Syntax.} 
The types of the simply typed lambda calculus are given by the grammar
\begin{equation}\label{SimpleTypes}
\begin{array}{rcl}
\tau 
& ::= & \theta \mid \unittype \mid \tau_1 \producttype \tau_2
        \mid \tau_1 \arrowtype \tau_2
\end{array}
\end{equation}
where $\theta$ ranges over base types.  We write
$\TypeClosure\mathrm{T}$ for the set of simple types generated by a set of
base types $\mathrm{T}$.  

The grammar for the terms is 
$$\begin{array}{rcl}
t 
& ::= & x \mid \pair{ } \mid \pi_1(t) \mid \pi_2(t) \mid
        \pair{t_1,t_2} \mid t(t') \mid \lambdaop{x:\tau}t
\end{array}$$ 
where $x$ ranges over (a countably infinite set of) variables.  The notion of
free and bound variables are standard.  As usual, we will identify terms up
to the renaming of bound variables.  

Typing contexts, with types in a set $\mathcal{T}$, are defined as functions $V
\rightarrow \mathcal{T}$ where the domain of the context, $V$, is a finite subset
of the set of variables.  Under this view, for a variable~$x$, a type~$\tau$,
and a context~$\Gamma$, we let \mbox{$(x:\tau) \in \Gamma$} stand for
\mbox{$x\in\mathrm{dom}(\Gamma)$} and $\Gamma(x) = \tau$.  For distinct variables
\mbox{$x_i$~($i=1,n$),} we use the notation $\pair{x_i:\tau_i}_{i=1,n}$ for
the context  \mbox{$\setof{ x_1,\ldots, x_n } \rightarrow \mathcal{T}$} mapping
$x_i$ to~$\tau_i$.  For a context~$\Gamma$, a variable $x$, and a type $\tau$,
the notation $\Gamma, x:\tau$ presupposes $x \not\in \mathrm{dom}(\Gamma)$ and denotes
the context $\mathrm{dom}(\Gamma)\cup\setof{x} \rightarrow \mathcal{T}$ mapping every
$y \in \mathrm{dom}(\Gamma)$ to $\Gamma(y)$, and $x$ to $\tau$.

The well-typed terms $\Gamma \vdash t: \tau$ in context (where $\Gamma$ is
a typing context, $t$ is a term, and $\tau$ is a type) are given by the usual
rules; see Figure~\ref{Terms}.
\begin{figure
\hrulefill
$$\begin{array}{c}
\begin{array}{c}
\\ \hline
\Gamma \vdash x:\tau
\end{array}
\quad(x:\tau) \in \Gamma
\\[1mm]%
\begin{array}{c}
\\ \hline
\Gamma \vdash \pair{ }: \unittype
\end{array}
\\[5mm]%
\begin{array}{c}
\Gamma \vdash t: \tau_1\producttype\tau_2
\\ \hline
\Gamma \vdash \pi_i(t): \tau_i
\end{array}
\quad(i=1,2)
\\[6mm]%
\begin{array}{c}
\Gamma \vdash t_i: \tau_i \quad(i=1,2)
\\ \hline
\Gamma \vdash \pair{t_1,t_2}: \tau_1\producttype\tau_2
\end{array}
\\[6mm]%
\begin{array}{c}
\Gamma \vdash t: \tau'\arrowtype\tau
\quad
\Gamma \vdash t': \tau'
\\ \hline
\Gamma \vdash t(t'): \tau
\end{array}
\\[6mm]%
\begin{array}{c}
\Gamma, x:\tau' \vdash t: \tau
\\ \hline
\Gamma \vdash \lambdaop{x:\tau'}t: \tau'\arrowtype\tau
\end{array}
\end{array}$$
\caption{Well-typed terms}\label{Terms}
\hrulefill
\end{figure}

\paragraph{Semantics.} 
The appropriate mathematical universes for giving semantics to the typed
lambda calculus are cartesian closed
categories~\cite{LambekScott,Crole,Taylor};~{\it i.e.},~categories with terminal
object, binary products, and exponentials (for which we respectively use
the notation~$1$,~$\times$, and~$\myArrow{\shortarrowlength}{}{}$).  

For an interpretation $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$
of base types in a cartesian closed category, we let 
$\mbox{\boldmath$s$}\sembracket{\xy(0,-1)\ar@{-}(2,-1)\endxy}: 
   \TypeClosure\mathrm{T} \rightarrow \cat S$ 
be the extension to simple types as prescribed by a chosen cartesian closed
structure.  That is,
$\mbox{\boldmath$s$}\sembracket\theta = \mbox{\boldmath$s$}(\theta)$ (for 
$\theta \in \mathrm{T}$), 
$\mbox{\boldmath$s$}\sembracket\unittype = 1$, and
$\mbox{\boldmath$s$}\sembracket{\tau\producttype\tau'} 
   = \mbox{\boldmath$s$}\sembracket\tau \times \mbox{\boldmath$s$}\sembracket{\tau'}$
and
$\mbox{\boldmath$s$}\sembracket{\tau\arrowtype\tau'} 
   = \mbox{\boldmath$s$}\sembracket\tau \myArrow{\shortarrowlength}{}{} \mbox{\boldmath$s$}\sembracket{\tau'}$
(for $\tau, \tau' \in \TypeClosure\mathrm{T}$).  
As usual, the interpretation of types is extended to contexts by
setting  
$\mbox{\boldmath$s$}\sembracket\Gamma
   = \prod_{x\in\mathrm{dom}(\Gamma)} \mbox{\boldmath$s$}\sembracket{\Gamma(x)}$ 
for all contexts~$\Gamma$.  
Finally, the semantics of a term $\Gamma \vdash t: \tau$ as a morphism  
$\mbox{\boldmath$s$}\sembracket\Gamma \rightarrow \mbox{\boldmath$s$}\sembracket\tau$ in
$\cat S$ is denoted $\mbox{\boldmath$s$}\sembracket{\Gamma \vdash t: \tau}$. 

\section*{I.2\quad From definability to normalisation}

Kripke relations were introduced by Jung and Tiuryn in~\cite{JungTiuryn} for
the purpose of characterising lambda definability.  We will analyse this
result and provide a corresponding extensional normalisation result. 

\paragraph{Kripke relations.} 
For a functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$, a 
\Def{$\scat C$-Kripke relation} $R$ of arity $\mbox{\boldmath$\varsigma$}$ over an object $A$ of
$\cat S$ is a family 
$\setof{ R(c) \subseteq \cat S(\mbox{\boldmath$\varsigma$}(c),A) }_{c \in \scriptobj{\,\scat C\,}}$
satisfying the following condition.
\begin{description}
\item[](Monotonicity)
  For every $\rho: c' \rightarrow c$ in $\scat C$ and every 
  \mbox{$a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A$} in $R(c)$, the map 
  $a \circ \mbox{\boldmath$\varsigma$}(\rho): \mbox{\boldmath$\varsigma$}(c') \rightarrow A$ is in $R(c')$. 
\end{description}
In other words, a $\scat C$-Kripke relation $R$ of arity~$\mbox{\boldmath$\varsigma$}$ over an object
$A$ is a unary predicate ${R\rightembedding\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),A)}$ over
the $\scat C^\mathrm{op}$-variable set of $A$-valued morphisms
$\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),A): \scat C^\mathrm{op} \rightarrow \mathbf{Set}$ in the functor
category $\mathbf{Set}^{\scat C^\mathrm{op}}$ of $\scat C^\mathrm{op}$-variable sets, referred to as
presheaves.

The category of Kripke relations $\K{\mbox{\boldmath$\varsigma$}}$ of arity 
$\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ has objects given by pairs $(R,A)$
consisting of an object $A$ of $\cat S$ and a 
$\scat C$-Kripke relation of arity $\mbox{\boldmath$\varsigma$}$ over $A$, and morphisms 
\mbox{$f: (R,A) \rightarrow (R',A')$} given by maps $f: A \rightarrow A'$ in
$\cat S$ such that, for all \mbox{$a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A$} in $R(c)$,
the composite \mbox{$f \circ a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A'$} is in $R'(c)$.
Composition and identities are as in $\cat S$.

\begin{example}
The category of $\scat C$-Kripke relations of arity the unique functor to the
terminal category is (isomorphic to) the complete Heyting algebra of
subterminal objects of the presheaf topos $\mathbf{Set}^{\scat C^\mathrm{op}}$.  
\end{example}

The following proposition is
well-known~(see,~{\it e.g.},~\cite{Alimohamed,MaReynolds}).   
\begin{proposition} \label{KripkeCCC}
Let $\scat C$ be a small category and let $\cat S$ be a cartesian closed
category.  For a functor \mbox{$\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$}, the
category of Kripke relations $\K{\mbox{\boldmath$\varsigma$}}$ is cartesian closed and the
forgetful functor \mbox{$\K{\mbox{\boldmath$\varsigma$}} \rightarrow \cat S: (R,A) \mapsto A$}
preserves the cartesian closed structure strictly.
\end{proposition}
The cartesian closed structure of $\K{\mbox{\boldmath$\varsigma$}}$ is given as follows. 
\begin{description}
\item[](Products)
  The terminal object is $(\top,1)$ where $1$
  is terminal in $\cat S$ and where 
  $\top(c) = \setof{ \mbox{\boldmath$\varsigma$}(c) \rightarrow 1}$ for all
  $c$ in $\scat C$.  

  The product $(R,A)\times(R',A')$ of $(R,A)$ and $(R',A')$ is 
  $$
  (R,A) 
    \stackleftarrow\pi 
  (R \wedge R' , A \times A')
    \stackrightarrow{\pi'} 
  (R',A')
  $$ 
  where 
  $A \stackleftarrow\pi A \times A' \stackrightarrow{\pi'} A'$
  is the product of $A$ and $A'$ in $\cat S$, and where 
  $a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A \times A'$ is in 
  $(R \wedge R')(c)$ iff $\pi \circ a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A$ is
  in $R(c)$ and $\pi' \circ a: \mbox{\boldmath$\varsigma$}(c) \rightarrow A'$ is in $R'(c)$.

\item[](Exponentials)
  The exponential $(R,A)\myArrow{\shortarrowlength}{}{}(R',A')$
  of $(R,A)$ and $(R',A')$ is 
  $$
  (R \supset R' , A \myArrow{\shortarrowlength}{}{} A') \times (R,A)
  \stackrightarrow\varepsilon
  (R',A')
  $$ 
  where $(A \myArrow{\shortarrowlength}{}{} A') \times A \stackrightarrow\varepsilon A'$ is the
  exponential of $A$ and $A'$ in $\cat S$, and where 
  ${f: \mbox{\boldmath$\varsigma$}(c) \rightarrow A \myArrow{\shortarrowlength}{}{} A'}$ is in $(R \supset R')(c)$
  iff for every $\rho: c' \rightarrow c$ in $\scat C$ and 
  $a: \mbox{\boldmath$\varsigma$}(c') \rightarrow A$ in $R(c')$, the composite 
  $\varepsilon \circ \pair{f \circ \mbox{\boldmath$\varsigma$}(\rho) , a}: \mbox{\boldmath$\varsigma$}(c') \rightarrow A'$ is
  in $R'(c')$.
\end{description}

The Fundamental Lemma of logical relations is a consequence of
Proposition~\ref{KripkeCCC}. 

\begin{lemma}\Rem{(Fundamental Lemma~\cite{Plotkin,Statman})}
For an interpretation of base types
$\mathcal{I}: \mathrm{T} \rightarrow \K{\mbox{\boldmath$\varsigma$}}:
       \theta \mapsto (\mathscr{R}_\theta,\mathcal{I}_0(\theta))$,
the interpretation 
\begin{center}
$\mathcal{I}_0\sembracket{\Gamma \vdash t: \tau}:
   \mathcal{I}_0\sembracket{\Gamma} \rightarrow \mathcal{I}_0\sembracket{\tau}$
in $\cat S$
\end{center}
of a term $\Gamma \vdash t: \tau$ yields a morphism 
\mbox{$\mathcal{I}\sembracket{\Gamma} \rightarrow \mathcal{I}\sembracket{\tau}$} in
$\K{\mbox{\boldmath$\varsigma$}}$; that is, for 
$\mathcal{I}\sembracket\Gamma = (\mathscr{R}_\Gamma,\mathcal{I}_0\sembracket\Gamma)$ 
and $\mathcal{I}\sembracket\tau = (\mathscr{R}_\tau,\mathcal{I}_0\sembracket\tau)$,  
the following diagram
$$\xymatrix@C=5pt{
\raisebox{1.5mm}{$\mathscr{R}_\Gamma$}
\ar[rrrrrr]
\ar@{^(->}[d] &&&&&& 
\raisebox{1mm}{$\mathscr{R}_\tau$} \ar@{^(->}[d]  
\\
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),\mathcal{I}_0\sembracket\Gamma) 
\ar[rrrrrr]_-{\mathcal{I}_0\sembracket{\Gamma \vdash t: \tau}\circ\xy(0,-1)\ar@{-}(2,-1)\endxy}
&&&&&&
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),\mathcal{I}_0\sembracket\tau) 
}$$
commutes in $\mathbf{Set}^{\scat C^\mathrm{op}}\!\!$ (for a necessarily unique natural map 
\mbox{$\mathscr{R}_\Gamma \rightarrow \mathscr{R}_\tau$}).
\end{lemma}

\paragraph{Definability.}
The definability result of Jung and Tiuryn~\cite{JungTiuryn} uses Kripke
relations varying over a poset of contexts ordered by context extension.
Here, however, to parallel the development with the one to follow in Part~II,
we will consider Kripke relations varying over a category of contexts and
context renamings. 

\begin{definition} \label{ContextCat}
For a set of types $\mathcal{T}$, we let $\F{}\!\downarrow\!\mathcal{T}$ be the category
with objects given by contexts $\Gamma$ with types in~$\mathcal{T}$, and
with morphisms $\Gamma \rightarrow \Gamma'$ given by type-preserving
context renamings; that is, by functions 
$\rho: \mathrm{dom}(\Gamma) \rightarrow \mathrm{dom}(\Gamma')$ such that for all
variables $x \in \mathrm{dom}(\Gamma)$, the types $\Gamma(x)$ and 
$\Gamma'(\rho x)$ are equal.  We write $\F{}[\mathcal{T}]$ for 
$(\F{}\!\downarrow\!\mathcal{T})^\mathrm{op}$.
\end{definition}

With respect to an interpretation 
\mbox{$\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$} 
of base types in a cartesian closed category, we write
$\mbox{\boldmath$s$}\sembracket{\xy(0,-1)\ar@{-}(2,-1)\endxy}$ for 
the canonical semantic functor 
$\F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S$ interpreting
contexts and their renamings.  This is explicitly given by 
\[
\mbox{\boldmath$s$}\sembracket\rho 
\ = \
\pair{ \mbox{\boldmath$s$}\sembracket{\Gamma' \vdash \rho x: \tau}}_{(x:\tau)\in\Gamma}
\ = \
\pair{\pi_{\rho x} }_{x\in\mathrm{dom}(\Gamma)}
\ : \ \mbox{\boldmath$s$}\sembracket{\Gamma'} \rightarrow \mbox{\boldmath$s$}\sembracket\Gamma
\]
for all $\rho: \Gamma \rightarrow \Gamma'$ in 
$\F{}\!\downarrow\!\TypeClosure\mathrm{T}$. 

For every type $\tau \in \TypeClosure\mathrm{T}$, the
\Def{definability relation} 
$$
\mathscr{D}_\tau(\Gamma) 
= 
\setof{ \
  \mbox{\boldmath$s$}\sembracket{\Gamma \vdash t: \tau }
    \mid \Gamma \vdash t: \tau
  \ }
\subseteq
  \cat S(\mbox{\boldmath$s$}\sembracket\Gamma,\mbox{\boldmath$s$}\sembracket\tau)
$$
is an $\F{}[\TypeClosure\mathrm{T}]$-Kripke relation of arity 
\mbox{$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy: 
   \F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S$}
over $\mbox{\boldmath$s$}\sembracket\tau$, and the family of definability relations 
$\setof{ \mathscr{D}_\tau }_{\tau \in \TypeClosure\mathrm{T}}$ has the
following logical characterisation.
\begin{lemma}\Rem{(Definability Lemma~\cite{JungTiuryn,Alimohamed})} 
\label{Definability_Lemma}
Let $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$ be an interpretation of base
types in a cartesian closed category.
Setting $\mathscr{R}_\theta = \mathscr{D}_\theta$ for all base types
$\theta \in \mathrm{T}$ and letting $\mathscr{R}_\tau$ be given by the
cartesian closed structure of the category of Kripke relations
$\K{\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy: 
      \F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S}$
for the other types~$\tau \in \TypeClosure\mathrm{T}$, it follows that
$\mathscr{R}_\tau = \mathscr{D}_\tau$ for all types 
$\tau \in \TypeClosure\mathrm{T}$.
\end{lemma}
The usual proof of the Definability Lemma
is by induction on the structure of types using the explicit description of
the cartesian closed structure in categories of Kripke relations given above;
see~\cite{JungTiuryn,Alimohamed} (and~\cite{FioreSimpson} for the case with
sum types).  However, there is a more conceptual argument based on
establishing that the definability relations satisfy the following closure
properties:
$$\begin{array}{rcl}
\mathscr{D}_{\unittype}
& = & 
\top
\\[2mm]
\mathscr{D}_{\mbox{\scriptsize$\tau \producttype \tau'$}} 
& = & 
\mathscr{D}_\tau \wedge \mathscr{D}_{\tau'} 
\\[2mm]
\mathscr{D}_{\tau \arrowtype \tau'} 
& = & 
\mathscr{D}_\tau \supset \mathscr{D}_{\tau'} 
\end{array}$$
which is, in effect, what the usual calculations really amount to.

The above analysis can be refined further.  Indeed, the fact
that neither of the following inclusions 
\begin{equation} \label{D_subseteq_R_subseteq_D}
\mathscr{D}_\tau \subseteq \mathscr{R}_\tau \subseteq \mathscr{D}_\tau
\end{equation}
in isolation is strong enough to re-establish the inductive hypothesis in the
Definability Lemma, suggests considering a more general situation in which the
Kripke logical relations $\mathscr{R}_\tau$ are bounded by possibly distinct
Kripke relations (unlike the situation in~(\ref{D_subseteq_R_subseteq_D})).  

We are thus led to the following Basic Lemma.  Notice the mixed-variance
treatment of exponentiation.  This is akin to Krivine's approach to
normalisation for the untyped lambda calculus using \Rem{adapted pairs} of
subsets of lambda terms~\cite[Chapter~III, pages~33--39]{Krivine}.
\begin{lemma}\Rem{(Basic Lemma)} \label{Basic_Lemma}
Consider an interpretation 
\mbox{$\mathcal{I}_0: \mathrm{T} \rightarrow \cat S$}
of base types in a cartesian closed category $\cat S$. 

With respect to a functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$, let 
$\pair{ (\mathscr{A}_\tau,\mathcal{I}_0\sembracket\tau) }
   _{\tau\in\TypeClosure\mathrm{T}}$ 
and 
$\pair{ ( \mathscr{B}_\tau,\mathcal{I}_0\sembracket\tau ) }
   _{\tau\in\TypeClosure\mathrm{T}}$ 
be two families of Kripke relations in $\K{\mbox{\boldmath$\varsigma$}}$ indexed by types
such that 
$$\begin{array}{c}
\mathscr{B}_\unittype \, = \, \top 
\\[2mm]
\mathscr{A}_{\mbox{\scriptsize$\sigma\producttype\tau$}}
\, \subseteq \, 
(\mathscr{A}_{\sigma} \wedge \mathscr{A}_{\tau})
\qquad\qquad 
(\mathscr{B}_{\sigma} \wedge \mathscr{B}_{\tau})
\, \subseteq \, 
\mathscr{B}_{\mbox{\scriptsize$\sigma\producttype\tau$}}
\\[2mm]
\mathscr{A}_{\sigma\arrowtype\tau}
\, \subseteq \, 
(\mathscr{B}_{\sigma} \supset \mathscr{A}_{\tau})
\qquad\qquad 
(\mathscr{A}_{\sigma} \supset \mathscr{B}_{\tau})
\, \subseteq \,
\mathscr{B}_{\sigma\arrowtype\tau}
\end{array}$$
For a family of Kripke relations
$\pair{ ( \mathscr{R}_\theta , \mathcal{I}_0\sembracket\theta ) }
   _{\theta\in\mathrm{T}}$ 
in $\K{\mbox{\boldmath$\varsigma$}}$ indexed by base types, let 
$\pair{ ( \mathscr{R}_\tau , \mathcal{I}_0\sembracket\tau ) }_
   {\tau\in\TypeClosure\mathrm{T}}$ 
be the family of Kripke relations indexed by types induced by the
cartesian closed structure of $\K{\mbox{\boldmath$\varsigma$}}$.

If
$\mathscr{A}_\theta
   \subseteq \mathscr{R}_\theta
     \subseteq \mathscr{B}_\theta$
for all base~types~$\theta \in \mathrm{T}$, then
\begin{enumerate}
\item \label{Basic_Lemma_One}
$\mathscr{A}_\tau
   \subseteq \mathscr{R}_\tau
   \subseteq \mathscr{B}_{\tau}$ 
for all types~$\tau \in \TypeClosure\mathrm{T}$, and thus

\item \label{Basic_Lemma_Two}
for all terms 
$\Gamma\vdash t:\tau$~$($with~$\Gamma=\pair{x_i:\tau_i}_{i=1,n})$
and morphisms $a_i: \mbox{\boldmath$\varsigma$}(c) \rightarrow \mathcal{I}_0\sembracket{\tau_i}$ in 
$\mathscr{A}_{\tau_i}(c)$~$(1 \leq i \leq n, c \in \obj{\scat C})$,
we have that
$\mathcal{I}_0\sembracket{\Gamma \vdash t: \tau} \circ \pair{a_1,\ldots,a_n}:
   \mbox{\boldmath$\varsigma$}(c) \rightarrow \mathcal{I}_0\sembracket{\tau}$
is in $\mathscr{B}_\tau(c)$.
\end{enumerate}
\end{lemma}
\begin{proof}
The proof of the first part is by induction on the structure of types.  
This uses the facts that
\begin{center}
$R\subseteq\top$ for all $(R,1)$ in $\K{\mbox{\boldmath$\varsigma$}}$ 
\end{center}
and that, for Kripke relations $(R_i,A_i)$ and $(R'_i,A_i)$ in
$\K{\mbox{\boldmath$\varsigma$}}$ ($i=1,2$), 
\begin{center}
if $R_1 \subseteq R'_1$ and $R_2 \subseteq R'_2$ then 
$(R_1\wedge R_2) \subseteq (R'_1\wedge R'_2)$ and 
$(R'_1\supset R_2) \subseteq (R_1\supset R'_2)$
\end{center}
which follows from the functoriality of binary products and exponentials using
the observation that, for $(R,A)$ and $(R',A)$ in
$\K{\mbox{\boldmath$\varsigma$}}$, 
\[ 
R \subseteq R'
\mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow}
\mathrm{id}_A: (R,A) \rightarrow (R',A)
\mbox{ in $\K{\mbox{\boldmath$\varsigma$}}$}
\quad.
\] 

The proof of the second part follows from considering
the interpretation $\mathcal{I}: \mathrm{T} \rightarrow \K{\mbox{\boldmath$\varsigma$}}$ mapping a base
type $\theta$ to the Kripke relation
$( \mathscr{R}_\theta , \mathcal{I}_0\sembracket\theta )$ and noticing that, 
by the first part and the Fundamental Lemma of logical relations, the diagram
below in $\mathbf{Set}^{\scat C^\mathrm{op}}$
\begin{equation} \label{Basic_Lemma_Diagram}
\begin{array}{c}\xymatrix@C=0pt{
\mathscr{A}_\Gamma 
\ar@{^(->}[r]
\ar@{^(->}[dr] & \mathscr{R}_\Gamma \ar@{^(->}[d] 
\ar@{->}[rrrrrrrrrr]
&&&&&&&&&& \mathscr{R}_\tau \ar@{^(->}[d] 
\ar@{^(->}[r]
& \mathscr{B}_\tau \ar@{^(->}[dl] 
\\
& 
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),\mathcal{I}_0\sembracket\Gamma)
\ar[rrrrrrrrrr]_-{\mathcal{I}_0\sembracket{\Gamma \vdash t: \tau} \circ \xy(0,-1)\ar@{-}(2,-1)\endxy}
&&&&&&&&&& 
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),\mathcal{I}_0\sembracket\tau)
}\end{array}
\end{equation}
commutes, where for $\Gamma = \pair{ x_i:\tau_i }_{i=1,n}$, 
$\mathscr{A}_\Gamma 
 = 
 \mathscr{A}_{\tau_1}\wedge\ldots\wedge\mathscr{A}_{\tau_n}$
and 
$\mathscr{R}_\Gamma 
 = 
 \mathscr{R}_{\tau_1}\wedge\ldots\wedge\mathscr{R}_{\tau_n}$.
\end{proof}

The Basic Lemma yields the Definability Lemma by considering 
$\mathscr{A}_\tau = \mathscr{D}_\tau = \mathscr{B}_\tau$ in 
the category of Kripke relations
$\K{\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy: 
   \F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S}$ 
for the given interpretation 
$\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$.  We will now see that the Basic
Lemma can be also applied to obtain an extensional normalisation result (see
Lemma~\ref{Extensional_Normalisation_Lemma}).     

\paragraph{Normalisation.}
For an interpretation \mbox{$\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$}
of base types in a cartesian closed category we aim at defining families  
$\setof{ ( \mathscr{DM}_\tau , \mbox{\boldmath$s$}\sembracket\tau ) 
   }_{\tau\in\TypeClosure\mathrm{T}}$
and 
$\setof{ ( \mathscr{DN}_\tau , \mbox{\boldmath$s$}\sembracket\tau ) 
         }_{\tau\in\TypeClosure\mathrm{T}}$
of $\F{}[\TypeClosure\mathrm{T}]$-Kripke relations of arity
$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy: 
   \F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S$
of definable morphisms such that
$$\begin{array}{c}
(i)\enspace
   \mathscr{DN}_\unittype \, = \, \top 
\\[2mm]
(ii)\enspace 
    \mathscr{DM}_{\mbox{\scriptsize$\sigma\producttype\tau$}}
    \,\subseteq\,
    (\mathscr{DM}_{\sigma} \wedge \mathscr{DM}_{\tau})
\qquad\qquad 
(iii)\enspace
     (\mathscr{DN}_{\sigma} \wedge \mathscr{DN}_{\tau})
     \,\subseteq\,
     \mathscr{DN}_{\mbox{\scriptsize$\sigma\producttype\tau$}}
\\[2mm]
(iv)\enspace
    \mathscr{DM}_{\sigma\arrowtype\tau}
    \,\subseteq\,
    ( \mathscr{DN}_{\sigma} \supset \mathscr{DM}_{\tau} )
\qquad\qquad 
(v)\enspace
   ( \mathscr{DM}_{\sigma} \supset \mathscr{DN}_{\tau} ) 
   \,\subseteq\,
   \mathscr{DN}_{\sigma\arrowtype\tau}
\\[2mm]
(vi)\enspace
    \mathscr{DM}_{\theta} \subseteq \mathscr{DN}_{\theta} 
    \quad (\theta \in \mathrm{T})
\\[2mm]
(vii)\enspace
     \pi_x: 
     \mbox{\boldmath$s$}\sembracket\Gamma \rightarrow \mbox{\boldmath$s$}\sembracket{\tau}
     \in \mathscr{DM}_{\tau}(\Gamma)
\quad ((x:\tau)\in\Gamma)
\end{array}$$
so that, by the second part of the Basic Lemma, we get (setting
$\mathscr{R}_\theta = \mathscr{DM}_\theta$ for all
$\theta \in \mathrm{T}$, and 
$a_i = \pi_i: 
 \mbox{\boldmath$s$}\sembracket\Gamma \rightarrow \mbox{\boldmath$s$}\sembracket{\tau_i}$ 
for $\Gamma = \pair{x_i:\tau_i}_{i=1,n}$) that, for all terms 
$\Gamma \vdash t: \tau$, 
\begin{equation} \label{Extensional_Normalisation}
\mbox{
$\mbox{\boldmath$s$}\sembracket{\Gamma \vdash t: \tau}: 
  \mbox{\boldmath$s$}\sembracket\Gamma \rightarrow \mbox{\boldmath$s$}\sembracket\tau$
is in $\mathscr{DN}_\tau(\Gamma)$\quad.
}
\end{equation}

The above will be achieved by distilling the semantic closure
properties~$(i)$--$(vii)$ into two syntactic typing systems $\vdash_\mathscr{M}$ and
$\vdash_\mathscr{N}$ with respect to which the definitions 
\begin{equation} \label{SemNeutralTerms}
\mathscr{DM}_\tau(\Gamma) 
\ = \
\setof{ \ 
        \mbox{\boldmath$s$}\sembracket{\Gamma \vdash M:\tau} 
        \mid
        \Gamma \vdash_\mathscr{M} M: \tau
        \ }
\end{equation}
\begin{equation} \label{SemNormalTerms}
\mathscr{DN}_\tau(\Gamma) 
\ = \
\setof{ \
        \mbox{\boldmath$s$}\sembracket{\Gamma \vdash N:\tau} 
        \mid
        \Gamma \vdash_\mathscr{N} N: \tau
        \ }
\end{equation}
will provide the required Kripke relations (see
Proposition~\ref{NEandNF_KripkeRelations}).  The conditions $(i)$--$(vii)$
amount, roughly, to the following properties. 
\begin{itemize}
\item
  The system~$\vdash_\mathscr{M}$ should contain variables
  (condition $(vii)$), and be closed under
  projections~(condition~$(ii)$) and under the application to terms in
  the system~$\vdash_\mathscr{N}$ (condition~$(iv)$).

\item
  The system~$\vdash_\mathscr{N}$ should contain the unit~(condition~$(i)$),
  and should be closed under pairing~(condition~$(iii)$) and under
  abstraction~(condition~$(v)$).

\item
  Every term of base type in the system~$\vdash_\mathscr{M}$ should be in the
  system~$\vdash_\mathscr{N}$~(condition~$(vi)$).
\end{itemize}
Formally, the systems are given by the rules in Figure~\ref{NN_Terms}.

\medskip
Thus, from purely semantic considerations, we have synthesised the notions of
neutral normal forms~({\it viz.}, those derivable in the system~$\vdash_\mathscr{M}$) and of
long $\beta\eta$-normal forms~({\it viz.},~those derivable in the
system~$\vdash_\mathscr{N}$), henceforth respectively referred to as \Rem{neutral} and
\Rem{normal} terms, and characterised as follows.
\begin{figure
\hrulefill
$$\begin{array}{c}
\begin{array}{c}
\\ \hline 
\Gamma \vdash_\mathscr{M} x: \tau
\end{array}
\quad(x:\tau) \in \Gamma
\\[6mm]%
\begin{array}{c}
\Gamma \vdash_\mathscr{M} M: \tau_1 \producttype \tau_2
\\ \hline
\Gamma \vdash_\mathscr{M} \pi_i(M): \tau_i
\end{array}
\quad(i=1,2)
\\[6mm]%
\begin{array}{c}
\Gamma \vdash_\mathscr{M} M: \tau \arrowtype \tau'
\quad
\Gamma \vdash_\mathscr{N} N: \tau
\\ \hline
\Gamma \vdash_\mathscr{M} M(N): \tau'
\end{array}
\\[4mm]%
\begin{array}{c}
\\ \hline
\Gamma \vdash_\mathscr{N} \pair{ }: \unittype
\end{array}
\\[6mm]%
\begin{array}{c}
\Gamma \vdash_\mathscr{N} N_i: \tau_i \quad (i=1,2)
\\ \hline
\Gamma \vdash_\mathscr{N} \pair{N_1,N_2}: \tau_1 \producttype \tau_2
\end{array}
\\[6mm]%
\begin{array}{c}
\Gamma, x: \tau \vdash_\mathscr{N} N: \tau'
\\ \hline
\Gamma \vdash_\mathscr{N} \lambdaop{x:\tau}N: \tau \arrowtype \tau'
\end{array}
\\[6mm]%
\begin{array}{c}
\Gamma \vdash_\mathscr{M} M: \theta
\\ \hline
\Gamma \vdash_\mathscr{N} M: \theta
\end{array}
\quad\mbox{($\theta$ a base type)}
\end{array}$$
\caption{Neutral and normal terms}\label{NN_Terms}
\hrulefill
\end{figure}

\begin{proposition}\label{Neutral_and_Normal_Characterisation}
\mbox{}
\begin{enumerate}
\item (Neutral terms)
\[
\Gamma \vdash_\mathscr{M} t: \tau
\mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow}
\begin{array}[t]{l}
[ \ \exists\ (x:\tau)\in\Gamma.\ t = x \ ]
\\[2mm]
\enspace \vee \
[ \ \exists\ \Gamma\vdash_\mathscr{M} M:\tau\producttype\tau'.\  t = \pi_1(M) \ ]
\enspace \vee \
[ \ \exists\ \Gamma\vdash_\mathscr{M} M:\tau'\producttype\tau.\  t = \pi_2(M) \ ]
\\[2mm]
\enspace \vee \
[ \ \exists\ \Gamma\vdash_\mathscr{M} M:\tau'\arrowtype\tau\, , 
            \Gamma\vdash_\mathscr{N} N:\tau' . \  
  t = M(N) \ ]
\end{array}
\]

\item (Normal terms) \label{Normal_Characterisation}
\begin{itemize}
\item  
  $\Gamma\vdash_\mathscr{N} t:\unittype \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} t = \pair{ }$

\item  
  $\Gamma\vdash_\mathscr{N} t:\tau_1\producttype\tau_2 
   \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} 
   [ \ \exists\ \Gamma\vdash_\mathscr{N} N_1:\tau_1\, , \Gamma \vdash_\mathscr{N} N_2:\tau_2 .\
     t = \pair{N_1,N_2}
     \ ]$

\item  
  $\Gamma\vdash_\mathscr{N} t:\tau\arrowtype\tau' 
   \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} 
   [ \ \exists\ \Gamma,x:\tau\vdash_\mathscr{N} N:\tau'.\ t = \lambdaop{x:\tau}N \ ]$

\item  For $\theta$ a base type, 
  $\Gamma\vdash_\mathscr{N} t:\theta \mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} \Gamma\vdash_\mathscr{M} t:\theta$.
\end{itemize}
\end{enumerate}
\end{proposition}

Neutral and normal terms are closed under context renamings and thereby
semantically induce Kripke relations.

\begin{proposition}\label{NEandNF_KripkeRelations}
Let $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$ be an interpretation of base
types in a cartesian closed category.
For all types $\tau\in\TypeClosure\mathrm{T}$, the
definitions~(\ref{SemNeutralTerms}) and~(\ref{SemNormalTerms}) respectively
yield  $\F{}[\TypeClosure\mathrm{T}]$-Kripke relations $\mathscr{DM}_\tau$ and
$\mathscr{DN}_\tau$ of arity 
$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy: 
   \F{}[\TypeClosure\mathrm{T}] \rightarrow \cat S$
satisfying conditions~$(i)$--$(vii)$.
\end{proposition}
\begin{proof}
The first part is a corollary of the facts that 
\begin{equation} \label{Neutral_Renaming_Invariance}
\Gamma\vdash_\mathscr{M} M:\tau 
\mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} 
\forall\ \rho:\Gamma\to\Gamma' \mbox{ in } \F{}\!\downarrow\!\TypeClosure\mathrm{T} .\
\Gamma'\vdash_\mathscr{M} M[\subst{\rho x}x]_{x\in\mathrm{dom}(\Gamma)} : \tau 
\end{equation}
and 
\begin{equation} \label{Normal_Renaming_Invariance}
\Gamma\vdash_\mathscr{N} N:\tau 
\mathrel{\Leftarrow\!\!\!\!\!\!\Rightarrow} 
\forall\ \rho:\Gamma\to\Gamma' \mbox{ in } \F{}\!\downarrow\!\TypeClosure\mathrm{T} .\
\Gamma'\vdash_\mathscr{N} N[\subst{\rho x}x]_{x\in\mathrm{dom}(\Gamma)} : \tau 
\quad.
\end{equation}

The second part follows by the construction of the systems $\vdash_\mathscr{M}$ and
$\vdash_\mathscr{N}$.  
\end{proof}

From Proposition~\ref{NEandNF_KripkeRelations}, we
have~(\ref{Extensional_Normalisation}) and therefore, 
from~(\ref{SemNormalTerms}) and
Proposition~\ref{Neutral_and_Normal_Characterisation}%
(\ref{Normal_Characterisation}), 
we obtain the following Extensional Normalisation Lemma.  
\begin{lemma}~\Rem{(Extensional Normalisation Lemma)} 
\label{Extensional_Normalisation_Lemma} 
Let $\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$ be an interpretation of base
types in a cartesian closed category.  For every term 
$\Gamma \vdash t: \tau$ there exists a long $\beta\eta$-normal term 
$\Gamma \vdash_\mathscr{N} N: \tau$ such that  
\[
\mbox{\boldmath$s$}\sembracket{\Gamma \vdash t: \tau}
\ = \
\mbox{\boldmath$s$}\sembracket{\Gamma \vdash N: \tau}
\ : \
\mbox{\boldmath$s$}\sembracket\Gamma \rightarrow \mbox{\boldmath$s$}\sembracket\tau
\]
in $\cat S$.
\end{lemma}

Specialising the Extensional Normalisation Lemma for the canonical
interpretation of types in the free cartesian closed category generated
by them we obtain the following syntactic result~({\it cf.}~\cite{StreicherNBE}).
\begin{corollary} \label{Corollary_BetaEtaLongNormalForms}
Every simply typed term is $\beta\eta$-equal to one in long $\beta\eta$-normal
form.
\end{corollary}

The above does not give information about the long~$\beta\eta$-normal form
associated to a term because Kripke relations are extensional predicates.
What is needed instead for this purpose is a notion of \Rem{intensional}
Kripke relation in which the extension of the predicate is witnessed (or
realised).  Technically, this amounts to revisiting the development in
categories obtained by the Artin-Wraith glueing construction~\cite{Wraith}.
This will be done in Part~II.  To do it at an appropriate abstract,
syntax-independent level we will first consider the  
typed lambda calculus algebraically.

\section*{\Large Part~II}

\section*{II.1\quad Algebraic typed lambda calculus}

We provide an algebraic setting for the syntax and semantics of the typed
lambda calculus following and extending the theory of~\cite{FiorePlotkinTuri}.
In particular, we describe the typed abstract syntax of simply typed and of
neutral and normal terms as initial algebras, and show how the usual semantics
corresponds to unique algebra homomorphisms from the initial (term) algebras
to suitable semantic algebras.   

\subsection*{II.1.1\quad Syntax}

Categories of contexts, which we study next, play a crucial role in
describing abstract syntax with variable binding; see~\cite{FiorePlotkinTuri}
for further details.

\paragraph{Free (co)cartesian categories.}
The category of untyped contexts and renamings $\F{}$ with objects given by
finite subsets of (the countably infinite set of) variables and morphisms
given by all functions is the free cocartesian category on one generator.  

More generally, the free cocartesian category over a set $\mathcal{T}$ can be
described as the comma category $\F{}\!\downarrow\!\mathcal{T}$ of contexts with types
in the set $\mathcal{T}$ and type-preserving context renamings.  
(That is, $\F{}\!\downarrow\!\mathcal{T}$ is the category with objects given by maps 
$\Gamma: V \rightarrow \mathcal{T}$ where $V$ is in $\F{}$, and with morphisms 
$\rho: \Gamma \rightarrow \Gamma'$ given by functions 
\mbox{$\rho: \mathrm{dom}(\Gamma) \rightarrow \mathrm{dom}(\Gamma')$} such that 
$\Gamma = \Gamma' \circ \rho$.) 
The initial object $(0 \rightarrow \mathcal{T})$ in
$\F{}\!\downarrow\!\mathcal{T}$ is the empty context; whilst the coproduct in
$\F{}\!\downarrow\!\mathcal{T}$ is
$$\begin{array}{rcl}
(V \stackrightarrow\Gamma \mathcal{T})
+
(V' \stackrightarrow{\Gamma'} \mathcal{T})
& = &
(V + V' \longstackrightarrow{[\Gamma,\Gamma']} \mathcal{T})
\end{array}$$

As before, we write $\F{}[\mathcal{T}]$ for $(\F{}\!\downarrow\!\mathcal{T})^\mathrm{op}$.
Further, we write $\ctxtemb\xy(0,-1)\ar@{-}(2,-1)\endxy: \mathcal{T} \rightarrow \F{}[\mathcal{T}]$ for
the universal embedding (mapping $\tau$ to 
$(1 \stackrightarrow\tau \mathcal{T})$) and exhibiting $\F{}[\mathcal{T}]$ as the
free cartesian category over $\mathcal{T}$. 

\paragraph{Typed abstract syntax with variable binding.}
The semantic universe on which to consider the algebras for the typed
lambda calculus over a set of base types $\mathrm{T}$ is the functor 
category $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ of
\mbox{$\F{}\!\downarrow\!\TypeClosure\mathrm{T}$-variable sets}, referred to as 
(covariant)~presheaves.  (Recall that
$\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ has objects given by
functors \mbox{$\F{}\!\downarrow\!\TypeClosure\mathrm{T} \rightarrow \mathbf{Set}$} and
morphisms $\varphi: P \rightarrow P'$ 
given by natural transformations; that is,~families of functions
\mbox{$\varphi 
 = 
 \setof{ \varphi_\Gamma: P(\Gamma) \rightarrow P'(\Gamma)
         }_{\Gamma\in\scriptobj{\,\F{}\!\downarrow\!\TypeClosure\mathrm{T}\,}}$}
such that 
$\varphi_{\Gamma'} \circ P(\rho) = P'(\rho) \circ \varphi_\Gamma$ for
all $\rho:\Gamma\rightarrow\Gamma'$ in~$\F{}\!\downarrow\!\TypeClosure\mathrm{T}$.)

The structure of $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ allowing the
interpretation of variables and binding operators is described below.
\begin{itemize}
\item
The presheaf of variables of type $\tau \in \TypeClosure\mathrm{T}$ is 
\begin{equation} \label{VPSh}
\VarPSh\tau = \mathbf{y}\ctxtemb\tau
\end{equation}
in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ where
$$\begin{array}{rcl}
\F{}[\TypeClosure\mathrm{T}] & \xymatrix{\ar@{^(->}[r]^\mathbf{y}&} &
\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}} \\[2mm]
\Gamma & \xymatrix{\ar@{|->}[r]&} &
(\F{}\!\downarrow\!\TypeClosure\mathrm{T})(\Gamma,\xy(0,-1)\ar@{-}(2,-1)\endxy)
\end{array}$$
is the Yoneda embedding.

Hence, 
$\VarPSh\tau(\Gamma) \cong \setof{ x \mid (x:\tau) \in \Gamma }$.

\item
For every type $\tau \in \TypeClosure\mathrm{T}$, the parameterisation
functor 
$\xy(0,-1)\ar@{-}(2,-1)\endxy\times\ctxtemb\tau: 
   \F{}[\TypeClosure\mathrm{T}] \rightarrow \F{}[\TypeClosure\mathrm{T}]$
induces the following situation
\begin{equation} \label{Adjoint_Situation_For_F[T]}
\begin{array}{c}\xymatrix@C=5pt{\ar@{}[rrrrrd]|(.5){\stackrel{\mathrm{Lan}}{\cong}}
\F{}[\TypeClosure\mathrm{T}]\ \ar@{^(->}[rrrrrr]^-\mathbf{y}
\ar[d]_-{\xy(0,-1)\ar@{-}(2,-1)\endxy\times\ctxtemb\tau} &&&&&& 
\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}
\ar[d]<-1ex>_-{\xy(0,-1)\ar@{-}(2,-1)\endxy\times\mathbf{y}\ctxtemb\tau} \ar@{}[d]|-{\dashv}
\\
\F{}[\TypeClosure\mathrm{T}]\ \ar@{^(->}[rrrrrr]_-\mathbf{y} &&&&&& 
\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}
\ar[u]<-1ex>_-{\mathbf{Set}^{(\xy(0,-1)\ar@{-}(2,-1)\endxy+\ctxtemb\tau)}}
}\end{array}
\end{equation}
Thus, in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$, the exponential
$P^{\VarPSh\tau}$ of the presheaf $\VarPSh\tau$ and a presheaf $P$ can be
explicitly described as \mbox{$P(\xy(0,-1)\ar@{-}(2,-1)\endxy+\ctxtemb\tau)$}. 

Hence, $P^{\VarPSh\tau}(\Gamma) \cong P(\Gamma+\ctxtemb\tau)$.
\end{itemize}

A \Def{typed lambda algebra} over a set of base types
$\mathrm{T}$ is a $\TypeClosure\mathrm{T}$-sorted algebra with
carrier given by a family 
$\setof{ {\mathscr{X}}_\tau }_{\tau\in\TypeClosure\mathrm{T}}$ of
presheaves in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ equipped
with the following operations:
\begin{center}\begin{tabular}{lcl}
(Variables) && 
  $\VarPSh\tau \rightarrow {\mathscr{X}}_\tau$
\\[2mm]
(Unit) &&
  $1 \rightarrow {\mathscr{X}}_\unittype$
\\[2mm]
(First Projection) &&
  ${\mathscr{X}}_{\tau\producttype\tau'} \rightarrow {\mathscr{X}}_\tau$
\\[2mm]
(Second Projection) &&
  ${\mathscr{X}}_{\tau'\producttype\tau} \rightarrow {\mathscr{X}}_\tau$
\\[2mm]
(Pairing) &&
  ${\mathscr{X}}_\tau \times {\mathscr{X}}_{\tau'} 
     \rightarrow
   {\mathscr{X}}_{\tau\producttype\tau'}$
\\[2mm]
(Application) && 
  ${\mathscr{X}}_{\tau'\arrowtype\tau} \times {\mathscr{X}}_{\tau'} 
     \rightarrow 
   {\mathscr{X}}_\tau$
\\[2mm]
(Abstraction) &&
  $({\mathscr{X}}_{\tau'})^{\VarPSh\tau} 
     \rightarrow
   {\mathscr{X}}_{\tau\arrowtype\tau'}$
\end{tabular}\end{center}
Informally, one thinks of the sets 
${\mathscr{X}}_\tau(\Gamma)$~($\tau\in\TypeClosure\mathrm{T}$,
$\Gamma \in \obj{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$) as the
$\tau$-sorted elements of the algebra~${\mathscr{X}}$ in the context $\Gamma$.
Note that under this interpretation the abstraction operation corresponds to
a natural family of mappings  
$$
{\mathscr{X}}_{\tau'}(\Gamma+\ctxtemb\tau) 
\rightarrow
{\mathscr{X}}_{\tau\arrowtype\tau'}(\Gamma)
$$
associating an element of sort $\tau'$ in the 
context \mbox{$\Gamma+\ctxtemb\tau$}~(that is,~the
context~$\Gamma$ extended with a fresh variable of type $\tau$) with an
element of sort $\tau\arrowtype\tau'$ in the context $\Gamma$.

In the tradition of categorical algebra, the category of typed lambda algebras
can be defined as the category of \mbox{$\Sigma$-algebras} for a signature
endofunctor~$\Sigma$ on
$(\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}})^{\TypeClosure\mathrm{T}}$.
This endofunctor is induced by the above operations as follows, 
for $\theta\in\mathrm{T}$ and $\tau,\tau'\in\TypeClosure\mathrm{T}$:  
$$\begin{array}{lcll}
(\Sigma{\mathscr{X}})_\theta
& = & \VarPSh\theta + \EEE\theta({\mathscr{X}})
\\[2mm]
(\Sigma{\mathscr{X}})_\unittype
& = & \VarPSh\unittype + 1 + 
      \EEE\unittype({\mathscr{X}})
\\[2mm]
(\Sigma{\mathscr{X}})_{\tau\producttype\tau'}
& = & \VarPSh{\tau\producttype\tau'} + 
      ({\mathscr{X}}_\tau \times {\mathscr{X}}_{\tau'}) +
      \EEE{\tau\producttype\tau'}({\mathscr{X}})
\\[2mm]
(\Sigma{\mathscr{X}})_{\tau\arrowtype\tau'}
& = & \VarPSh{\tau\arrowtype\tau'} + 
      ({\mathscr{X}}_{\tau'})^{\VarPSh\tau} +
      \EEE{\tau\arrowtype\tau'}({\mathscr{X}})
\end{array}$$
where 
$$\begin{array}{cl}
\EEE\tau({\mathscr{X}}) 
\; = \; \coprod_{\tau'\in\TypeClosure\mathrm{T}}\:
        {\mathscr{X}}_{\tau\producttype\tau'} 
        +
        {\mathscr{X}}_{\tau'\producttype\tau} 
        +
        ({\mathscr{X}}_{\tau'\arrowtype\tau}\times{\mathscr{X}}_{\tau'})
\end{array}$$
is the signature endofunctor corresponding to the projections and application
operations onto $\tau$.

The initial $\Sigma$-algebra 
$\TermPSh{} = \setof{ \TermPSh\tau }_{\tau\in\TypeClosure\mathrm{T}}$
with its structure
\begin{equation}\label{LamInitialAlg}
\begin{array}{rcl}
\VarPSh\theta + \EEE\theta(\TermPSh{})
&
\stackrightarrow\cong
&
\TermPSh\theta
\\[2mm]
\VarPSh\unittype + 1 + 
\EEE\unittype(\TermPSh{})
& \stackrightarrow\cong &
\TermPSh\unittype
\\[2mm]
\VarPSh{\tau\producttype\tau'} + 
(\TermPSh\tau \times \TermPSh{\tau'}) +
      \EEE{\tau\producttype\tau'}(\TermPSh{})
& \stackrightarrow\cong &
\TermPSh{\tau\producttype\tau'}
\\[2mm]
\VarPSh{\tau\arrowtype\tau'} + 
(\TermPSh{\tau'})^{\VarPSh\tau} +
\EEE{\tau\arrowtype\tau'}(\TermPSh{})
& \stackrightarrow\cong &
\TermPSh{\tau\arrowtype\tau'}
\end{array}
\end{equation}
can be explicitly described as the family of presheaves of terms 
$$
\TermPSh\tau(\Gamma) 
  = \setof{ \ t \mid \Gamma \vdash t: \tau \ }
$$
with presheaf action given by variable renaming~(that is,~by the
mapping associating $\Gamma \vdash t: \tau$ to 
\mbox{$\Gamma' \vdash t[\subst{\rho x}x]_{x\in\mathrm{dom}(\Gamma)}: \tau$}
for any $\rho: \Gamma \rightarrow \Gamma'$ in
$\F{}\!\downarrow\!\TypeClosure\mathrm{T}$), and with operations 
$$\begin{array}{lcl}
\mathsf{var}_\tau 
  & : & \VarPSh\tau \rightarrow \TermPSh\tau
\\[2mm]
\mathsf{unit}_\unittype 
  & : & 1 \rightarrow \TermPSh\unittype
\\[2mm]
\mathsf{fst}^{(\tau')}_\tau 
  & : & \TermPSh{\tau\producttype\tau'} \rightarrow \TermPSh{\tau}
\\[2mm]
\mathsf{snd}^{(\tau')}_\tau 
  & : & \TermPSh{\tau'\producttype\tau} \rightarrow \TermPSh{\tau}
\\[2mm]
\mathsf{pair}_{\tau\producttype\tau'} 
  & : & \TermPSh\tau \times \TermPSh{\tau'} 
        \rightarrow
        \TermPSh{\tau\producttype\tau'}
\\[2mm]
\mathsf{app}^{(\tau')}_\tau 
  & : & \TermPSh{\tau'\arrowtype\tau} \times \TermPSh{\tau'}
        \rightarrow
        \TermPSh\tau
\\[2mm]
\mathsf{abs}_{\tau\arrowtype\tau'} 
  & : & (\TermPSh{\tau'})^{\VarPSh\tau} 
        \rightarrow
        \TermPSh{\tau\arrowtype\tau'}
\end{array}$$
corresponding to the typing rules in Figure~\ref{Terms}.

\smallskip
A full theory of typed abstract syntax with variable binding incorporating
substitution along the lines of~\cite{FiorePlotkinTuri} can be developed
(see,~{\it e.g.},~\cite{FioreHur,FioreSzamozvancev}).  This is however not necessary
for the purposes of the paper.

\medskip
The notions of neutral and normal terms are given by mutual
induction~(see Figure~\ref{NN_Terms}) and, as such, the associated
algebraic notion corresponds to considering a signature endofunctor on
the product category 
$(\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}})^{\TypeClosure\mathrm{T}}
 \times
 (\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}})^{\TypeClosure\mathrm{T}}$.
This endofunctor, with components $\pair{\Sigma_1,\Sigma_2}$, is defined
below:
$$
\left\{\begin{array}{rcl}
(\Sigma_1({\mathscr{X}},{\mathscr{Y}}))_\tau 
=  \VarPSh\tau + \EEE\tau({\mathscr{X}},{\mathscr{Y}})
\end{array}\right.
\qquad\qquad
\left\{\begin{array}{lcl}
(\Sigma_2({\mathscr{X}},{\mathscr{Y}}))_\theta 
& = & \VarPSh\theta + \EEE\theta({\mathscr{X}},{\mathscr{Y}})
\\[2mm]
(\Sigma_2({\mathscr{X}},{\mathscr{Y}}))_\unittype 
& = & 1
\\[2mm]
(\Sigma_2({\mathscr{X}},{\mathscr{Y}}))_{\tau\producttype\tau'} 
& = & 
{\mathscr{Y}}_\tau \times {\mathscr{Y}}_{\tau'}
\\[2mm]
(\Sigma_2({\mathscr{X}},{\mathscr{Y}}))_{\tau\arrowtype\tau'} 
& = & 
({\mathscr{Y}}_{\tau'})^{\VarPSh\tau} 
\end{array}\right.
$$
where
\[\textstyle
\EEE\tau({\mathscr{X}},{\mathscr{Y}}) 
 = \coprod_{\tau'\in\TypeClosure\mathrm{T}}\:
     {\mathscr{X}}_{\tau\producttype\tau'}
     +
     {\mathscr{X}}_{\tau'\producttype\tau}
     +
     ({\mathscr{X}}_{\tau'\arrowtype\tau}\times{\mathscr{Y}}_{\tau'})
\]
for $\theta\in\mathrm{T}$ and $\tau,\tau'\in\TypeClosure\mathrm{T}$.

We write $(\NEPSh{},\NFPSh{})$ for the initial $\pair{\Sigma_1,\Sigma_2}$-algebra
with structure, for $\theta\in\mathrm{T}$ and
$\tau,\tau'\in\TypeClosure\mathrm{T}$, as follows:
\begin{equation} \label{NEandNFPShsOne}
\left\{\begin{array}{rcl}
\VarPSh\tau + \EEE\tau(\NEPSh{},\NFPSh{})
& \stackrightarrow\cong &
\NEPSh\tau
\end{array}\right.
\qquad\qquad
\left\{\begin{array}{rcl}
\VarPSh\theta + \EEE\theta(\NEPSh{},\NFPSh{})
& \stackrightarrow\cong &
\NFPSh\theta
\\[2mm]
1
& \stackrightarrow\cong &
\NFPSh\unittype
\\[2mm]
\NFPSh\tau \times \NFPSh{\tau'}
& \stackrightarrow\cong &
\NFPSh{\tau\producttype\tau'}
\\[2mm]
(\NFPSh{\tau'})^{\VarPSh\tau} 
& \stackrightarrow\cong &
\NFPSh{\tau\arrowtype\tau'}
\end{array}\right.
\end{equation}
Note that we have an isomorphism
\begin{equation} \label{normISO}
\mathsf{norm} 
  \, : \,
  \NEPSh\theta 
  \cong 
  \VarPSh\theta + \EEE\theta(\NEPSh{},\NFPSh{})
  \cong
  \NFPSh\theta
\end{equation}
for all $\theta\in\mathrm{T}$. 

Explicitly, the presheaves $\NEPSh\tau$ and $\NFPSh\tau$ can be respectively
described as the neutral and normal terms
$$
\begin{array}{l}
\NEPSh\tau(\Gamma) 
\ = \ \setof{\, M\ \mid\ \Gamma \vdash_\mathscr{M} M: \tau\, }
\end{array}
\qquad\qquad
\begin{array}{r}
\NFPSh\tau(\Gamma) 
\ = \ \setof{\, N\ \mid\ \Gamma \vdash_\mathscr{N} N: \tau\, }
\end{array}
$$
with presheaf action given by variable 
renaming~(recall~(\ref{Neutral_Renaming_Invariance}) 
and~(\ref{Normal_Renaming_Invariance})), 
and with operations
\begin{equation} \label{NEandNFPShsTwo}
\ \left\{\begin{array}{lcl}
\mathsf{var}_\tau 
& \ : & 
\VarPSh\tau \rightarrow \NEPSh\tau
\\[2mm]
\mathsf{fst}^{(\tau')}_\tau 
& \ : & 
\NEPSh{\tau\producttype\tau'} \rightarrow \NEPSh{\tau}
\\[2mm]
\mathsf{snd}^{(\tau')}_\tau 
& \ : & 
\NEPSh{\tau'\producttype\tau} \rightarrow \NEPSh{\tau}
\\[2mm]
\mathsf{app}^{(\tau')}_\tau 
& \ : & 
\NEPSh{\tau'\arrowtype\tau} \times \NFPSh{\tau'}
  \rightarrow \NEPSh\tau
\end{array}\right.
\qquad\qquad
\left\{\begin{array}{lcl}
\mathsf{var}_\theta 
& \!\! : & 
\VarPSh\theta \rightarrow \NFPSh\theta
\\[2mm]
\mathsf{fst}^{(\tau')}_\theta 
& \!\! : & 
\NEPSh{\theta\producttype\tau'} \rightarrow \NFPSh{\theta}
\\[2mm]
\mathsf{snd}^{(\tau')}_\theta 
& \!\! : & 
\NEPSh{\tau'\producttype\theta} \rightarrow \NFPSh{\theta}
\\[2mm]
\mathsf{app}^{(\tau')}_\theta 
& \!\! : & 
\NEPSh{\tau'\arrowtype\theta} \times \NFPSh{\tau'}
  \rightarrow \NFPSh\theta
\\[2mm]
\mathsf{unit}_\unittype 
& \!\! : & 
1 \stackrightarrow\cong \NFPSh\unittype
\\[2mm]
\mathsf{pair}_{\tau\producttype\tau'} 
& \!\! : & 
\NFPSh\tau \times \NFPSh{\tau'} 
  \stackrightarrow\cong \NFPSh{\tau\producttype\tau'}
\\[2mm]
\mathsf{abs}_{\tau\arrowtype\tau'} 
& \!\! : & 
(\NFPSh{\tau'})^{\VarPSh\tau} 
  \stackrightarrow\cong \NFPSh{\tau\arrowtype\tau'}
\end{array}\right.
\end{equation}
corresponding to the typing rules in Figure~\ref{NN_Terms}. 

Note that every $\Sigma$-algebra ${\mathscr{X}}$ induces a canonical 
$\pair{\Sigma_1,\Sigma_2}$-algebra structure on the pair $({\mathscr{X}},{\mathscr{X}})$ and 
hence, by initiality, homomorphic interpretations 
$(\NEPSh{},\NFPSh{}) \rightarrow ({\mathscr{X}},{\mathscr{X}})$.  Applying this
observation to the initial $\Sigma$-algebra $\TermPSh{}$ we obtain the
embeddings $\NEPSh{} \rightmono \TermPSh{}$ and 
$\NFPSh{} \rightmono \TermPSh{}$ of neutral and normal terms into terms.

\paragraph{Structural induction.}
Initial algebras have the following associated structural induction
principle~\cite{LehmannSmyth}. 
\begin{equation} \label{Induction_Principle}
\begin{minipage}{14.5cm}{\em
Let $\alpha: FA \rightarrow A$ be an
initial algebra for an endofunctor~$F$, if the subobject 
$m: P \rightmono A$ satisfies the closure property of being a
sub~$F$-algebra of $A$, in the sense that the diagram 
$$\xymatrix{
\raisebox{0.55mm}{$FP$} \ar[d]_-{Fm} \ar@{-->}[r] & \ar@{>->}[d]^-m
\raisebox{1.1mm}{$P$} \\
FA \ar[r]_-{\alpha}^-\cong & A
}$$
commutes for a (necessarily unique) map $FP \rightarrow P$, then 
$m: P \rightmono A$ is an isomorphism. 
}\end{minipage}
\end{equation}

For the initial $\Sigma$-algebra~$\TermPSh{}$ (resp.~the initial
$\pair{\Sigma_1,\Sigma_2}$-algebra~$(\NEPSh{},\NFPSh{})$) the structural induction
principle corresponds, in elementary terms, to proving a property of terms
(resp.~of neutral and normal terms) by induction (resp.~simultaneous
induction) on their derivation.
The structural induction principle for the initial 
$\pair{\Sigma_1,\Sigma_2}$-algebra~$(\NEPSh{},\NFPSh{})$ features in the proof of
Theorem~\ref{THEOREM}.

\subsection*{II.1.2\quad Semantics}

As we will see below, every interpretation of base types in a cartesian closed
category induces a canonical semantic typed lambda algebra with respect to
which the unique algebra homomorphism from the initial (term) algebra is the
usual semantics of simply typed terms. 

\paragraph{Nerve functor.}
Every functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ induces the following
situation \begin{equation}\label{Relative_Hom_Diagram}
\begin{array}{c}\xymatrix@C=5pt{ 
\ar@{}[rrrrrrrd]|-{\raisebox{5mm}{$\nt\mbox{\boldmath$\varsigma$}\mbox{$\Downarrow${\tiny Lan}}$}}
\scat C\ \ar@{^(->}[rrrrrrr]^-\mathbf{y}
\ar[drrrr]_-{\mbox{\boldmath$\varsigma$}} &&&&&&&
\mathbf{Set}^{\scat C^\mathrm{op}} \\
&&&& \cat S \ar[urrr]_-{\clone\mbox{\boldmath$\varsigma$}} &&& 
}\end{array}
\end{equation}
where $\clone\mbox{\boldmath$\varsigma$}(A) = \cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),A)$ and where
$(\nt\mbox{\boldmath$\varsigma$}_\Gamma)_{\Gamma'} = \mbox{\boldmath$\varsigma$}_{\Gamma',\Gamma}: 
   \scat C(\Gamma',\Gamma) \rightarrow \cat S(\mbox{\boldmath$\varsigma$}(\Gamma'),\mbox{\boldmath$\varsigma$}(\Gamma))$.
We refer to $\clone\mbox{\boldmath$\varsigma$}: \cat S \rightarrow \mathbf{Set}^{\scat C^\mathrm{op}}$ as the
\Def{$\mbox{\boldmath$\varsigma$}$-nerve functor} and to the presheaf $\clone\mbox{\boldmath$\varsigma$}(A)$ as the
\Def{$\mbox{\boldmath$\varsigma$}$-nerve} of $A$.

\medskip 
Two important properties of nerve functors follow.
\begin{proposition} \label{RelativeHom_Properties}
For a functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ where $\scat C$ is small, the
nerve functor $\clone\mbox{\boldmath$\varsigma$}: \cat S \rightarrow \mathbf{Set}^{\scat C^\mathrm{op}}$ preserves
limits.
Further, for $\mbox{\boldmath$\varsigma$}$ and $\scat C$ cartesian and $\cat S$ cartesian
closed, it also commutes with exponentiation by representables in the sense
that there is a canonical natural isomorphism  
$$\xymatrix@C=50pt{\ar@{}[dr]|(.5)\cong
\cat S \ar[d]_-{\clone\mbox{\boldmath$\varsigma$}}  
\ar[r]^-{\mbox{\boldmath$\varsigma$}(\Gamma) \;\myArrow{\shortarrowlength}{}{}\, (\_\!\_)} & \cat S 
\ar[d]^-{\clone\mbox{\boldmath$\varsigma$}}
\\
\mathbf{Set}^{\scat C^\mathrm{op}} \ar[r]_-{(\_\!\_)^{\mathbf{y}(\Gamma)}}
&
\mathbf{Set}^{\scat C^\mathrm{op}} 
}$$
for all $\Gamma \in \obj\scat C$.
\end{proposition}  
\begin{proof}
The first part is well-known and follows from the canonical natural
isomorphism 
$$\begin{array}{rcl}
\cat S(\mbox{\boldmath$\varsigma$}(\Gamma),L)
& \cong & 
\lim_{\Delta\in\scat D}\: \cat S(\mbox{\boldmath$\varsigma$}(\Gamma),D(\Delta))
\\[2mm]
f & \mapsto & \pair{\, \pi_\Delta \circ f \,}_{\Delta\in\scat D}
\end{array}
\quad\qquad
(\Gamma\in\scat C)
$$
available for any diagram $D: \scat D \rightarrow \cat S$ with limit
$\pair{\, \pi_\Delta: L \rightarrow D(\Delta) \,}_{\Delta\in\scat D}$ 
in $\cat S$. 

For the second part, note that for $\Gamma\in\obj\scat C$ we have the
following situation~(generalising~(\ref{Adjoint_Situation_For_F[T]}))
$$
\begin{array}{c}\xymatrix@C=5pt{\ar@{}[rrrrrd]|(.5){\stackrel{\mathrm{Lan}}{\cong}}
\scat C\ \ar@{^(->}[rrrrrr]^-\mathbf{y}
\ar[d]_-{\xy(0,-1)\ar@{-}(2,-1)\endxy\times\Gamma} &&&&&& 
\mathbf{Set}^{\scat C^\mathrm{op}}
\ar[d]<-1ex>_-{\xy(0,-1)\ar@{-}(2,-1)\endxy\times\mathbf{y}(\Gamma)} \ar@{}[d]|-{\dashv}
\\
\scat C\ \ar@{^(->}[rrrrrr]_-\mathbf{y} &&&&&& 
\mathbf{Set}^{\scat C^\mathrm{op}}
\ar[u]<-1ex>_-{\mathbf{Set}^{(\xy(0,-1)\ar@{-}(2,-1)\endxy\times\Gamma)^\mathrm{op}}}
}\end{array}
$$
from which it follows that

(P^{\mathbf{y}(\Gamma)})(\Delta)
\cong
P(\Delta\times\Gamma)
$
naturally in $\Delta\in\scat C$.  
We thus obtain a canonical isomorphism
$$
\begin{array}{rcl}
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}(\Delta)
& \cong & (\clone\mbox{\boldmath$\varsigma$} A)(\Delta\times\Gamma)
\ = \ \cat S(\mbox{\boldmath$\varsigma$}(\Delta\times\Gamma),A)
\\[2mm]
& \cong & \cat S(\mbox{\boldmath$\varsigma$}(\Delta)\times\mbox{\boldmath$\varsigma$}(\Gamma),A)
\\[2mm]
& \cong & \cat S(\mbox{\boldmath$\varsigma$}(\Delta),\mbox{\boldmath$\varsigma$}(\Gamma)\myArrow{\shortarrowlength}{}{} A)
\ = \ \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}(\Gamma)\myArrow{\shortarrowlength}{}{} A)(\Delta)
\end{array}
$$
natural in $\Gamma,\Delta\in\scat C$ and $A\in\cat S$.
\end{proof}

\paragraph{Initial algebra semantics.}
Using the nerve functor
$\clone{\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy}
 : \cat S \rightarrow \mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$
induced by the cartesian extension
$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy:\F{}[\TypeClosure\mathrm{T}]\rightarrow\cat S$
of an interpretation \mbox{$\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$} of base 
types in a cartesian closed category, the operations
$$\begin{array}{lcl}
\pi_1
& : &
\mbox{\boldmath$s$}\sembracket{\tau} \times \mbox{\boldmath$s$}\sembracket{\tau'}
\rightarrow 
\mbox{\boldmath$s$}\sembracket\tau
\\[2mm]
\pi_2
& : &
\mbox{\boldmath$s$}\sembracket{\tau'} \times \mbox{\boldmath$s$}\sembracket\tau 
\rightarrow 
\mbox{\boldmath$s$}\sembracket\tau
\\[2mm]
\varepsilon
& : &
(\mbox{\boldmath$s$}\sembracket{\tau} \myArrow{\shortarrowlength}{}{} \mbox{\boldmath$s$}\sembracket{\tau'}) 
\times
\mbox{\boldmath$s$}\sembracket{\tau}
\rightarrow 
\mbox{\boldmath$s$}\sembracket{\tau'}
\end{array}$$
in $\cat S$ can be lifted to $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ to
provide a \emph{semantic typed lambda algebra} structure on the family
\begin{equation} \label{Semantic_Algebra_Carrier}
\SemPSh{} 
\ = \
\setof{
        \ \cat S(\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy,\mbox{\boldmath$s$}\sembracket\tau) \
        }_{\tau \in \TypeClosure\mathrm{T}}
\ = \
\setof{ \ \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\tau) \
       
        }_{\tau \in \TypeClosure\mathrm{T}}
\end{equation}
The operations are as follows:
\begin{equation} \label{Semantic_Algebra_Structure}
\begin{minipage}{.925\textwidth}
\begin{enumerate}
\item \label{Semantic_Operations_Var}
$\VarPSh\tau 
\longstackrightarrow{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy$}}
\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\tau)$

\item \label{Semantic_Operations_Unit}
$1 \stackrightarrow\cong \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\unittype)$

\item
$\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau\producttype\tau'})
 \longstackrightarrow{\mbox{\scriptsize$\clone\mbox{\boldmath$s$}(\pi_1)$}}
 \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\tau)$

\item
$\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau'\producttype\tau})
 \longstackrightarrow{\mbox{\scriptsize$\clone\mbox{\boldmath$s$}(\pi_2)$}}
 \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\tau)$

\item \label{Semantic_Operations_Pair}
$\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket\tau)
 \times
 \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau'})
 \stackrightarrow\cong
 \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau\producttype\tau'})$

\item \label{Semantic_Operations_Eval}
$
\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau'\arrowtype\tau})
\times
\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau'})
\stackrightarrow\cong
\clone\mbox{\boldmath$s$}((\mbox{\boldmath$s$}\sembracket{\tau'}\myArrow{\shortarrowlength}{}{}\mbox{\boldmath$s$}\sembracket\tau)
              \times
              \mbox{\boldmath$s$}\sembracket{\tau'})
\longstackrightarrow{\mbox{\scriptsize$\clone\mbox{\boldmath$s$}(\varepsilon)$}}
\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau})
$

\item \label{Semantic_Operations_Abs}
$(\clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau'}))^{\VarPSh\tau}
 \stackrightarrow\cong
 \clone\mbox{\boldmath$s$}(\mbox{\boldmath$s$}\sembracket{\tau\arrowtype\tau'})$
\end{enumerate}
\end{minipage}
\end{equation}
(Note that item~\ref{Semantic_Operations_Var} relies on
diagram~(\ref{Relative_Hom_Diagram}) while
items~\ref{Semantic_Operations_Unit}, \ref{Semantic_Operations_Pair},
\ref{Semantic_Operations_Eval}, and \ref{Semantic_Operations_Abs} rely on
Proposition~\ref{RelativeHom_Properties}.  Similar applications of this
proposition will be used throughout without further reference.)

\medskip
By initiality, the semantic typed lambda algebra induces semantic homomorphic
interpretations $\Termsem{}: \TermPSh{} \rightarrow \SemPSh{}$ and
$(\NEsem{},\NFsem{}): (\NEPSh{},\NFPSh{}) \rightarrow (\SemPSh{},\SemPSh{})$.
These are related as shown below
\begin{equation}\label{Initial_Algebra_Semantics}
\begin{array}{c}\xymatrix{
\NEPSh{}\ \ar[rd]_-{\NEsem{}} \ar@{>->}[r] & \TermPSh{} \ar[d]_-{\Termsem{}} 
& \ar@{>->}[l] \ar[ld]^-{\NFsem{}} \ \NFPSh{} \\ 
& \SemPSh{} & 
}\end{array}
\end{equation}
Indeed, by the initiality of $(\NEPSh{},\NFPSh{})$,
(\ref{Initial_Algebra_Semantics}) directly follows from the fact that the
homomorphism property of $\Termsem{}: \TermPSh{} \rightarrow \SemPSh{}$
amounts to the commutativity of the diagrams in Appendix~\ref{Appendix_l} and
that the homorphism property of
$(\NEsem{},\NFsem{}): (\NEPSh{},\NFPSh{}) \rightarrow (\SemPSh{},\SemPSh{})$
amounts to the commutativity of the diagrams in Appendix~\ref{Appendix_(m,n)}.

Explicitly, for $\tau\in\TypeClosure\mathrm{T}$, the mapping
$\Termsem\tau: \TermPSh\tau \rightarrow \SemPSh\tau$ is the standard semantic
interpretation of terms
\begin{equation}\label{StandardSemanticInterpretation}
t\in\TermPSh\tau(\Gamma)
\xymatrix{\ar@{|->}[r]^-{\Termsem\tau}&}
\mbox{\boldmath$s$}\sembracket{\Gamma \vdash t: \tau}
  \in\cat S(\mbox{\boldmath$s$}\sembracket\Gamma,\mbox{\boldmath$s$}\sembracket\tau)
\end{equation}
whilst $\NEsem\tau: \NEPSh\tau \rightarrow \SemPSh\tau$ and 
$\NFsem\tau: \NFPSh\tau \rightarrow \SemPSh\tau$ are, respectively, the 
semantic interpretations of neutral and normal terms.  

\section*{II.2\quad Normalisation by evaluation via categorical glueing}

We will now see how, by working with \emph{intensional Kripke relations}, the
analysis of normalisation given in Section~I.2 amounts to normalisation by
evaluation.   
As in that section, we will work with semantic models of (covariant)
presheaves in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ over nerves induced
by interpretations~$\mbox{\boldmath$s$}$
of the set of base types~$\mathrm{T}$ in arbitrary cartesian closed
categories~(see~(\ref{mu_Interpretation})).  
This level of generality allows the definition of normalisation functions
$\nf\tau\mbox{\boldmath$s$}: \TermPSh\tau \rightarrow \NFPSh\tau$
($\tau\in\TypeClosure\mathrm{T}$) in
$\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ over the
$\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy$-nerve of $\mbox{\boldmath$s$}\sembracket\tau$
(Corollary~\ref{Corollary_Correctness_Two}) that are parametric on the
interpretation~$\mbox{\boldmath$s$}$.  
Crucially, the normalisation functions will be shown to be parametrically
polymorphic, in the sense of being interpretation
independent~(Corollary~\ref{Corollary_nfCoincidence}).
This is methodologically important.  
Firstly, as in Corollary~\ref{Corollary_BetaEtaLongNormalForms}, the
consideration of the universal interpretation of base types into the free
cartesian closed category over them leads to our solution of the
\emph{intensional normalisation problem}~(see the discussions after 
Corollaries~\ref{Corollary_Correctness_Two} and~\ref{Corollary_nfCoincidence}
in~\S~\emph{Normalisation function} below) stated in the Introduction.  
Secondly, the consideration of the trivial interpretation of base types in the
trivial cartesian closed category leads to a normalisation algorithm from
which a normalisation program is 
synthesised~(see~\S~\emph{Normalisation algorithm} below).  

\paragraph{Intensional Kripke relations.}
The category of intensional $\scat C$-Kripke relations of arity 
$\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ is defined as the glueing
of $\mathbf{Set}^{\scat C^\mathrm{op}}$ and $\cat S$ along the nerve functor 
$\clone\mbox{\boldmath$\varsigma$}: \cat S \rightarrow \mathbf{Set}^{\scat C^\mathrm{op}}$.  
That is, as the comma category
\mbox{$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$} of objects given by triples 
$(P,p,A)$ with $P\in\obj{\mathbf{Set}^{\scat C^\mathrm{op}}}$, $A\in\obj{\cat S}$, and
$p: P \rightarrow \clone\mbox{\boldmath$\varsigma$}(A)$ in $\mathbf{Set}^{\scat C^\mathrm{op}}$, and of
morphisms $(P,p,A) \rightarrow (P',p',A')$ given  
by pairs 
$$
(~\varphi:P\rightarrow P'\mbox{ in $\mathbf{Set}^{\scat C^\mathrm{op}}$} 
 ,~
 f:A\rightarrow A'\mbox{ in $\cat S$}
 ~)
$$
such that the diagram
$$
\begin{array}{c}\xymatrix{
P \ar[d]_-p \ar[rr]^-{\varphi} && P' \ar[d]^-{p'} \\
\clone\mbox{\boldmath$\varsigma$}(A) \ar[rr]_-{\clone\mbox{\boldmath$\varsigma$}(f)} && \clone\mbox{\boldmath$\varsigma$}(A')
}\end{array}
\quad
\mbox{ in $\mathbf{Set}^{\scat C^\mathrm{op}}$}
$$
commutes. 

\begin{example} \label{Trivial_Glueing}
The category of intensional $\scat C$-Kripke relations of arity the unique
functor to the terminal category is (isomorphic to) the presheaf topos
$\mathbf{Set}^{\scat C^\mathrm{op}}$.  
\end{example}

As it is well-known (see,~{\it e.g.},~\cite{LambekScott,Crole,Taylor}), for $\cat S$
cartesian closed, the glueing category $\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$ is
also cartesian closed. 
Indeed, the cartesian closed structure of
$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$ is given as follows.  
\begin{description}
\item[](Products)
  The terminal object is 
  $(1,t,1)$ where $t$ is the unique map 
  $1\stackrightarrow\cong\clone\mbox{\boldmath$\varsigma$}(1)$.

  The binary 
  product $(P,p,A)\times(Q,q,B)$
  of $(P,p,A)$ and $(Q,q,B)$
  is $(P\times Q,r,A\times B)$ where $r$ is the composite
  
  P\times Q
    \longstackrightarrow{p\times q}
      \clone\mbox{\boldmath$\varsigma$}(A)\times\clone\mbox{\boldmath$\varsigma$}(B)
        \stackrightarrow\cong
          \clone\mbox{\boldmath$\varsigma$}(A\times B)$

\item[](Exponentials)
  The exponential \mbox{$(P,p,A)\myArrow{\shortarrowlength}{}{}(Q,q,B)$} of $(P,p,A)$ and
  $(Q,q,B)$ is $(R,r,A\myArrow{\shortarrowlength}{}{} B)$ in the pullback diagram
  \begin{equation}\label{Exponential_By_Pullback}
  \begin{array}{c}\xymatrix{\ar@{}[rrrrd]|-{\mathrm{pb}}
  R \ar[rrrr] \ar[d]_-{r} && && \ar[d]^-{q^P} Q^{P}
  \\
  \clone\mbox{\boldmath$\varsigma$}(A\myArrow{\shortarrowlength}{}{} B) \ar[rr] &&
  (\clone\mbox{\boldmath$\varsigma$} B)^{(\clone\mbox{\boldmath$\varsigma$} A)}
  \ar[rr]_-{(\clone\mbox{\boldmath$\varsigma$} B)^p} && 
  (\clone\mbox{\boldmath$\varsigma$} B)^{P}
  }\end{array}
  \end{equation}
  where the map 
  $\clone\mbox{\boldmath$\varsigma$}(A\myArrow{\shortarrowlength}{}{} B) \rightarrow (\clone\mbox{\boldmath$\varsigma$} B)^{(\clone\mbox{\boldmath$\varsigma$} A)}$ 
  is the exponential transpose of the composite
  $$
  \clone\mbox{\boldmath$\varsigma$}(A\myArrow{\shortarrowlength}{}{} B)\times\clone\mbox{\boldmath$\varsigma$}(A)
    \stackrightarrow\cong
  \clone\mbox{\boldmath$\varsigma$}((A\myArrow{\shortarrowlength}{}{} B)\times A)
    \longstackrightarrow{\clone\mbox{\boldmath$\varsigma$}(\varepsilon)}
  \clone\mbox{\boldmath$\varsigma$}(B)
  \quad.
  $$

  Explicitly, one may take $R(c)$ to be
  \begin{equation}\label{PShExponentialNaturality}
  \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
    \left\{\begin{array}{l|l}
      ( \, f: \mbox{\boldmath$\varsigma$}(c)\to A\myArrow{\shortarrowlength}{}{} B 
          \, , \, 
          \varphi : \mathbf{y}(c)\times P\to Q
        \, )
      &
      \begin{array}{l}
        \forall\, \rho: c'\to c.\ \forall\, a\in P(c').\
        \\[.5mm]
        \quad
        q_{c'}(\varphi_{c'}(\rho,a))
        =
        \varepsilon \circ \pair{ f\circ \mbox{\boldmath$\varsigma$}(\rho) , p_{c'}(a) }
      \end{array}
      \end{array}\right\}
  \end{equation}
  with $r$ projecting pairs onto their first component.
\end{description}
\begin{proposition}\label{Gluecat_CCC}
Let $\scat C$ be a small category and let $\cat S$ be a cartesian closed
category.  For a functor \mbox{$\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$}, the 
glueing category \mbox{$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$} is cartesian
closed and the forgetful functor
$\pi
 : {\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}} \rightarrow \cat S
 : (P,p,A)\mapsto A$
preserves the cartesian closed structure strictly.
\end{proposition}

\begin{remark}
The category of $\scat C$-Kripke relations $\K\mbox{\boldmath$\varsigma$}$ is a full subcategory of
the glueing category $\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone{\mbox{\boldmath$\varsigma$}}$ via the mapping
$(R,A) \mapsto (R,R\rightembedding\clone\mbox{\boldmath$\varsigma$}(A),A)$.  
On the other hand, every glued object $(P,f,A)$ has an associated Kripke
relation given by the extension of the map~$f$ (as shown in the diagram below,
where $\mathrm{im}(f)$ denotes the image of $f$)
$$\xymatrix@C=5pt@R=10pt{
P \ar[dd]_-f \ar@{->>}[rd] \\
& \mathrm{im}(f) \ar@{^(->}[dl] \\
\clone\mbox{\boldmath$\varsigma$}(A) 
}$$
and the mapping $\mathrm{im}: (P,f,A) \mapsto (\mathrm{im}(f),A)$ exhibits $\K\mbox{\boldmath$\varsigma$}$ as a
reflective subcategory of $\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$.  
For $\cat S$ cartesian closed, as can be readily seen from the explicit
descriptions of finite products in $\K\mbox{\boldmath$\varsigma$}$ and
$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$, the reflection 
$\mathrm{im}: \K\mbox{\boldmath$\varsigma$} \to \mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$ preserves the cartesian
structure and, therefore, $\K\mbox{\boldmath$\varsigma$}$ is an exponential ideal of
$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$ (as can also be readily seen from the
descriptions of exponentials in $\K\mbox{\boldmath$\varsigma$}$ and
$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$).  Thus, for $(P,p,A)$ and $(Q,q,A)$ in 
$\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$, there are inclusions
\[
  \mathrm{im}( \ (P,p,A)\myArrow{\shortarrowlength}{}{}\!(Q,q,B) \ )(c)
  \ \subseteq \
  ( \ \mathrm{im}(P,p,A) \!\supset \mathrm{im}(Q,q,B) \ )(c)
  \qquad(\,c\in\obj{\scat C}\,)
\]
where 
  \[\begin{array}{l}
  \mathrm{im}( \ (P,p,A)\myArrow{\shortarrowlength}{}{}\!(Q,q,B) \ )(c)
  \\[2.5mm] \quad
    =
    \left\{\begin{array}{l|l}
      f: \mbox{\boldmath$\varsigma$}(c)\to A\myArrow{\shortarrowlength}{}{} B 
      &
      \begin{array}{l}
        \exists\, \varphi : \mathbf{y}(c)\times P\to Q.\
        \forall\, \rho: c'\to c.\ \forall\, a\in P(c').\
        \\[1mm]
        \quad
        q_{c'}(\varphi_{c'}(\rho,a))
        =
        \varepsilon \circ \pair{ f\circ \mbox{\boldmath$\varsigma$}(\rho) , p_{c'}(a) }
      \end{array}
      \end{array}\right\}
  \end{array}\]
and
\[\begin{array}{l}
  ( \ \mathrm{im}(P,p,A) \!\supset \mathrm{im}(Q,q,B) \ ) (c) 
  \\[2.5mm] \quad
    =
    \left\{\begin{array}{l|l}
      f: \mbox{\boldmath$\varsigma$}(c)\to A\myArrow{\shortarrowlength}{}{} B 
      &
      \begin{array}{l}
        \forall\, \rho: c'\to c.\ \forall\, a\in P(c').\
        \exists\, b\in Q(c').\
        \\[1mm]
        \quad
        q_{c'}(b)
        =
        \varepsilon \circ \pair{ f\circ \mbox{\boldmath$\varsigma$}(\rho) , p_{c'}(a) }
      \end{array}
      \end{array}\right\}\ .
\end{array}\]
These inclusions may be strict; as it happens, for instance, when
$\scat C^\mathrm{op}=\F{}$~(the category of untyped contexts and renamings), $\mbox{\boldmath$\varsigma$}$ is
the unique functor to the trivial cartesian closed category, $Q=\mathbf{y}(1)$ (for
a singleton context $1$), $P=\mathrm{im}(Q\to\clone\mbox{\boldmath$\varsigma$}(1))$, and
$c=0$~(the empty context).  Indeed, in this situation,
$(P\myArrow{\shortarrowlength}{}{}\!\!Q)(c)\cong\mathbf{Set}^{\F{}}(P,Q)=\emptyset$ whilst
$(\mathrm{im}(p)\supset\mathrm{im}(q))(c)=(P\supset P)(c)=\setof{\mathrm{id}}$.  
Thus, in general, the reflection 
$\mathrm{im}: \K\mbox{\boldmath$\varsigma$} \to \mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$ does not preserve
exponentials.
\end{remark}

Now, note that~(\ref{Relative_Hom_Diagram}) induces the embedding 
$$\begin{array}{rcl}
\scat C & \longstackrightembedding\ext\yon & \mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}
\\[1mm]
\Gamma 
& \mapsto & 
( \ \mathbf{y}(\Gamma)\ , 
  \ \mathbf{y}(\Gamma) 
      \longstackrightarrow{\nt\mbox{\boldmath$\varsigma$}_\Gamma} 
        \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$} \Gamma)\ ,
  \ \mbox{\boldmath$\varsigma$}(\Gamma)\ )
\end{array}$$
extending both 
the Yoneda embedding $\mathbf{y}:\scat C\rightembedding\mathbf{Set}^{\scat C^\mathrm{op}}$ and the
functor $\mbox{\boldmath$\varsigma$}:\scat C\rightarrow\cat S$ 
$$\xymatrix@R=0pt{
& \scat C \ar@{^(->}[ldddd]_-\mathbf{y} \ar@{^(->}[dddd]^-\ext\yon \ar[rdddd]^-\mbox{\boldmath$\varsigma$} 
\\ \\ \\ \\
\mathbf{Set}^{\scat C^\mathrm{op}} & \ar[l] \mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$} \ar[r] & \cat S
\\
P & \ar@{|->}[l]_-\varpi (P,p,A) \ar@{|->}[r]^-\pi &  A
}$$
and satisfying the following extended form of the Yoneda Lemma (which we will
use in \S~\emph{Normalisation function} below).
\begin{lemma}\Rem{(Extended Yoneda Lemma)}
For a functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ where $\scat C$ is a
small category, the natural transformation
$$
\Hom{\ext\yon(\xy(0,-1)\ar@{-}(2,-1)\endxy),(P,p,A)} \rightarrow P(\xy(0,-1)\ar@{-}(2,-1)\endxy):\
(\varphi,f) \mapsto \varphi(\mathrm{id})
\quad,
$$
where $\Hom{\xy(0,-1)\ar@{-}(2,-1)\endxy,\xy(0,-1)\ar@{=}(2,-1)\endxy}$ denotes the hom-functor of the glueing
category $\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$, is an isomorphism making
the following diagram  
$$\xymatrix@R=0pt@C=10pt{
\Hom{\ext\yon(\xy(0,-1)\ar@{-}(2,-1)\endxy),(P,p,A)} \ar[rr]^-\cong \ar[ddddr]_-\pi &&
P(\_\!\_) \ar[ddddl]^-p
\\ \\ \\ \\
& \cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),A) 
}$$
commute.
\end{lemma}
\begin{proof}
Follows from the fact that, for $\varphi: \mathbf{y}(\Gamma) \rightarrow P$ in
$\mathbf{Set}^{\scat C^\mathrm{op}}$ and $f: \mbox{\boldmath$\varsigma$}(\Gamma) \rightarrow A$ in $\cat S$,
the diagram
$$\xymatrix{
\mathbf{y}(\Gamma) \ar[d]_{\nt\mbox{\boldmath$\varsigma$}_\Gamma} \ar[r]^-\varphi &  P \ar[d]^-p
\\
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),\mbox{\boldmath$\varsigma$}(\Gamma)) \ar[r]_-{f \circ \_\!\_} &
\cat S(\mbox{\boldmath$\varsigma$}(\xy(0,-1)\ar@{-}(2,-1)\endxy),A)
}$$
commutes if and only if $f = p_\Gamma(\varphi_\Gamma(\mathrm{id}_\Gamma))$.
\end{proof}

\begin{proposition} \label{Glued_Exponential_to_Representable}
For a functor $\mbox{\boldmath$\varsigma$}: \scat C \rightarrow \cat S$ where $\scat C$ is
small, $\scat C$ and $\mbox{\boldmath$\varsigma$}$ are cartesian, and $\cat S$ is cartesian
closed, we have that 
$\ext\yon: \scat C \rightembedding \mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$
preserves products and that the exponential
$(P,p,A)^{\ext\yon(\Gamma)}$ in $\mathbf{Set}^{\scat C^\mathrm{op}}\!\downarrow\!\clone\mbox{\boldmath$\varsigma$}$
can be described as $(P^{\mathbf{y}(\Gamma)},p',\mbox{\boldmath$\varsigma$}(\Gamma)\arrowtype A)$ where
$p'$ is the composite
$$
P^{\mathbf{y}(\Gamma)} 
  \longstackrightarrow{p^{\mathbf{y}(\Gamma)}}
    (\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}
      \stackrightarrow\cong 
        \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}(\Gamma)\myArrow{\shortarrowlength}{}{} A)
\quad.
$$
\end{proposition}
\begin{proof}
The first part follows from the commutativity of
$$\xymatrix{
\mathbf{y}(\Gamma\times\Delta) \ar[r]^-\cong
\ar[dd]_-{\nt\mbox{\boldmath$\varsigma$}_{\Gamma\times\Delta}} & 
\mathbf{y}(\Gamma) \times \mathbf{y}(\Delta)
\ar[d]^-{\nt\mbox{\boldmath$\varsigma$}_\Gamma\times\nt\mbox{\boldmath$\varsigma$}_\Delta}
\\
& 
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)\times\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Delta)
\ar[d]^-\cong
\\
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}(\Gamma\times\Delta)) \ar[r]_-\cong
& 
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}(\Gamma)\times\mbox{\boldmath$\varsigma$}(\Delta)) 
}$$
for all $\Gamma,\Delta\in\obj\scat C$. 

For the second part, since the exponential $(P,p,A)^{\ext\yon(\Gamma)}$
is given by pulling back 
the map
$p^{\mathbf{y}(\Gamma)}: 
   P^{\mathbf{y}(\Gamma)} \rightarrow (\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}$
along the composite
$$
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A)
  \stackrightarrow f
(\clone\mbox{\boldmath$\varsigma$} A)^{\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)}
  \longlongstackrightarrow{(\clone\mbox{\boldmath$\varsigma$} A)^{\nt\mbox{\boldmath$\varsigma$}_\Gamma}}
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}
$$
(recall~(\ref{Exponential_By_Pullback})), where $f$ is the exponential
transpose of  
$$\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A) \times \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)
  \stackrightarrow\cong
 \clone\mbox{\boldmath$\varsigma$}((\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A) \times \mbox{\boldmath$\varsigma$}\Gamma)
  \longstackrightarrow{\clone\mbox{\boldmath$\varsigma$}(\varepsilon)}
 \clone\mbox{\boldmath$\varsigma$}(A)\quad,$$
it will be enough to show that the composite
$$
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}
  \stackrightarrow\cong
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A)
  \stackrightarrow f
(\clone\mbox{\boldmath$\varsigma$} A)^{\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)}
  \longlongstackrightarrow{(\clone\mbox{\boldmath$\varsigma$} A)^{\nt\mbox{\boldmath$\varsigma$}_\Gamma}}
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)}
$$
is the identity.  This is indeed the case as follows from the
commutativity of the diagram below
{\scriptsize$$
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
\xymatrix{
& 
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A) \times \mathbf{y}(\Gamma)
\ar[rr]^-{\mbox{$f \times \mathrm{id}$}} 
\ar[dr]^-{\mbox{$\mathrm{id}\times\nt\mbox{\boldmath$\varsigma$}_\Gamma$}}
\ar[d]^-{\mbox{$\cong\times\mathrm{id}$}}
& & 
(\clone\mbox{\boldmath$\varsigma$} A)^{\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)} \times \mathbf{y}(\Gamma)
\ar[rd]^-{\mbox{$\mathrm{id}^{\nt\mbox{\boldmath$\varsigma$}_\Gamma}\times\mathrm{id}$}} 
\ar[d]^-{\mbox{$\mathrm{id}\times\nt\mbox{\boldmath$\varsigma$}_\Gamma$}}
&
\\
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)} \times \mathbf{y}(\Gamma) 
\ar[ru]^-{\mbox{$\cong\times\mathrm{id}$}} 
\ar[dddrr]_-{\mbox{$\varepsilon$}}
\ar[r]^-{\mbox{$\cong\times\mathrm{id}$}}
& 
(\clone\mbox{\boldmath$\varsigma$} A)(\xy(0,-1)\ar@{-}(2,-1)\endxy\times\Gamma) \times \mathbf{y}(\Gamma)
\ar[r]^-{\mbox{$\cong\times\nt\mbox{\boldmath$\varsigma$}_\Gamma$}}
\ar[dddr]_-{\mbox{$e$}}
& 
\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma \myArrow{\shortarrowlength}{}{} A) \times \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)
\ar[r]^-{\mbox{$f\times \mathrm{id}$}}
\ar[d]^-{\mbox{$\cong$}}
& 
(\clone\mbox{\boldmath$\varsigma$} A)^{\clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$} \Gamma)} 
  \times \clone\mbox{\boldmath$\varsigma$}(\mbox{\boldmath$\varsigma$}\Gamma)
\ar[dddl]^-{\mbox{$\varepsilon$}}
& 
(\clone\mbox{\boldmath$\varsigma$} A)^{\mathbf{y}(\Gamma)} \times \mathbf{y}(\Gamma)
\ar[dddll]^-{\mbox{$\varepsilon$}}
\\
& & 
\clone\mbox{\boldmath$\varsigma$}((\mbox{\boldmath$\varsigma$}\Gamma\myArrow{\shortarrowlength}{}{} A)\times \mbox{\boldmath$\varsigma$}\Gamma)
\ar[dd]|-{\mbox{$\clone\mbox{\boldmath$\varsigma$}(\varepsilon)$}}
& & 
\\
\\
& & \clone\mbox{\boldmath$\varsigma$}(A) & &
}$$}%
where 
\begin{equation} \label{RepresentableExponentialEvaluationMap}
e_P 
\, : \, 
P(\xy(0,-1)\ar@{-}(2,-1)\endxy\times\Gamma)\times\mathbf{y}(\Gamma) \rightarrow P(\xy(0,-1)\ar@{-}(2,-1)\endxy)
\, : \, 
(x,\rho) \mapsto (P\pair{\mathrm{id},\rho})(x)
\end{equation}
denotes the counit of the adjunction 
$\xy(0,-1)\ar@{-}(2,-1)\endxy \times \mathbf{y}(\Gamma) 
   \dashv \mathbf{Set}^{(\xy(0,-1)\ar@{-}(2,-1)\endxy\times\Gamma)^\mathrm{op}}: 
     \mathbf{Set}^{\scat C^\mathrm{op}} \rightarrow \mathbf{Set}^{\scat C^\mathrm{op}}$.
\end{proof}

\paragraph{Glueing syntax and semantics.}
Let \mbox{$\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$} be an interpretation of
base types in a cartesian closed category.  The embedding
\mbox{$\ext\yon: \F{}[\TypeClosure\mathrm{T}] \rightembedding \mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$}
restricted to types $\tau\in\TypeClosure\mathrm{T}$ yields the glued 
object
$$
\Varobj\tau 
\ = \
\ext\yon\ctxtemb\tau
\ = \
(\ \VarPSh\tau\ ,\ 
   \VarPSh\tau
     \longstackrightarrow{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket{\xy(0,-1)\ar@{-}(2,-1)\endxy}$}}  
       \SemPSh\tau\ ,\
   \mbox{\boldmath$s$}\sembracket\tau\ )
\qquad\mbox{in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$}
$$
glueing the syntax and semantics of variables.  In the same
spirit, glueing the syntax and semantics of neutral and normal
terms~(see~(\ref{Initial_Algebra_Semantics})) we obtain the glued objects   
$$
\begin{array}{rcl}
\NEobj\tau & = & 
(\ \NEPSh\tau\ ,\ 
   \NEPSh\tau\longstackrightarrow{\NEsem\tau}\SemPSh\tau\ ,\
   \mbox{\boldmath$s$}\sembracket\tau\ )
\\[2mm]
\NFobj\tau & = & 
(\ \NFPSh\tau\ ,\ 
   \NFPSh\tau\longstackrightarrow{\NFsem\tau}\SemPSh\tau\ ,\
   \mbox{\boldmath$s$}\sembracket\tau\ )
\end{array}
$$
in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

Having constructed the $\pair{\Sigma_1,\Sigma_2}$-algebra structure on
$(\SemPSh{},\SemPSh{})$ by lifting the semantic operations in
$\cat S$~(recall~(\ref{Semantic_Algebra_Carrier})
and~(\ref{Semantic_Algebra_Structure})), the homomorphism property of the
semantic interpretation 
$(\NEsem{},\NFsem{}):(\NEPSh{},\NFPSh{}) \rightarrow (\SemPSh{},\SemPSh{})$
(see Appendix~\ref{Appendix_(m,n)}) 
entails the two propositions below,
which show how the algebraic operations on the initial
$\pair{\Sigma_1,\Sigma_2}$-algebra $(\NEPSh{},\NFPSh{})$ and on the semantic
$\pair{\Sigma_1,\Sigma_2}$-algebra $(\SemPSh{},\SemPSh{})$ can be glued to
yield operations in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$ on the pair of families of glued objects 
$( \setof{ \NEobj\tau }_{\tau\in\TypeClosure\mathrm{T}}\ ,\ 
   \setof{ \NFobj\tau }_{\tau\in\TypeClosure\mathrm{T}} )$.
\begin{proposition} \label{mu_Operations}
Let $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$ be an interpretation of base
types in a cartesian closed category.
\begin{enumerate}
\item \label{mu_Operations_One}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of maps
$$
( \
\mathsf{var}_\tau: \VarPSh\tau \rightarrow \NEPSh\tau
\ , \
\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\tau$}
\ )
$$
constitute a map $\Varobj\tau \rightarrow \NEobj\tau$ in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{mu_Operations_Two}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of maps
$$
( \
\mathsf{fst}^{(\tau')}_\tau: \NEPSh{\tau\producttype\tau'} \rightarrow \NEPSh\tau
\ , \
\pi_1: 
  \mbox{\boldmath$s$}\sembracket{\tau}\times\mbox{\boldmath$s$}\sembracket{\tau'}
  \rightarrow
  \mbox{\boldmath$s$}\sembracket{\tau}
\ )
$$
constitute a map $\NEobj{\tau\producttype\tau'} \rightarrow \NEobj\tau$ in
$\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{mu_Operations_Three}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of maps
$$
( \ 
\mathsf{snd}^{(\tau')}_\tau: \NEPSh{\tau'\producttype\tau} \rightarrow \NEPSh\tau
\ , \
\pi_2: 
  \mbox{\boldmath$s$}\sembracket{\tau'}\times\mbox{\boldmath$s$}\sembracket{\tau}
  \rightarrow
  \mbox{\boldmath$s$}\sembracket{\tau}
\ )
$$
constitute a map $\NEobj{\tau'\producttype\tau} \rightarrow \NEobj\tau$ in
$\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{mu_Operations_Four}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of maps
$$
( \ 
\mathsf{app}^{(\tau')}_\tau: 
  \NEPSh{\tau'\arrowtype\tau}\times\NFPSh{\tau'}
  \rightarrow
  \NEPSh{\tau}
\ , \
\varepsilon: (\mbox{\boldmath$s$}\sembracket{\tau'}\myArrow{\shortarrowlength}{}{}\mbox{\boldmath$s$}\sembracket\tau)
       \times
       \mbox{\boldmath$s$}\sembracket{\tau'}
       \rightarrow
       \mbox{\boldmath$s$}\sembracket\tau
\ ) 
$$
constitute a map 
$\NEobj{\tau'\arrowtype\tau} \times \NFobj{\tau'} 
 \rightarrow 
 \NEobj\tau$ 
in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.
\end{enumerate}
\end{proposition}
\begin{proof}
Items~\ref{mu_Operations_One}, \ref{mu_Operations_Two},
\ref{mu_Operations_Three}, and \ref{mu_Operations_Four} respectively follow
from~(\ref{Proof_Of_mu_Operation_One}), (\ref{Proof_Of_mu_Operation_Two}),
(\ref{Proof_Of_mu_Operation_Three}), and (\ref{Proof_Of_mu_Operation_Four}) in
Appendix~\ref{Appendix_(m,n)}.
\end{proof}
\begin{proposition} \label{nu_Operations}
Let $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$ be an interpretation of base
types in a cartesian closed category.
\begin{enumerate}
\item \label{nu_Operation_One}
For a base type $\theta \in \mathrm{T}$, the pair of isomorphisms
$$
( \
\NEPSh\theta 
  \cong \VarPSh\theta+\EEE\theta(\NEPSh{},\NFPSh{})
    \cong \NFPSh\theta
\ ,\ 
\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}(\theta)$}}
\ )
$$
constitute an isomorphism $\NEobj\theta \cong \NFobj\theta$ in
$\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{nu_Operation_Two}
The pair of isomorphisms
$$ 
( \
\mathsf{unit}_\unittype: 1 \stackrightarrow\cong \NFPSh\unittype
\ , \
\mathrm{id}_1
\ )
$$
constitute an isomorphism $1 \stackrightarrow\cong \NFobj\unittype$
in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{nu_Operation_Three}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of isomorphisms
$$
( \ 
\mathsf{pair}_{\tau\producttype\tau'}:
  \NFPSh\tau \times \NFPSh{\tau'}
    \stackrightarrow\cong
      \NFPSh{\tau\producttype\tau'}
\ , \
\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\tau\times\mbox{\boldmath$s$}\sembracket{\tau'}$}}
\ )
$$
constitute an isomorphism 
$\NFobj\tau\times\NFobj{\tau'} 
 \medstackrightarrow\cong
 \NFobj{\tau\producttype\tau'}$ 
in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.

\item \label{nu_Operation_Four}
For $\tau, \tau' \in \TypeClosure\mathrm{T}$, the pair of isomorphisms
$$
( \ 
\mathsf{abs}_{\tau\arrowtype\tau'}: 
  {\NFPSh{\tau'}}^{\VarPSh\tau} 
  \stackrightarrow\cong
  \NFPSh{\tau\arrowtype\tau'}
\ , \
\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\tau\myArrow{\shortarrowlength}{}{}\mbox{\boldmath$s$}\sembracket{\tau'}$}}
\ )
$$
constitute an isomorphism 
${\NFobj{\tau'}}^{\Varobj\tau} 
 \medstackrightarrow\cong 
 \NFobj{\tau\arrowtype\tau'}$
in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$.
\end{enumerate}
\end{proposition}
\begin{proof}
Items~\ref{nu_Operation_One}, \ref{nu_Operation_Two},
\ref{nu_Operation_Three}, and \ref{nu_Operation_Four}
respectively follow from 
~(\ref{Proof_Of_mu_Operation_One}-
\ref{Proof_Of_nu_Operation_One(iv)}),
(\ref{Proof_Of_nu_Operation_Two}),
(\ref{Proof_Of_nu_Operation_Three}), 
and
(\ref{Proof_Of_nu_Operation_Four}) (relying on
Proposition~\ref{Glued_Exponential_to_Representable})
in Appendix~\ref{Appendix_(m,n)}.
\end{proof}
Note that the above operations on glued objects are given by pairs of
syntactic operations together with their associated semantic meaning in the
case of 
neutral terms~(Proposition~\ref{mu_Operations}) 
and together with the identity in the case of 
normal terms~(Proposition~\ref{nu_Operations}). 

\paragraph{Normalisation by evaluation.}
Let $\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$ be an interpretation of base
types in a cartesian closed category.  Consider the interpretation
\begin{equation} \label{mu_Interpretation}
\begin{array}{rcl}
\mathrm{T} & \longstackrightarrow{\ext\mbox{\boldmath$s$}} & \mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$} \\
\theta & \mapsto & \NEobj\theta
\end{array}
\end{equation}
By Proposition~\ref{Gluecat_CCC}, the semantics of terms induced by
$\ext\mbox{\boldmath$s$}$ in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$ extends the semantics induced by $\mbox{\boldmath$s$}$ in
$\cat S$; that is, 
the denotation $\ext\mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}$ is a pair 
of the form 
\[
(\ \mbox{\boldmath$s$}'\sembracket{\Gamma\vdash t:\tau} 
   \ , \
   \mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}) \ )
\]
such that, letting 
\[
\ext\mbox{\boldmath$s$}\sembracket\tau
\ = \
(\, \NSSemPSh\tau \,,\, \NSsem\tau \,,\, \mbox{\boldmath$s$}\sembracket\tau \,)
\enspace, 
\]
the diagram
$$\xymatrix@R=20pt@C=6pt{
\prod_{i=1,n} \NSSemPSh{\tau_i}
\ar[d]_-{\prod_{i=1,n}\NSsem{\tau_i}} 
\ar[r]^-{\mbox{\scriptsize$\mbox{\boldmath$s$}'\sembracket{\Gamma\vdash t:\tau}$}} 
& \NSSemPSh\tau \ar[dd]^-{\NSsem\tau} 
\\
\prod_{i=1,n} 
  \cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\tau_i})
\ar[d]|-\cong
\\
\cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\Gamma}) 
\ar[r]_-{\raisebox{-4mm}{\scriptsize
         $\mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}\circ\_\!\_$}}
& \cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\tau}) 
}$$
commutes for all $\Gamma=\pair{x_i:\tau_i}_{i=1,n}$. 

We now aim at defining maps 
$\xymatrix@C=15pt{\NEPSh\tau\ar@{.>}[r]&\NSSemPSh\tau\ar@{.>}[r]&\NFPSh\tau}$
($\tau\in\TypeClosure\mathrm{T}$)
such that
\begin{equation} \label{uq_Maps}
\begin{array}{c}\xymatrix@R=15pt{
\NEPSh\tau \ar@{.>}[r] \ar[dr]_-{\NEsem\tau} & \NSSemPSh\tau \ar@{.>}[r]
\ar[d]_-{\NSsem\tau} & \ar[dl]^-{\NFsem\tau} \NFPSh\tau \\
& \cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket\tau) 
}\end{array}
\end{equation}
commutes; so that, for all terms 
$\Gamma\vdash t:\tau$~($\Gamma=\pair{x_i:\tau_i}_{i=1,n}$), the diagram
below
$$\xymatrix@R=20pt@C=6pt{
\prod_{i=1,n} \NEPSh{\tau_i} \ar[rd]_(.35){\prod_{i=1,n}\NEsem{\tau_i}} 
\ar@{.>}[r] &
\ar[d]^-{\prod_{i=1,n}\NSsem{\tau_i}} \prod_{i=1,n} \NSSemPSh{\tau_i}
\ar[r]^-{\mbox{\scriptsize$\mbox{\boldmath$s$}'\sembracket{\Gamma\vdash t:\tau}$}} & 
\NSSemPSh\tau \ar@{.>}[r] \ar[dd]_-{\NSsem\tau} & \NFPSh\tau 
\ar[ddl]^-{\NFsem\tau}
\\
& \prod_{i=1,n}
\cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\tau_i})
\ar[d]|-\cong
\\
& 
\cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\Gamma}) 
\ar[r]_-{\raisebox{-4mm}{\scriptsize
         $\mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}\circ\_\!\_$}}
& \cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket{\tau}) 
}$$
will commute ({\it cf.}~diagram~(\ref{Basic_Lemma_Diagram}) of the Basic Lemma
(Lemma~\ref{Basic_Lemma
)) 
and, hence, the evaluation of the horizontal top composite at the tuple
$\pair{\mathsf{var}_{\tau_i}(x_i)}_{i=1,n}$ of the variables in the
context~$\Gamma$ will yield a
normal term in $\NFPSh\tau(\Gamma)$ with the
same semantics as the given term~$t$~(compare the Extensional Normalisation
Lemma (Lemma~\ref{Extensional_Normalisation_Lemma
)
and see Corollary~\ref{Corollary_Correctness_Two} below).  
Moreover, as we will show below~(see
Corollary~\ref{Corollary_Correctness_Three}), the long $\beta\eta$-normal
forms associated to two $\beta\eta$-equal terms will be 
the same. 

\medskip
The abstract way to define the maps in~(\ref{uq_Maps}) ---which in the
literature on normalisation by evaluation are either referred to as
\Rem{unquote} and \Rem{quote} or as \Rem{reflect} and \Rem{reify}--- is by
defining maps 
$$
\NEobj\tau 
\longstackrightarrow{\unquotemap\tau}
\ext\mbox{\boldmath$s$}\sembracket\tau
\longstackrightarrow{\quotemap\tau}
\NFobj\tau 
\quad\mbox{in $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$}
$$
that project in $\cat S$ onto identities (see
Proposition~\ref{pi(u)=id=pi(q)} below).  
The definition of these maps is by induction on the structure of types relying
on Propositions~\ref{mu_Operations} and~\ref{nu_Operations} as follows:
\begin{enumerate}
\item
For a base type $\theta \in \mathrm{T}$, we define
$\unquotemap\theta = \mathrm{id}_{\NEobj\theta}$ and 
\mbox{$\quotemap\theta 
         = (\NEobj\theta\stackrightarrow\cong\NFobj\theta)$}.

\item
We let 
$\unquotemap\unittype = (\NEobj\unittype \rightarrow 1)$
and 
$\quotemap\unittype 
 = (1 
   \xymatrix@C=33pt{\ar[r]^-{(\mathsf{unit}_\unittype,\mathrm{id})}_-\cong&}
   \NFobj\unittype)$.

\item
For types $\tau,\tau'\in\TypeClosure\mathrm{T}$, we define 
$$
\unquotemap{\tau\producttype\tau'}:
  \NEobj{\tau\producttype\tau'} 
  \rightarrow
  \ext\mbox{\boldmath$s$}\sembracket{\tau}\times\ext\mbox{\boldmath$s$}\sembracket{\tau'}
$$
as the pairing of the maps
$$\begin{array}{ccc}
\NEobj{\tau\producttype\tau'}
\xymatrix@C=50pt{\ar[r]^-{(\mathsf{fst}^{(\tau')}_{\tau},\pi_1)}&}
\NEobj{\tau}
\xymatrix{\ar[r]^-{\unquotemap{\tau}}&}
\ext\mbox{\boldmath$s$}\sembracket{\tau}
& \mbox{ and } & 
\NEobj{\tau\producttype\tau'}
\xymatrix@C=50pt{\ar[r]^-{(\mathsf{snd}^{(\tau)}_{\tau'},\pi_2)}&}
\NEobj{\tau'}
\xymatrix{\ar[r]^-{\unquotemap{\tau'}}&}
\ext\mbox{\boldmath$s$}\sembracket{\tau'}
\quad,
\end{array}$$
and let 
$\quotemap{\tau\producttype\tau'}:
 \ext\mbox{\boldmath$s$}\sembracket{\tau}\times\ext\mbox{\boldmath$s$}\sembracket{\tau'}
 \rightarrow
 \NFobj{\tau\producttype\tau'}$
be the composite
$$
\ext\mbox{\boldmath$s$}\sembracket{\tau}\times\ext\mbox{\boldmath$s$}\sembracket{\tau'}
\xymatrix@C=30pt{\ar[r]^-{\quotemap{\tau}\times\quotemap{\tau'}}&}
\NFobj{\tau}\times\NFobj{\tau'}
\xymatrix@C=40pt{\ar[r]^-{(\mathsf{pair}_{\tau\producttype\tau'},\mathrm{id})}_-\cong&}
\NFobj{\tau\producttype\tau'}\ .
$$ 

\item
For types $\tau,\tau'\in\TypeClosure\mathrm{T}$, we define 
$$
\unquotemap{\tau\arrowtype\tau'}:
 \NEobj{\tau\arrowtype\tau'}
 \rightarrow
 \ext\mbox{\boldmath$s$}\sembracket{\tau'}^{\ext\mbox{\boldmath$s$}\sembracket\tau}
$$
as the exponential transpose of the map
$$
\NEobj{\tau\arrowtype\tau'}\times\ext\mbox{\boldmath$s$}\sembracket\tau
\longstackrightarrow{\mathrm{id}\times\quotemap\tau}
\NEobj{\tau\arrowtype\tau'}\times\NFobj\tau
\longlongstackrightarrow{(\mathsf{app}^{(\tau)}_{\tau'},\varepsilon)}
\NEobj{\tau'}
\longstackrightarrow{\unquotemap{\tau'}}
\ext\mbox{\boldmath$s$}\sembracket{\tau'}
\ , 
$$
and let 
$\quotemap{\tau\arrowtype\tau'}:
 \ext\mbox{\boldmath$s$}\sembracket{\tau'}^{\ext\mbox{\boldmath$s$}\sembracket\tau}
 \rightarrow
 \NFobj{\tau\arrowtype\tau'}$
be the composite
$$
\ext\mbox{\boldmath$s$}\sembracket{\tau'}^{\ext\mbox{\boldmath$s$}\sembracket\tau}
\xymatrix@C=35pt{\ar[r]^-{{\quotemap{\tau'}}^{\unquotemap\tau\mathrm{v}_\tau}}&}
{\NFobj{\tau'}}^{\Varobj\tau}
\xymatrix@C=55pt{\ar[r]^-{(\mathsf{abs}_{\tau\arrowtype\tau'},\mathrm{id})}_\cong&}
\NFobj{\tau\arrowtype\tau'}
$$
where $\mathrm{v}_\tau=(\mathsf{var}_\tau,\mathrm{id}):\Varobj\tau\rightarrow\NEobj\tau$.
\end{enumerate}

Proposition~\ref{pi(u)=id=pi(q)} below yields~(\ref{uq_Maps}) as a corollary.
\begin{proposition}\label{pi(u)=id=pi(q)}
For every type $\tau\in\TypeClosure\mathrm{T}$, we have the identities
$$
\pi(\unquotemap\tau) 
 \ = \ \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\tau$}}
 \ = \ \pi(\quotemap\tau)
$$ 
for $\pi$ the forgetful functor $\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$} \rightarrow \cat S$.
\end{proposition}
\begin{proof*}
The proof is by induction on the structure of types.
\begin{enumerate}
\item
For a base type $\theta \in \mathrm{T}$, 
$\pi(\unquotemap\theta) 
   = \pi(\quotemap\theta) 
   = \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\theta}$
by definition of $\unquotemap\theta$ and $\quotemap\theta$.

\item
$\pi(\unquotemap\unittype) 
   = \pi(\quotemap\unittype) 
   = \mathrm{id}_{1}$
by definition of $\unquotemap\unittype$ and $\quotemap\unittype$.

\item
For types $\tau,\tau'\in\TypeClosure\mathrm{T}$, 
$$\begin{array}{rcll}
\pi(\unquotemap{\tau\producttype\tau'})
& = & \pair{ \; \pi(\unquotemap\tau) \circ \pi_1 
             \, , 
             \, \pi(\unquotemap{\tau'}) \circ \pi_2
             \; }
    & \mbox{, by definition of $\unquotemap{\tau\producttype\tau'}$}
\\[1.5mm]
& = & \pair{ \, \pi_1 \, , \, \pi_2 \, } 
    & \mbox{, by induction}
\\[1.5mm]
& = &
\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau}
     \times
     \mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
\end{array}$$
and
$$\begin{array}{rcll}
\pi(\quotemap{\tau\producttype\tau'})
& = & \pi(\quotemap\tau) \times \pi(\quotemap{\tau'})
    & \mbox{, by definition of $\quotemap{\tau\producttype\tau'}$}
\\[1.5mm]
& = & \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau} 
           \times 
           \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
    & \mbox{, by induction}
\\[1.5mm]
& = & \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau 
           \times 
           \mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}} 
\quad.
\end{array}$$

\item
For types $\tau,\tau'\in\TypeClosure\mathrm{T}$, 
$$\begin{array}{rcll}
& & 
\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
\varepsilon \circ 
  (\pi(\unquotemap{\tau\arrowtype\tau'}) 
     \times \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau})
\\[1.5mm]
& = & \pi(\unquotemap{\tau'}) \circ \varepsilon \circ
        (\mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau
              \myArrow{\shortarrowlength}{}{}\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
              \times \pi(\quotemap\tau))
& \mbox{, by definition of $\unquotemap{\tau\arrowtype\tau'}$}
\\[1.5mm]
& = & \varepsilon
    & \mbox{, by induction}
\end{array}$$
and hence
$$\begin{array}{rcl}
\pi(\unquotemap{\tau\arrowtype\tau'})
& = & \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau}
           \myArrow{\shortarrowlength}{}{}
           \mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
\quad ;
\end{array}$$
further
\begin{center}
\hfill
$\begin{array}[b]{rcll}
\pi(\quotemap{\tau\arrowtype\tau'})
& = & (\pi(\unquotemap\tau) \circ \pi(\mathrm{v}_\tau)) 
        \myArrow{\shortarrowlength}{}{} (\pi(\quotemap{\tau'}))
    & \mbox{, by definition of $\quotemap{\tau\arrowtype\tau'}$}
\\[1.5mm]
& = & \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau} 
      \myArrow{\shortarrowlength}{}{} 
      \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
    & \mbox{, by induction and definition of $\mathrm{v}_\tau$}
\\[1.5mm]
& = & \mathrm{id}_{\mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket\tau
           \;\myArrow{\shortarrowlength}{}{}
           \mbox{\scriptsize$\mbox{\boldmath$s$}$}\sembracket{\tau'}}
\quad.
\end{array}$\hfill$\Box$
\end{center}
\end{enumerate}
\end{proof*}

\paragraph{Normalisation function.}
Every interpretation $\mbox{\boldmath$s$}: \mathrm{T} \rightarrow \cat S$ of base types
in a cartesian closed category, induces a \Rem{normalisation function}
$\nf\tau\mbox{\boldmath$s$}: \TermPSh\tau \rightarrow \NFPSh\tau$ in
$\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$
defined as the composite
$$
\TermPSh\tau 
\stackrightarrow{\extTermsem\tau}
\Hom{\ext\mbox{\boldmath$s$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy,\ext\mbox{\boldmath$s$}\sembracket\tau}
\longstackrightarrow{\arHom{\unquotemap{}\mathrm{v}{},\quotemap\tau}}
\Hom{\ext\yon(\xy(0,-1)\ar@{-}(2,-1)\endxy),\NFobj\tau}
\stackrightarrow\cong
\NFPSh\tau
$$
where $\extTermsem{}$ denotes the semantics of terms induced by the
interpretation $\ext\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\mbox{$\Set^{\F{}\comma\TypeClosure\BaseTypeSet}\comma\clone{\semfun\sembracket\fstarg}$}$ 
of~(\ref{mu_Interpretation}) and where
$$\begin{array}{lcl}
(\unquotemap{}\mathrm{v})_\Gamma
& = & 
\ext\yon(\Gamma) 
  \stackrightarrow{\mathrm{v}_\Gamma}
\NEobj{}\sembracket\Gamma
  \stackrightarrow{\unquotemap\Gamma}
\ext\mbox{\boldmath$s$}\sembracket\Gamma
\end{array}$$
for
$$\begin{array}{lcl}
\NEobj{}\sembracket\Gamma 
& = & 
\prod_{(x:\tau)\in\Gamma}\NEobj\tau
\quad ,
\\[1mm]
\mathrm{v}_\Gamma 
& = & 
\ext\yon(\Gamma) 
  \stackrightarrow\cong
\prod_{(x:\tau)\in\Gamma}\Varobj\tau
  \xymatrix@C=50pt{\ar[r]^-{\prod_{(x:\tau)\in\Gamma} \mathrm{v}_\tau}&}
\NEobj{}\sembracket\Gamma
\quad ,
\\[2mm]
\unquotemap\Gamma 
& = & 
\prod_{(x:\tau)\in\Gamma} \unquotemap\tau
\quad .
\end{array}$$
Explicitly, 
$$
\nf{\tau,\Gamma}\mbox{\boldmath$s$}(t)
\ = \
( \quotemap\tau\ 
    \ext\mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}\
      (\unquotemap{}\mathrm{v})_\Gamma
  
    (\mathrm{id}_\Gamma)
\enspace\in \NFPSh\tau(\Gamma) 
$$
for all terms $t\in\TermPSh\tau(\Gamma)$. 

\medskip
Having the same denotation, $\beta\eta$-equal terms are identified
by the normalisation function.
\begin{corollary}\label{Corollary_Correctness_Three}
Let $\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$ be an interpretation of base
types in a cartesian closed category.  
For every pair of terms $t,t'$ in $\TermPSh\tau(\Gamma)$, if $t =_{\beta\eta} t'$
then $\nf{\tau,\Gamma}\mbox{\boldmath$s$}(t) = \nf{\tau,\Gamma}\mbox{\boldmath$s$}(t')$ in
$\NFPSh\tau(\Gamma)$.
\end{corollary}
Further, as a consequence of Proposition~\ref{pi(u)=id=pi(q)}
(see also~(\ref{uq_Maps})), we have that a term and its associated normal form
have the same semantics.
\begin{corollary}\label{Corollary_Correctness_Two}
For every interpretation 
$\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$
of base types in a cartesian closed category, the diagram
$$\xymatrix{
\TermPSh\tau \ar[dr]_-{\Termsem\tau} 
\ar[rr]^-{\mbox{\scriptsize$\nf\tau\mbox{\boldmath$s$}$}} && 
\NFPSh\tau \ar[ld]^-{\NFsem\tau}\\
& \cat S(\mbox{\boldmath$s$}\sembracket\_\!\_,\mbox{\boldmath$s$}\sembracket\tau)
}$$
commutes for all types $\tau\in\TypeClosure\mathrm{T}$.   
\end{corollary}

Considering the universal interpretation
$\mbox{\boldmath$f$}: \mathrm{T} \rightarrow \mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ of the set of
base types $\mathrm{T}$ into the free cartesian closed category
$\mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ over them, by
Corollary~\ref{Corollary_Correctness_Two}, we have that   
\begin{equation} \label{t_betaetaequal_f-nf(t)}
t =_{\beta\eta} \nf{\tau,\Gamma}\mbox{\boldmath$f$}(t) 
\end{equation}
and hence, by Corollary~\ref{Corollary_Correctness_Three}, that 
\[
\nf{\tau,\Gamma}\mbox{\boldmath$s$}(t) 
= 
\nf{\tau,\Gamma}\mbox{\boldmath$s$}(\nf{\tau,\Gamma}\mbox{\boldmath$f$}(t))
\]
for all terms $t\in\TermPSh\tau(\Gamma)$.  
Thus, the normalisation function $\nf\tau\mbox{\boldmath$f$}$ is idempotent and
therefore fixes some normal terms.  
In fact, as we will see below (see~(\ref{NF_eqn}) in Theorem~\ref{THEOREM}),
all normalisation functions $\nf\tau\mbox{\boldmath$s$}$ fix all normal terms:  that is,
\begin{equation}\label{nf_Fixes_Normal_Forms}
\mbox{for all $N \in \NFPSh\tau(\Gamma)$, 
  $\nf{\tau,\Gamma}\mbox{\boldmath$s$}(N) = N$\quad.}
\end{equation}
This fixed-point property is important: from it and
Corollary~\ref{Corollary_Correctness_Three} it follows that 
\begin{itemize}
\item
  for all terms $t\in\TermPSh\tau(\Gamma)$ and normal terms
  \mbox{$N\in\NFPSh\tau(\Gamma)$}, if $t =_{\beta\eta} N$ then
  $\nf{\tau,\Gamma}\mbox{\boldmath$s$}(t) = N$, and 

\item 
  for every pair of normal terms $N,N' \in \NFPSh\tau(\Gamma)$, if 
  $N =_{\beta\eta} N'$ then $N = N'$;
\end{itemize}
so that, further using Corollary~\ref{Corollary_Correctness_Two} in the
form~(\ref{t_betaetaequal_f-nf(t)}), we have that 
\begin{itemize}
\item
  for all terms \mbox{$t\in\TermPSh\tau(\Gamma)$}, 
  $\nf{\tau,\Gamma}\mbox{\boldmath$s$}(t) = \nf{\tau,\Gamma}\mbox{\boldmath$f$}(t)$.
\end{itemize}
Thus, the fixed-point property~(\ref{nf_Fixes_Normal_Forms}) allows one to
conclude that: 
\begin{quote}
  all interpretations induce the same normalisation function
  $\simplenf\tau: \TermPSh\tau \rightarrow \NFPSh\tau$ 
such that, for every term
$t\in\TermPSh\tau(\Gamma)$, one has that
$\simplenf{\tau,\Gamma}(t)\in\NFPSh\tau(\Gamma)$ is the unique normal term
$\beta\eta$-equal to $t$.
\end{quote}

\medskip
We now
establish~(\ref{nf_Fixes_Normal_Forms}).  
The appropriate induction hypothesis to proceed by induction on the structure
of neutral and normal terms is stated in the theorem below.
\begin{theorem} \label{THEOREM}
For every interpretation 
$\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$
of base types in a cartesian closed category, the diagrams
\begin{equation}\label{NE_eqn}
\begin{array}{c}\xymatrix@C=-5pt{
\NEPSh\tau \ar[drr]_-{\extNEsem\tau} 
& \cong \Hom{\ext\yon(\_\!\_),\NEobj\tau}
\ar[rr]^-{\arHom{\mathrm{id},\unquotemap\tau}} 
&& 
\Hom{\ext\yon(\_\!\_),\ext\mbox{\boldmath$s$}\sembracket\tau}
\\
& & \Hom{\ext\mbox{\boldmath$s$}\sembracket{\_\!\_},\ext\mbox{\boldmath$s$}\sembracket\tau}
\ar[ru]_-{\arHom{\unquotemap{}\mathrm{v}{},\mathrm{id}}} & 
}\end{array}
\end{equation}
and
\begin{equation}\label{NF_eqn}
\begin{array}{c}\xymatrix{
\NFPSh\tau \ar[rr]|-\cong \ar[dr]_{\extNFsem\tau} & & 
\Hom{\ext\yon(\_\!\_),\NFobj\tau} \\
& \Hom{\ext\mbox{\boldmath$s$}\sembracket\_\!\_,\ext\mbox{\boldmath$s$}\sembracket\tau} 
\ar[ru]_-{\arHom{\unquotemap{}\mathrm{v}{},\quotemap\tau}}
}\end{array}
\end{equation}
commute for all types $\tau \in \TypeClosure\mathrm{T}$.
\end{theorem}
\begin{proof}
The proof uses the induction principle associated to the initial 
$\pair{\Sigma_1,\Sigma_2}$-algebra $(\NEPSh{},\NFPSh{})$ 
(see~(\ref{Induction_Principle})) by considering the
equalisers 
\begin{center}
$\SubNEPSh\tau \stackrightmono{\SubNEmap\tau} \NEPSh\tau$
\ and \
$\SubNFPSh\tau \stackrightmono{\SubNFmap\tau} \NFPSh\tau$
\end{center}
of~(\ref{NE_eqn}) and~(\ref{NF_eqn}) respectively, and showing that the
family 
$$
(\SubNEmap\tau,\SubNFmap\tau):
  (\SubNEPSh\tau,\SubNFPSh\tau) \rightmono (\NEPSh\tau,\NFPSh\tau)
\qquad(\tau\in\TypeClosure\mathrm{T})
$$ 
is a sub~$\pair{\Sigma_1,\Sigma_2}$-algebra, from which it follows that
$\SubNEmap\tau$ and $\SubNFmap\tau$ are isomorphisms and hence
that~(\ref{NE_eqn}) and~(\ref{NF_eqn}) commute.  The details are spelled
out in Appendix~\ref{PROOF}.  
\end{proof}

\begin{remark}
In elementary terms, the above categorical proof amounts to establishing the
identities  
$$
\ext\mbox{\boldmath$s$}\sembracket{\Gamma\vdash M:\tau}\ 
  (\unquotemap{}\mathrm{v})_\Gamma
\ = \
\unquotemap\tau\ (M[\xy(0,-1)\ar@{-}(2,-1)\endxy],\mbox{\boldmath$s$}\sembracket{\Gamma\vdash M:\tau})
$$
and 
$$
\quotemap\tau\
  \ext\mbox{\boldmath$s$}\sembracket{\Gamma\vdash N:\tau}\
    (\unquotemap{}\mathrm{v})_\Gamma
\ = \
(N[\xy(0,-1)\ar@{-}(2,-1)\endxy],\mbox{\boldmath$s$}\sembracket{\Gamma\vdash N:\tau})
$$
for $M\in\NEPSh\tau(\Gamma)$ and $N\in\NFPSh\tau(\Gamma)$, by simultaneous 
induction on the derivation of neutral and normal
terms~({\it cf.}~\cite{Reynolds}).  
\end{remark}

\medskip
The commutativity of diagram~(\ref{NF_eqn}) amounts to
property~(\ref{nf_Fixes_Normal_Forms}) and hence, as explained above, all
normalisation functions coincide. 
\begin{corollary} \label{Corollary_nfCoincidence}
For every interpretation 
$\mbox{\boldmath$s$}:\mathrm{T}\rightarrow\cat S$
of base types in a cartesian closed category and for the universal
interpretation 
$\mbox{\boldmath$f$}: \mathrm{T} \rightarrow \mathcal{F}_{\mathrm{ccc}}[\mathrm{T}]$ of base
types into the free cartesian closed category over them, the identity
$$\begin{array}{rclll}
\nf\tau\mbox{\boldmath$s$} & = & \nf\tau\mbox{\boldmath$f$} 
& : \TermPSh\tau \rightarrow \NFPSh\tau
&\mbox{ in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$}
\end{array}$$
holds.
\end{corollary}

Summarising, we have obtained normalisation functions
$$
\simplenf{\tau,\Gamma}: 
  \TermPSh\tau(\Gamma) \rightarrow \NFPSh\tau(\Gamma)
\quad(\tau\in\TypeClosure\mathrm{T}, 
      \Gamma\in\obj{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}) 
$$ satisfying the correctness properties below.
\begin{itemize}
\item
For all context renamings~$\rho: \Gamma \rightarrow \Gamma'$
in $\F{}\!\downarrow\!\TypeClosure\mathrm{T}$, 
$$
(\simplenf{\tau,\Gamma}\ t)[\rho] = \simplenf{\tau,\Gamma'}(t[\rho])
$$
for every term $t \in \TermPSh\tau(\Gamma)$.

\item
For all normal terms $N\in\NFPSh\tau(\Gamma)$, 
$$\simplenf{\tau,\Gamma}(N) = N\quad.$$

\item
For all terms $t\in\TermPSh\tau(\Gamma)$, 
$$\simplenf{\tau,\Gamma}(t)=_{\beta\eta} t\quad.$$

\item
For all terms $t,t'\in\TermPSh\tau(\Gamma)$, 
\begin{center}
if $t=_{\beta\eta} t'$ then 
$\simplenf{\tau,\Gamma}(t) = \simplenf{\tau,\Gamma}(t')$\quad.
\end{center}
\end{itemize}

\paragraph{Normalisation algorithm.}
The simplest description of the normalisation function from which to extract
an algorithm is the one induced by the trivial interpretation 
$\mbox{\boldmath$t$}$
of base types in the trivial cartesian closed category as, in this case, the
glueing category
$\mathbf{Set}^{\F{}
 \!\downarrow\!\TypeClosure\mathrm{T}}\!\downarrow\!\clone{\mbox{\boldmath$t$}\sembracket\xy(0,-1)\ar@{-}(2,-1)\endxy}$ 
is simply (isomorphic to) the presheaf category
$\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$ (recall
Example~\ref{Trivial_Glueing}).  In fact, previous categorical analysis of
normalisation by evaluation have centred around this
interpretation~\cite{AHS,Reynolds}.

Explicitly, the unquote and quote maps
\begin{equation} \label{UnquoteQuoteMaps}
\NEPSh\tau \longstackrightarrow{\unquotemap\tau} \mbox{\boldmath$s$}\sembracket\tau
\longstackrightarrow{\quotemap\tau} 
\NFPSh\tau 
\quad(\tau\in\TypeClosure\mathrm{T})
\end{equation}
in $\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$, with respect to the 
interpretation of base types 
$\mbox{\boldmath$s$}: 
     \theta \mapsto \NEPSh\theta$,  
are (in the internal language of
$\mathbf{Set}^{\F{}\!\downarrow\!\TypeClosure\mathrm{T}}$) as follows:
\begin{description}
\item[]1.%
\begin{tabular}[t]{l}
$\unquotemap\theta(M) = M$
\\[2mm]
$\quotemap\theta(M) = \mathsf{norm}(M)$, where 
$\mathsf{norm}:
\NEPSh\theta\stackrightarrow\cong\NFPSh\theta$~(see~(\ref{normISO}))
\end{tabular}

\item[]2.%
\begin{tabular}[t]{l}
$\unquotemap\unittype(M) = (\,)$
\\[2mm]
$\quotemap\unittype(\,) = \mathsf{unit}_\unittype(\,)$
\end{tabular}

\item[]3.%
\begin{tabular}[t]{l}
$\unquotemap{\tau\producttype\tau'}(M)
 = (\ \unquotemap\tau(\mathsf{fst}^{(\tau')}_\tau\,M)\ ,\ 
     \unquotemap{\tau'}(\mathsf{snd}^{(\tau)}_{\tau'}\,M)\ )$
\\[2mm]
$\quotemap{\tau\producttype\tau'}(x,x')
 = \mathsf{pair}_{\tau\producttype\tau'}
     (\ \quotemap\tau(x)\ ,\
        \quotemap{\tau'}(x')\ )$
\end{tabular}

\item[]4.%
\begin{tabular}[t]{l}
$\unquotemap{\tau\arrowtype\tau'}(M)
 = \semlambdaop 
     {x^{\mbox{\scriptsize$\mbox{\boldmath$s$}\sembracket\tau$}}}
     {\unquotemap{\tau'}(\mathsf{app}^{(\tau)}_{\tau'}(M,\quotemap\tau\,x))}$
\\[2mm]
$\quotemap{\tau\arrowtype\tau'}(f)
 = \mathsf{abs}_{\tau\arrowtype\tau'}
     ( \semlambdaop
         {v^{\VarPSh\tau}}
         {\quotemap{\tau'}(f(\unquotemap\tau(\mathsf{var}_\tau\,v)))}
       )$
\end{tabular}
\end{description}
and the normalisation function 
is given by
\begin{equation} \label{NormalisationFunction}
\simplenf{\tau,\Gamma}(t)
=
\quotemap\tau
  ( \mbox{\boldmath$s$}\sembracket{\Gamma\vdash t:\tau}\,
      \pair{\unquotemap{\tau_i}(\mathsf{var}_{\tau_i}\,x_i)}_{i=1,n}
    )
\end{equation}
for all terms $t\in\TermPSh\tau(\Gamma)$ where 
$\Gamma=\pair{x_i:\tau_i}_{i=1,n}$. 

These functions can be directly implemented, for instance, in metalanguages
supporting abstract syntax with variable binding, like HOAS~\cite{HOAS},
\texttt{Fresh O'Caml}~\cite{FreshOCAML}, the Scope-and-Type Safe Universe of
Syntaxes with Binding~\cite{AllaisEtAl}, and the SOAS
Framework~\cite{FioreSzamozvancev}.  
Indeed, for concreteness, we here synthesise an elementary implementation in
Agda considered as a dependently-typed functional programming
language\footnote{The code is available from
  \url{www.cl.cam.ac.uk/~mpf23/Notes/Notes.html}.}.

\medskip

\begin{code}[hide]%
\>[0]\<%
\\
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Primitive}\<%
\\
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.Unit}\<%
\\
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.Nat}\<%
\\
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.Sigma}\<%
\\
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaKeyword{import}\AgdaSpace{}%
\AgdaModule{Agda.Builtin.Equality}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaComment{-- composition}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}∘\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}%
\>[11I]\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\<%
\\
\>[.][@{}l@{}]\<[11I]%
\>[6]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{\}(}\AgdaBound{y}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaBound{y}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{C}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
\AgdaBound{g}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{g}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaComment{-- binary product}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}×\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}%
\AgdaBound{n}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaBound{A}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaRecord{Σ}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{π₁}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\<%
\\
\>[0]\AgdaFunction{π₁}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaField{fst}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{π₂}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{B}\<%
\\
\>[0]\AgdaFunction{π₂}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaField{snd}\<%
\end{code}

\mysubparagraph{Syntax.}
We consider simple types over a countably infinite set of base
types~(see~(\ref{SimpleTypes})): 
\begin{code}%
\>[0]\AgdaComment{-- base types}\<%
\\
\>[0]\AgdaFunction{T}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaFunction{T}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{Nat}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaComment{-- simple types}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{T}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\\
\>[2]\AgdaInductiveConstructor{υ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\\
\>[2]\AgdaOperator{\AgdaInductiveConstructor{\AgdaUnderscore{}⋆\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\\
\>[2]\AgdaOperator{\AgdaInductiveConstructor{\AgdaUnderscore{}⇒\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\end{code}

Typing contexts~(Definition~\ref{ContextCat}) are inductively generated by
context extension from an empty context:
\begin{code}%
\>[0]\AgdaComment{-- typing contexts}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaSymbol{→}%
\>[17]\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{·}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\<%
\\
\>[2]\AgdaOperator{\AgdaInductiveConstructor{\AgdaUnderscore{}::\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\<%
\end{code}
We then have a family of variable indices~(recall~(\ref{VPSh})) given as
follows:
\begin{code}%
\>[0]\AgdaComment{-- variable indices}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{•}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{↑}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{𝓧}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓧}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSymbol{)}\<%
\end{code}
for which context renamings~(Definition~\ref{ContextCat}) are considered:
\begin{code}%
\>[0]\AgdaComment{-- context renamings}\<%
\\
\>[0]\AgdaFunction{𝔽↓₀}\AgdaSpace{}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{𝓣}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓣}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaBound{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaBound{𝓣}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\end{code}

The abstract syntax of simply typed terms~(see~(\ref{LamInitialAlg})) is
implemented by the inductive family below:
\begin{code}%
\>[0]\AgdaComment{-- simply typed terms}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{var}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{unit}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaInductiveConstructor{υ}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{pair}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{fst₀}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}%
\>[20]\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{snd₀}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{abs}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{app}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\end{code}
Analogously, the abstract syntax of neutral and normal
terms~(see~(\ref{NEandNFPShsOne}) and~(\ref{NEandNFPShsTwo})) is implemented
by the following mutually-inductive families:
\begin{code}%
\>[0]\AgdaComment{-- neutral and normal terms}\<%
\\
\>[0]\AgdaKeyword{mutual}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{fstₘ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{sndₘ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{appₘ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[0]\<%
\\
\>[2]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaInductiveConstructor{varₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{i}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{T}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{fstₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{i}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{T}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{sndₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{i}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{T}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{appₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{i}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaFunction{T}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{unitₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaInductiveConstructor{υ}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{pairₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[4]\AgdaInductiveConstructor{absₙ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\end{code}
Their presheaf actions~(recall~(\ref{Neutral_Renaming_Invariance})
and~(\ref{Normal_Renaming_Invariance})) will be needed:
\begin{code}%
\>[0]\AgdaComment{-- neutral and normal presheaf actions}\<%
\\
\>[0]\AgdaKeyword{mutual}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₘ}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{fstₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{fstₘ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{sndₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{sndₘ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{appₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{appₘ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[2]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₙ}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaInductiveConstructor{varₙ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{varₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{fstₙ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{fstₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{sndₙ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{sndₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{appₙ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{appₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{unitₙ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{unitₙ}\<%
\\
\>[2]\AgdaInductiveConstructor{pairₙ}\AgdaSpace{}%
\AgdaBound{n₁}\AgdaSpace{}%
\AgdaBound{n₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{pairₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{n₁}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{n₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaInductiveConstructor{absₙ}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{=}%
\>[804I]\AgdaInductiveConstructor{absₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaFunction{lift}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₙ}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[.][@{}l@{}]\<[804I]%
\>[18]\AgdaKeyword{where}\<%
\\
\>[18][@{}l@{\AgdaIndent{0}}]%
\>[20]\AgdaFunction{lift}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[20]\AgdaFunction{lift}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\<%
\\
\>[20]\AgdaFunction{lift}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{↑}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{↑}\AgdaSymbol{(}\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\<%
\end{code}
Note the treatment of abstraction guaranteeing fresh bindings.

\medskip
\mysubparagraph{Semantics.}
We implement the presheaf semantics of types induced by the interpretation of
base types as neutral terms~(see~(\ref{mu_Interpretation})).  Note that for
higher types the implementation glosses over the naturality condition required
of presheaf exponentials~(see~(\ref{PShExponentialNaturality})).
\begin{code}%
\>[0]\AgdaComment{-- type semantics}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{υ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaRecord{⊤}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{β}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₘ}}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{υ}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{x₁}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x₂}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{x₁}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{ρ′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{ρ′}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSymbol{)}\<%
\end{code}

The semantic interpretation of
terms~(see~(\ref{StandardSemanticInterpretation})) follows:
\begin{code}%
\>[0]\AgdaComment{-- term semantics}\<%
\\
\>[0]\AgdaFunction{Π}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\<%
\\
\>[0]\AgdaFunction{Π}\AgdaSpace{}%
\AgdaInductiveConstructor{·}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaRecord{⊤}\<%
\\
\>[0]\AgdaFunction{Π}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{P}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaBound{P}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{×}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{P}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧₀}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{var}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}%
\>[1042I]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≪}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≫}}\<%
\\
\>[.][@{}l@{}]\<[1042I]%
\>[13]\AgdaKeyword{where}\<%
\\
\>[13][@{}l@{\AgdaIndent{0}}]%
\>[15]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}≪\AgdaUnderscore{}≫}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\<%
\\
\>[15]\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≪}}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≫}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{π₂}\AgdaSpace{}%
\AgdaBound{ε}\<%
\\
\>[15]\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≪}}\AgdaSpace{}%
\AgdaInductiveConstructor{↑}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≫}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{π₁}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≪}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{≫}}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{unit}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{pair}\AgdaSpace{}%
\AgdaBound{t₁}\AgdaSpace{}%
\AgdaBound{t₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t₁}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{fst₀}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{π₁}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{snd₀}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{π₂}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{abs}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaBound{x}%
\>[1138I]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₚ}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[.][@{}l@{}]\<[1138I]%
\>[17]\AgdaKeyword{where}\<%
\\
\>[17][@{}l@{\AgdaIndent{0}}]%
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₚ}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₚ}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{·}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ₚ}}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₚ}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaInductiveConstructor{app}\AgdaSpace{}%
\AgdaBound{t₁}\AgdaSpace{}%
\AgdaBound{t₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t₁}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t₂}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaBound{ε}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\end{code}

\medskip
\mysubparagraph{Normalisation by evaluation.}
The unquote and quote functions~(see~(\ref{UnquoteQuoteMaps})) are
implemented:
\begin{code}%
\>[0]\AgdaComment{-- unquote and quote}\<%
\\
\>[0]\AgdaKeyword{mutual}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓜}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{m}\<%
\\
\>[2]\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{υ}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[2]\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{fstₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{sndₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[2]\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaInductiveConstructor{appₘ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ₘ}}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{q}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{varₙ}\AgdaSpace{}%
\AgdaBound{x}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{fstₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{fstₙ}\AgdaSpace{}%
\AgdaBound{m}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{sndₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{sndₙ}\AgdaSpace{}%
\AgdaBound{m}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{appₘ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{appₙ}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{υ}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{unitₙ}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x₁}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x₂}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{pairₙ}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{q}\AgdaSpace{}%
\AgdaBound{x₁}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{q}\AgdaSpace{}%
\AgdaBound{x₂}\AgdaSymbol{)}\<%
\\
\>[2]\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{absₙ}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{q}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaInductiveConstructor{↑}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\end{code}
\begin{remark}
A technical point to note is that the implementation of
\AgdaFunction{q}\AgdaSpace{}\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}\AgdaBound{f}\AgdaSpace{}
arises from the functorial action of presheaf
exponentiation~(in particular with respect to the evaluation
map~(\ref{RepresentableExponentialEvaluationMap})),
which in this case instatiates to the equivalent expression
\mbox{%
\AgdaInductiveConstructor{absₙ}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{q}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}\AgdaFunction{[}\AgdaSpace{}%
\AgdaInductiveConstructor{↑}\AgdaSpace{}\AgdaFunction{]}\AgdaSpace{}%
\AgdaSymbol{(λ}\AgdaSpace{}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}\AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{u}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{varₘ}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSymbol{))}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}\AgdaSymbol{)}%
}.
\end{remark}

Finally, the normalisation function~(see~(\ref{NormalisationFunction})) is:
\begin{code}%
\>[0]\AgdaComment{-- nbe}\<%
\\
\>[0]\AgdaFunction{nf}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{𝓝}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[0]\AgdaFunction{nf}\AgdaSpace{}%
\AgdaBound{t}%
\>[1369I]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{q}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧₀}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{Π₀}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{u}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}%
\AgdaInductiveConstructor{varₘ}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaFunction{xs}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[.][@{}l@{}]\<[1369I]%
\>[5]\AgdaKeyword{where}\<%
\\
\>[5][@{}l@{\AgdaIndent{0}}]%
\>[7]\AgdaFunction{Π₀}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{α}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{α}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaBound{Δ}\<%
\\
\>[7]\AgdaFunction{Π₀}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{·}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[7]\AgdaFunction{Π₀}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{xs}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{Π₀}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaBound{xs}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[0]\<%
\\
\>[7]\AgdaFunction{xs}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[7]\AgdaFunction{xs}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{·}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[7]\AgdaFunction{xs}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}%
\>[1454I]\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}%
\>[24]\AgdaFunction{xs}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaInductiveConstructor{↑}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ᵥ}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\>[1454I][@{}l@{\AgdaIndent{0}}]%
\>[17]\AgdaKeyword{where}\<%
\\
\>[17][@{}l@{\AgdaIndent{0}}]%
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ᵥ}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝔽↓}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{𝔽↓₀}\AgdaSpace{}%
\AgdaDatatype{𝓣}\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{Δ}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{Γ}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaFunction{Π}\AgdaSpace{}%
\AgdaBound{Ξ}\AgdaSpace{}%
\AgdaDatatype{V}\AgdaSpace{}%
\AgdaBound{Γ}\<%
\\
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ᵥ}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaInductiveConstructor{·}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}}\<%
\\
\>[19]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}[\AgdaUnderscore{}]ᵥ}}\AgdaSpace{}%
\AgdaSymbol{\{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{::}}\AgdaSpace{}%
\AgdaSymbol{\AgdaUnderscore{}\}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{xs}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaBound{xs}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]ᵥ}}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}%
\AgdaBound{ρ}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\end{code}

\begin{code}[hide]%
\>[0]\AgdaComment{-- examples}\<%
\\
\>[0]\AgdaFunction{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\\
\>[0]\AgdaFunction{A}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaInductiveConstructor{zero}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaInductiveConstructor{zero}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaInductiveConstructor{υ}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{s}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{A}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{A}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaInductiveConstructor{·}\<%
\\
\>[0]\AgdaFunction{s}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{abs}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{var}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓣}\<%
\\
\>[0]\AgdaFunction{B}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaInductiveConstructor{zero}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⋆}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaInductiveConstructor{zero}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaInductiveConstructor{θ}\AgdaSpace{}%
\AgdaInductiveConstructor{zero}\AgdaSpace{}%
\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{t1}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaInductiveConstructor{·}\<%
\\
\>[0]\AgdaFunction{t1}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{abs}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{var}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSymbol{)}\<%
\\
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{t2}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{𝓛}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{B}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{⇒}}\AgdaSpace{}%
\AgdaFunction{B}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{)}\AgdaSpace{}%
\AgdaInductiveConstructor{·}\<%
\\
\>[0]\AgdaFunction{t2}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{abs}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{var}\AgdaSpace{}%
\AgdaInductiveConstructor{•}\AgdaSymbol{)}\<%
\end{code}


\section*{\Large Conclusion}

We have given a new categorical view of normalisation by evaluation for typed
lambda calculus, both for extensional
and intensional
normalisation problems.

\medskip
Extensional normalisation was obtained from a basic lemma unifying
definability and normalisation.  Our analysis has the important methodological
consequence of providing guidance when looking for normal forms.  Indeed, a
basic lemma based on the definability result of Fiore and
Simpson~\cite{FioreSimpson} via Grothendiek logical relations led to syntactic
counterparts of the normal forms of Altenkirch, Dybjer, Hofmann, and
Scott~\cite{ADHS} and has been applied to establish extensional normalisation
for the typed lambda calculus with empty and sum
types~\cite{FioreDiCosmoBalat}.  Along this line of research, one can study
normalisation for other calculi for which definability results based on
Kripke relations have been obtained ---as classical linear
logic~\cite{Streicher}, for instance. 

\medskip
The approach to normalisation by evaluation presented in the paper is novel,
chiefly, in the following respects.  
\begin{itemize}
  \item
    The refinement from the extensional setting to the intensional one
    leading to the formalisation of normalisation by evaluation via
    categorical glueing.

  \item
    The use of an algebraic framework to structure both the development and
    proofs culminating in the definition of the normalisation function within
    a simply typed metatheory. 

  \item
    The synthesis of a normalisation-by-evaluation program in a
    dependently-typed functional programming language.
\end{itemize}

The obtained abstract normalisation algorithm synthesises various concrete
implementations.  Its specialisation to particular implementations of abstract
syntax directly yields normalisation programs for concrete syntactic 
representations.
In particular, we have provided a normalisation-by-evaluation program for the
type-and-scope safe, intrinsically-typed encoding of typed lambda
terms~\cite{AltenkirchReus,BentonEtAl,AllaisEtAl}.
How the abstract setting is related to representations of binding based on
generating globally unique identifiers, say as in~\cite{Filinski01}, needs to
be investigated.  

The role of categorical glueing in our analysis is reminiscent of
realisability.  It would be interesting to understand whether there are
connections to the modified realisability approach of Berger~\cite{Berger}. 

\paragraph{Acknowledgements.}
The basis for this work, which was motivated by a question of Roberto
Di~Cosmo, was done during a visit to PPS, Universit\'e Paris~7 in July~2001
organised by Paul-Andr\'e Melli\`es and supported by the CNRS.
Discussions with Pierre-Louis Curien and Vincent Danos are gratefully
acknowledged.  

