100.00015pt\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}t:=\mathsf{apd}\,(t[\mathsf{q}])[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\cong}{\mathit{\oldDelta}}]$

Finally we define:

${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}:=k_{\mathsf{K}\,{\mathit{\oldGamma}}}[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\cong}{\mathit{\oldGamma}}]\qquad\qquad{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{\mathit{\oldGamma}}:={\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\cong}}^{-1}{\mathit{\oldGamma}}\circ(\epsilon,\mathsf{ap}\,\mathsf{p}[\mathsf{id},\mathsf{tt}])\qquad\qquad{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{\mathit{\oldGamma}}:=\mathsf{q}\circ(\mathsf{p},\mathsf{S}_{\mathsf{K}\,{\mathit{\oldGamma}}})\circ(\epsilon,\mathsf{id})$

and
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}\,\sigma\,t_{k}\,t:=\mathsf{mk}{\forall}{\Pi}\,(\mathsf{q}[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\cong}\,{\mathit{\oldGamma}}\circ\sigma])\,t_{k}\,t$.
Once again,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{unspan}}}$
is straightforward, and the equations come from the corresponding equations in
the local theory.

###  4.3. Roundtrips

The 9 operations of the local syntax coincide with the same ones after
globalising and localising them. The proofs essentially rely on manipulations
on substitutions and naturality properties.

In addition, the 9 operations of the global syntax coincide with the same ones
after localising and globalising them. To prove that the
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\prime}$
that we define by induction is the same as the initial
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$,
we do a mutual induction proving that
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\cong}{\mathit{\oldGamma}}=(\epsilon,\mathsf{id})$.
The proof for substitutions is also an induction, the others rely on
naturality.

###  4.4. Isomorphism

Subsection 4.1 says that the global syntax
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$
is also a model of the local theory. Thus we obtain a map $\alpha$ from the
local syntax to this global model. Note that it is identity on the core
calculus (Figure 2 or Definition 3.1). Similarly, Subsection 4.2 decorates the
local syntax with a model of the global syntax providing a morphism $\beta$
from
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$
to the local syntax. By induction by $\mathsf{Syn}$ and
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$,
we prove the compositions of $\alpha$ and $\beta$ are identities. The only
nontrivial cases of this induction are handled in Subsection 4.3. Thus we
obtain e.g. that for all ${\mathit{\oldGamma}}:\mathsf{Con}_{\mathsf{Syn}}$,
$\beta\,(\alpha\,{\mathit{\oldGamma}})={\mathit{\oldGamma}}$, and so on.

##  5\. Gluing for the global theory

In this section we extend the gluing proof of (Kaposi et al., 2019a) to the
global theory. We first define the notion of weak morphism which also has to
respect
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$,
then we define the gluing model. Finally we show how to make use of gluing by
defining a global section functor from the syntax of the global theory
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$
to the presheaf model $\mathsf{PSh}(\square)$ (Problem 3.7), and applying
gluing to this, which shows that our theory enjoys canonicity.

###  5.1. Weak Morphism of Models Respecting
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$

A weak morphism is a functor which has an action on types and terms and
preserves instantiation of substitution strictly and we require that the empty
context and context extension are preserved up to isomorphism. Furthermore, we
require that the functor preserves
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}$
and
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$
strictly.

###### Definition 5.1 (Weak morphisms of models of the global theory).

Given two models of the global theory $\mathcal{C}$ and $\mathcal{D}$, a weak
morphism $F$ from $\mathcal{C}$ to $\mathcal{D}$ contains the following
functions and satisfies the following equations. We usually omit the
subscripts saying which model is meant because it is clear from the context,
and we also overload the names for the four maps in $F$.

Maps Preservation of core structure Preservation of
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}},{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}},{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}},{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$
$\displaystyle
F:\mathsf{Con}_{\mathcal{C}}\rightarrow\mathsf{Con}_{\mathcal{D}}$
$\displaystyle F\,(\sigma\circ\rho)=F\,\sigma\circ F\,\rho$ $\displaystyle
F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\,{\mathit{\oldGamma}})=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,{\mathit{\oldGamma}})$
$\displaystyle
F:\mathsf{Sub}\,{\mathit{\oldDelta}}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Sub}\,(F\,{\mathit{\oldDelta}})\,(F\,{\mathit{\oldGamma}})\hskip
20.00003pt$ $\displaystyle F\,\mathsf{id}=\mathsf{id}$ $\displaystyle
F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\,\sigma)=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,\sigma)$
$\displaystyle
F:\mathsf{Ty}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Ty}\,(F\,{\mathit{\oldGamma}})$
$\displaystyle F_{\epsilon}^{-1}:\mathsf{Sub}\,\diamond\,(F\,\diamond)$
$\displaystyle
F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\,A)=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,A)$
$\displaystyle
F:\mathsf{Tm}\,{\mathit{\oldGamma}}\,A\rightarrow\mathsf{Tm}\,(F\,{\mathit{\oldGamma}})\,(F\,A)$
$\displaystyle F_{\epsilon}^{-1}\circ\epsilon=\mathsf{id}_{F\,\diamond}$
$\displaystyle
F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\,t)=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,t)$
$\displaystyle F\,(A[\sigma])=F\,A[F\,\sigma]$ $\displaystyle
F\,{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,{\mathit{\oldGamma}}}$
$\displaystyle F\,(t[\sigma])=F\,t[F\,\sigma]$ $\displaystyle
F\,{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{\mathit{\oldGamma}}={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{F\,{\mathit{\oldGamma}}}$
$\displaystyle
F_{\mathop{\triangleright}}^{-1}:\mathsf{Sub}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}F\,A)\,(F\,({\mathit{\oldGamma}}\mathop{\triangleright}A))\hskip
20.00003pt$ $\displaystyle
F\,{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{\mathit{\oldGamma}}={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}}$
$\displaystyle
F_{\mathop{\triangleright}}^{-1}\circ(F\,\mathsf{p},F\,\mathsf{q})=\mathsf{id}$
$\displaystyle(F\,\mathsf{p},F\,\mathsf{q})\circ
F_{\mathop{\triangleright}}^{-1}=\mathsf{id}$

For any such $F$ we can define comparison maps expressing that $\mathsf{K}$,
$\top$, $\Sigma$, $\mathsf{Eq}$ are preserved automatically up to isomorphism,
$\Pi$ and $\mathsf{U}$ are preserved in a lax way and $\mathsf{Bool}$ in an
oplax way. The specification is on the left, the implementations are on the
right.

$\displaystyle F_{\mathsf{K}}$
$\displaystyle{}:F\,(\mathsf{K}\,{\mathit{\oldTheta}})\cong\mathsf{K}\,(F\,{\mathit{\oldTheta}})$
$\displaystyle F_{\mathsf{K}}$ $\displaystyle{}:=F\,\mathsf{q}\circ
F_{\mathop{\triangleright}}^{-1}$ $\displaystyle F_{\Sigma}$
$\displaystyle{}:F\,(\Sigma\,A\,B)\cong\Sigma\,(F\,A)\,(F\,B[F_{\mathop{\triangleright}}^{-1}])$
$\displaystyle F_{\Sigma}$
$\displaystyle{}:=(F\,(\pi_{1}\,q),F\,(\pi_{2}\,q))[F_{\mathop{\triangleright}}^{-1}]$
$\displaystyle F_{\mathsf{Eq}}$
$\displaystyle{}:F\,(\mathsf{Eq}_{A}\,u\,v)\cong\mathsf{Eq}_{F\,A}\,(F\,u)\,(F\,v)$
$\displaystyle F_{\mathsf{Eq}}$
$\displaystyle{}:=\mathsf{refl}[F_{\mathop{\triangleright}}^{-1}]$
$\displaystyle F_{\Pi}$
$\displaystyle{}:\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}F\,(\Pi\,A\,B))(\Pi\,(F\,A)\,(F\,B[F_{\mathop{\triangleright}}^{-1}])[\mathsf{p}])\hskip
20.00003pt$ $\displaystyle F_{\Pi}$
$\displaystyle{}:=\mathsf{lam}\,(F\,(\mathsf{app}\,\mathsf{q})[F_{\mathop{\triangleright}}^{-1}])[F_{\mathop{\triangleright}}^{-1}]$
$\displaystyle F_{\mathsf{U}}$
$\displaystyle{}:\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}F\,\mathsf{U})\,\mathsf{U}$
$\displaystyle F_{\mathsf{U}}$
$\displaystyle{}:=\mathsf{c}(F\,(\mathsf{El}\,\mathsf{q})[F_{\mathop{\triangleright}}^{-1}])$
$\displaystyle F_{\mathsf{Bool}}^{-1}$
$\displaystyle{}:\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}\mathsf{Bool})\,(F\,\mathsf{Bool}[\mathsf{p}])$
$\displaystyle F_{\mathsf{Bool}}^{-1}$
$\displaystyle{}:=\mathsf{ite}\,\mathsf{q}\,(F\,\mathsf{true}[\mathsf{p}])\,(F\,\mathsf{false}[\mathsf{p}])$

We note that a consequence of preservation of
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
is that
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}F_{\mathop{\triangleright}}^{-1}=F_{\mathop{\triangleright}}^{-1}$.

###  5.2. The Gluing Displayed Model

A displayed model over a base model is equivalent to a model with a morphism
into the base. It can also be seen as the collection of motives and methods
for the induction principle of the syntax (the initial model). The components
of a displayed model can be computed for any generalised algebraic theory
using the methods in (Kaposi et al., 2019b). We mark displayed components with
a bullet. For example, displayed contexts are a set indexed over contexts:
$\mathsf{Con}^{\bullet}:\mathsf{Con}\rightarrow\mathsf{Set}$ where
$\mathsf{Con}$ is the set of contexts of the base model. Displayed types are
indexed implicitly over a base context, a displayed context at the base
context and a base type:
$\mathsf{Ty}^{\bullet}:\\{{\mathit{\oldGamma}}:\mathsf{Con}\\}\rightarrow\mathsf{Con}^{\bullet}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Ty}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Set}$.
The displayed variants of equations are well-typed because of the
corresponding equations in the base model.

###### Problem 5.2 (Gluing).

Given a weak morphism $F$ from $\mathcal{C}$ to $\mathcal{D}$, we construct a
displayed model of the global theory over $\mathcal{C}$.

###### Construction.

Gluing of a weak morphism from $\mathcal{C}$ to $\mathcal{D}$ gives a
displayed model over $\mathcal{C}$. This model construction is a
generalisation of logical predicates. A displayed context is a predicate over
$F$ applied to the context, a displayed type is a dependent predicate over $F$
applied to the type. A displayed substitution/term says expresses that $F$ of
the substitution/term respects the predicates.

$\displaystyle\mathsf{Con}^{\bullet}\,{\mathit{\oldGamma}}$
$\displaystyle{}:=\mathsf{Ty}\,(F\,{\mathit{\oldGamma}})$
$\displaystyle\mathsf{Ty}^{\bullet}\,{\mathit{\oldGamma}}^{\bullet}\,A$
$\displaystyle{}:=\mathsf{Ty}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}\mathop{\triangleright}F\,A[\mathsf{p}])$
$\displaystyle\mathsf{Sub}^{\bullet}\,{\mathit{\oldDelta}}^{\bullet}\,{\mathit{\oldGamma}}^{\bullet}\,\sigma$
$\displaystyle{}:=\mathsf{Tm}\,(F\,{\mathit{\oldDelta}}\mathop{\triangleright}{\mathit{\oldDelta}}^{\bullet})\,({\mathit{\oldGamma}}^{\bullet}[F\,\sigma\circ\mathsf{p}])\hskip
30.00005pt$
$\displaystyle\mathsf{Tm}^{\bullet}\,{\mathit{\oldGamma}}^{\bullet}\,A^{\bullet}\,t$
$\displaystyle{}:=\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet})\,(A^{\bullet}[\mathsf{id},F\,t[\mathsf{p}]])$

The core calculus is glued using the same technique as the standard model:
composition and substitution are modelled by substitution, context extension
by $\Sigma$ types.

$\displaystyle\sigma^{\bullet}\circ^{\bullet}\rho^{\bullet}$
$\displaystyle{}:=\sigma^{\bullet}[F\,\rho\circ\mathsf{p},\rho^{\bullet}]$
$\displaystyle t^{\bullet}[\sigma^{\bullet}]^{\bullet}$
$\displaystyle{}:=t^{\bullet}[F\,\sigma\circ\mathsf{p},\sigma^{\bullet}]$
$\displaystyle\mathsf{id}^{\bullet}$ $\displaystyle{}:=\mathsf{q}$
$\displaystyle{\mathit{\oldGamma}}^{\bullet}\mathbin{{\mathop{\triangleright}}^{\bullet}}A^{\bullet}$
$\displaystyle{}:=\Sigma\,({\mathit{\oldGamma}}^{\bullet}[F\,\mathsf{p}])\,(A^{\bullet}[F\,\mathsf{p}\circ\mathsf{p},\mathsf{q},F\,\mathsf{q}[\mathsf{p}]])$
$\displaystyle\diamond^{\bullet}$ $\displaystyle{}:=\top$
$\displaystyle(\sigma^{\bullet},^{\bullet}t^{\bullet})$
$\displaystyle{}:=(\sigma^{\bullet},t^{\bullet})$
$\displaystyle\epsilon^{\bullet}$ $\displaystyle{}:=\mathsf{tt}$
$\displaystyle\mathsf{p}^{\bullet}$ $\displaystyle{}:=\pi_{1}\,\mathsf{q}$
$\displaystyle A^{\bullet}[\sigma^{\bullet}]^{\bullet}$
$\displaystyle{}:=A^{\bullet}[(F\,\sigma\circ\mathsf{p},\sigma^{\bullet})\uparrow]\hskip
75.0001pt$ $\displaystyle\mathsf{q}^{\bullet}$
$\displaystyle{}:=\pi_{2}\,\mathsf{q}$

The type formers $\mathsf{K}$, $\top$, $\Sigma$, $\mathsf{Eq}$, $\Pi$,
$\mathsf{U}$ and $\mathsf{Bool}$ in the gluing displayed model are defined as
follows. $\mathsf{K}^{\bullet}$ simply returns its argument context,
$\top^{\bullet}$, $\Sigma^{\bullet}$, $\mathsf{Eq}^{\bullet}$ are pointwise.
$\Pi^{\bullet}$ expresses that if the predicate holds for an input, it holds
for the output. $\mathsf{U}^{\bullet}$ gives predicate space,
$\mathsf{Bool}^{\bullet}$ for a $b$ in $F\,\mathsf{Bool}$ says that there is a
boolean which is equal to $b$ when mapped using $F_{\mathsf{Bool}}^{-1}$. The
definitions are straightforward, but technical: adjustments using
$F_{\mathop{\triangleright}}^{-1}$ and the comparison maps (e.g. $F_{\Sigma}$,
$F_{\Pi}$) have to make things match. The definitions below satisfy all the
equations of the displayed model.

$\displaystyle\mathsf{K}^{\bullet}\,{\mathit{\oldTheta}}^{\bullet}$
$\displaystyle{}:={\mathit{\oldTheta}}^{\bullet}[F_{\mathsf{K}}][F\,\epsilon\circ\mathsf{p}^{2},\mathsf{q}]$
$\displaystyle\top^{\bullet}$ $\displaystyle{}:=\top$
$\displaystyle\mathsf{tt}^{\bullet}$ $\displaystyle{}:=\mathsf{tt}$
$\displaystyle\Sigma^{\bullet}\,A^{\bullet}\,B^{\bullet}[\gamma,\gamma^{\bullet},F_{\Sigma}^{-1}[\gamma,(a,b)]]$
$\displaystyle{}:=\Sigma\,(A^{\bullet}[\gamma,\gamma^{\bullet},a])\,(B^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\gamma,a)\circ\mathsf{p},(\gamma^{\bullet}[\mathsf{p}],\mathsf{q}),b[\mathsf{p}]])$
$\displaystyle(u^{\bullet},^{\bullet}v^{\bullet})$
$\displaystyle{}:=(u^{\bullet},v^{\bullet})$
$\displaystyle\pi_{1}^{\bullet}\,t^{\bullet}$
$\displaystyle{}:=\pi_{1}\,t^{\bullet}$
$\displaystyle\pi_{2}^{\bullet}\,t^{\bullet}$
$\displaystyle{}:=\pi_{2}\,t^{\bullet}$
$\displaystyle\mathsf{Eq}^{\bullet}_{A^{\bullet}}\,u^{\bullet}\,v^{\bullet}$
$\displaystyle{}:=\mathsf{Eq}_{A^{\bullet}[\mathsf{p},F\,u[\mathsf{p}^{2}]]}\,(u^{\bullet}[\mathsf{p}])\,(v^{\bullet}[\mathsf{p}])$
$\displaystyle\mathsf{refl}^{\bullet}$ $\displaystyle{}:=\mathsf{refl}$
$\displaystyle\Pi^{\bullet}\,A^{\bullet}\,B^{\bullet}[\gamma,\gamma^{\bullet},t]$
$\displaystyle{}:=\Pi\,(F\,A[\gamma])\,\big{(}\Pi\,(A^{\bullet}[(\gamma,\gamma^{\bullet})\uparrow])\,$
$\displaystyle\hskip
20.00003pt(B^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\gamma\uparrow)\circ\mathsf{p},(\gamma^{\bullet}[\mathsf{p}^{2}],\mathsf{q}),\mathsf{app}\,(F_{\Pi}[\gamma,t])[\mathsf{p}]])\big{)}$
$\displaystyle\mathsf{lam}^{\bullet}\,t^{\bullet}$
$\displaystyle{}:=\mathsf{lam},\big{(}\mathsf{lam}\,(t^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\mathsf{p}^{3},1),(2,0)])\big{)}$
$\displaystyle\mathsf{app}^{\bullet}\,t^{\bullet}$
$\displaystyle{}:=\mathsf{app},(\mathsf{app}\,t)[F\,\mathsf{p}\circ\mathsf{p},\pi_{1}\,q,F\,\mathsf{q}[\mathsf{p}],\pi_{2}\,\mathsf{q}]$
$\displaystyle\mathsf{U}^{\bullet}[\gamma,\gamma^{\bullet},a]$
$\displaystyle{}:=\mathsf{El}\,(F_{\mathsf{U}}[\gamma,a])\Rightarrow\mathsf{U}$
$\displaystyle\mathsf{El}^{\bullet}\,a^{\bullet}$
$\displaystyle{}:=\mathsf{El}\,(\mathsf{app}\,a^{\bullet})$
$\displaystyle\mathsf{c}^{\bullet}\,A^{\bullet}$
$\displaystyle{}:=\mathsf{lam}\,(\mathsf{c}\,A^{\bullet})$
$\displaystyle\mathsf{Bool}^{\bullet}[\gamma,\gamma^{\bullet},b]$
$\displaystyle{}:=\Sigma\,\mathsf{Bool}\,(\mathsf{Eq}_{F\,\mathsf{Bool}[\gamma][\mathsf{p}]}\,(F_{\mathsf{Bool}}^{-1}[\gamma\uparrow])\,(b[\mathsf{p}]))$
$\displaystyle\mathsf{true}^{\bullet}$
$\displaystyle{}:=(\mathsf{true},\mathsf{refl})$
$\displaystyle\mathsf{false}^{\bullet}$
$\displaystyle{}:=(\mathsf{false},\mathsf{refl})$
$\displaystyle\mathsf{ite}^{\bullet}\,t^{\bullet}\,u^{\bullet}\,v^{\bullet}$
$\displaystyle{}:=\mathsf{ite}\,(\pi_{1}\,t^{\bullet})\,u^{\bullet}\,v^{\bullet}$

The displayed versions of the
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}$
and
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$
operators are defined as follows.

$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}{\mathit{\oldGamma}}^{\bullet}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}\hskip
40.00006pt\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}\sigma^{\bullet}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\sigma^{\bullet}\hskip
40.00006pt\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}A^{\bullet}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}A^{\bullet}\hskip
40.00006pt\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}t^{\bullet}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}t^{\bullet}$
${{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}^{\bullet}}_{{\mathit{\oldGamma}}^{\bullet}}:=\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]\hskip
40.00006pt{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}^{\bullet}}_{{\mathit{\oldGamma}}^{\bullet}}:=\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]\hskip
40.00006pt{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}^{\bullet}}_{{\mathit{\oldGamma}}^{\bullet}}:=\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]$

$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}{\mathit{\oldGamma}}^{\bullet}$
has to be in
$\mathsf{Ty}\,(F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}))$
and
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}$
is in
$\mathsf{Ty}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,{\mathit{\oldGamma}}))$,
but these are equal because $F$ respects
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
strictly. The situation is similar for the other operators.

For
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}^{\bullet}\,\sigma^{\bullet}\,t_{k}^{\bullet}\,t^{\bullet}$,
we need a term in

$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldDelta}}\mathop{\triangleright}{\mathit{\oldDelta}}^{\bullet})\,\big{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\Pi^{\bullet}\,A^{\bullet}\,B^{\bullet})[F\,\sigma\circ\mathsf{p},\sigma^{\bullet},F\,({\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}\,\sigma\,t_{k}\,t)[\mathsf{p}]]\big{)}$
$\displaystyle=$ (introduce abbreviation $\rho$)
$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldDelta}}\mathop{\triangleright}{\mathit{\oldDelta}}^{\bullet})\,\big{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\Pi^{\bullet}\,A^{\bullet}\,B^{\bullet})[\rho]\big{)}$
$\displaystyle=$
$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldDelta}}\mathop{\triangleright}{\mathit{\oldDelta}}^{\bullet})\,\bigg{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\Big{(}\Pi\,(F\,A[\mathsf{p}^{2}])\,\big{(}\Pi\,(A^{\bullet}[\mathsf{p}^{2},\mathsf{q}])\,(B^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\mathsf{p}^{4},1),(3,0),F_{\Pi}[\mathsf{p}^{4},2]\mathbin{\$}1])\big{)}\Big{)}[\rho]\bigg{)}$
$\displaystyle\cong$ (curry-uncurry)
$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldDelta}}\mathop{\triangleright}{\mathit{\oldDelta}}^{\bullet})\,\bigg{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\Big{(}\Pi\,\big{(}\Sigma\,(F\,A[\mathsf{p}^{2}])\,(A^{\bullet}[\mathsf{p}^{2},\mathsf{q}])\big{)}\,\big{(}B^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\mathsf{p}^{3},\pi_{1}\,0),(2,\pi_{2}\,0),F_{\Pi}[\mathsf{p}^{3},1]\mathbin{\$}\pi_{1}\,0]\big{)}\Big{)}[\rho]\bigg{)}.$

We can directly apply
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}$
to build an element of this latter type reusing the uncurried versions of
$t_{k}^{\bullet}$ and $t^{\bullet}$, respectively.

$w:={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}\,\rho\,\Big{(}\mathsf{lam}\,\big{(}\mathsf{app}\,(\mathsf{app}\,t_{k}^{\bullet})[\mathsf{p},\pi_{1}\,\mathsf{q},\pi_{2}\,\mathsf{q}]\big{)}\Big{)}\Big{(}\mathsf{lam}\,\big{(}\mathsf{app}\,(\mathsf{app}\,t^{\bullet})[\mathsf{p},\pi_{1}\,\mathsf{q},\pi_{2}\,\mathsf{q}]\big{)}\Big{)}$

Now we curry the resulting term under
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
to obtain the definition of
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}^{\bullet}$:

${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}^{\bullet}\,\sigma^{\bullet}\,t_{k}^{\bullet}\,t^{\bullet}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{lam}\,(\mathsf{lam}\,(2\mathbin{\$}(1,0))))[\rho,w]$

For
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{unspan}}}^{\bullet}\,A_{k}^{\bullet}\,A^{\bullet}\,t_{k}^{\bullet}$,
we need a term in

$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet})\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}\,\mathsf{U}^{\bullet}[\epsilon^{\bullet}]^{\bullet}[\mathsf{id},F\,(\mathsf{unspan}\,A_{k}\,A\,t_{k})[\mathsf{p}]])$
$\displaystyle=$
$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet})\,\Big{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\big{(}F\,(\mathsf{El}\,\mathsf{q})[F_{\mathop{\triangleright}}^{-1}]\Rightarrow\mathsf{U}\big{)}\big{[}F\,\epsilon\circ\mathsf{p},F\,(\mathsf{unspan}\,A_{k}\,A\,t_{k})[\mathsf{p}]\big{]}\Big{)}$
$\displaystyle=$ (introduce abbreviation $\rho$)
$\displaystyle\mathsf{Tm}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet})\,\Big{(}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\big{(}F\,(\mathsf{El}\,\mathsf{q})[F_{\mathop{\triangleright}}^{-1}]\Rightarrow\mathsf{U}\big{)}[\rho]\Big{)},$

which is the span of a predicate. We already have predicates on $F\,A_{k}$ and
$F\,A$ with a map from witnesses of the second one to the first one that lies
over $F\,t_{k}$:

$\displaystyle A_{k}^{\bullet}$
$\displaystyle{}:\mathsf{Ty}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}\mathop{\triangleright}F\,A_{k}[\mathsf{p}])$
$\displaystyle A^{\bullet}$
$\displaystyle{}:\mathsf{Ty}\,(F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}\mathop{\triangleright}F\,A[\mathsf{p}])$
$\displaystyle t_{k}^{\bullet}$
$\displaystyle{}:\mathsf{Tm}\,(F\,({\mathit{\oldGamma}}\mathop{\triangleright}A)\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}\mathbin{{\mathop{\triangleright}}^{\bullet}}A^{\bullet})\,(A_{k}^{\bullet}[F\,\mathsf{p}\circ\mathsf{p},\pi_{1}\,\mathsf{q},F\,t_{k}[\mathsf{p}]])$

The way to make terms in
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
of a function space is by
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}$.
The function (the predicate) at the base is essentially $A_{k}^{\bullet}$, the
predicate at the apex is given by
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{unspan}}}\,(A_{k}^{\bullet}[\dots])\,A^{\bullet}\,(t_{k}^{\bullet}[\dots])$
where $A_{k}^{\bullet}$ and $t_{k}^{\bullet}$ have to be substituted to plug
in their dependencies properly.

$\displaystyle{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{unspan}}}^{\bullet}\,A_{k}^{\bullet}\,A^{\bullet}\,t_{k}^{\bullet}:=$
$\displaystyle\hskip
20.00003pt{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{mk}{\forall}{\Pi}}}\,\rho\,\big{(}\mathsf{lam}\,(\mathsf{c}\,A_{k}^{\bullet})\big{)}\,\bigg{(}\mathsf{lam}\,\Big{(}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{unspan}}}\,$
$\displaystyle\big{(}A_{k}^{\bullet}[\mathsf{p},F\,t_{k}[F_{\mathop{\triangleright}}^{-1}][\mathsf{p}^{2},\mathsf{q}]]\big{)}\,A^{\bullet}\,\big{(}t_{k}^{\bullet}[F_{\mathop{\triangleright}}^{-1}\circ(\mathsf{p}^{3},1),(2,0)]\big{)}\Big{)}\bigg{)}$

The equations for the global syntax follow from the preservation properties of
the weak morphism. Here is a typical example:

$\displaystyle\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{\bullet}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}^{\bullet}_{{\mathit{\oldGamma}}^{\bullet}}$
$\displaystyle=$
$\displaystyle\mathsf{q}[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]$
$\displaystyle=$ (one of the five equations)
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}\circ{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]$
$\displaystyle=$
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(F\,{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]$
$\displaystyle=$ ($F$ commutes with
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
on contexts)
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]$
$\displaystyle=$
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][\mathsf{p}\circ{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}},\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]]$
$\displaystyle=$
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\mathsf{p})\circ{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}},\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]]$
$\displaystyle=$ (naturality of
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$)
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}}\circ\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\mathsf{p}),\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]]$
$\displaystyle=$
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}}\circ\mathsf{p},\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]]$
$\displaystyle=$ ($F$ commutes with
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$)
$\displaystyle\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{F\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}^{\bullet}}][F\,{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{\mathit{\oldGamma}}\circ\mathsf{p},\mathsf{q}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{F\,{\mathit{\oldGamma}}\mathop{\triangleright}{\mathit{\oldGamma}}^{\bullet}}]]$
$\displaystyle=$
$\displaystyle{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}^{\bullet}_{\forall^{\bullet}{\mathit{\oldGamma}}^{\bullet}}\circ^{\bullet}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}^{\bullet}_{{\mathit{\oldGamma}}^{\bullet}}$

This completes the construction of the gluing displayed model. ∎

###  5.3. The Global Section Functor

We define a way to interpret morphisms in $\square$ in our syntax (see
Definition 3.3). The substitution $\ulcorner f\urcorner_{\mathit{\oldGamma}}$
for an $f:\square(J,I)$ is defined mutually with three equations by induction
on $f$:

$\displaystyle\ulcorner f\urcorner_{\mathit{\oldGamma}}:{}$
$\displaystyle\mathsf{Sub}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\mathit{\oldGamma}})\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}{\mathit{\oldGamma}})$
$\displaystyle\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{n}{\mathit{\oldGamma}}}\circ\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}\circ\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+n}{\mathit{\oldGamma}}}$
$\displaystyle\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{\mathit{\oldGamma}}\circ\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{n}{\mathit{\oldGamma}}}=\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+n}{\mathit{\oldGamma}}}\circ\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{\mathit{\oldGamma}}$
$\displaystyle\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{\mathit{\oldGamma}}\circ\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{2+n}{\mathit{\oldGamma}}}=\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{2+n}{\mathit{\oldGamma}}}\circ\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I+n}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{\mathit{\oldGamma}}$

$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\,{\mathit{\oldGamma}}$
denotes the $I$ times iteration of
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
on ${\mathit{\oldGamma}}$. The different cases333An alternative definition of
$\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\urcorner_{\mathit{\oldGamma}}$ uses
$\ulcorner\mathsf{suc}\,f\urcorner_{\mathit{\oldGamma}}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\ulcorner
f\urcorner_{\mathit{\oldGamma}}$, $\ulcorner
k_{I}\urcorner_{\mathit{\oldGamma}}={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\mathit{\oldGamma}}}$,
and so on. This version generates a global section functor which only
satisfies
$\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\cong\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,{\mathit{\oldGamma}})$
up to isomorphism. An isomorphism is enough to build a gluing model, however
it is much more tedious than our current, stricter approach. of
$\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$:

$\displaystyle\ulcorner f\circ g\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\ulcorner g\urcorner_{\mathit{\oldGamma}}\circ\ulcorner
f\urcorner_{\mathit{\oldGamma}}\hskip 50.00008pt$
$\displaystyle\ulcorner\mathsf{suc}\,f\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}}\hskip
80.00012pt$
$\displaystyle\ulcorner\mathsf{R}_{I}\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}_{{\mathit{\oldGamma}}}$
$\displaystyle\ulcorner\mathsf{id}\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\mathsf{id}$ $\displaystyle\ulcorner
k_{I}\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{{\mathit{\oldGamma}}}$
$\displaystyle\ulcorner\mathsf{S}_{I}\urcorner_{\mathit{\oldGamma}}$
$\displaystyle{}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}_{{\mathit{\oldGamma}}}$

The fact that $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\urcorner_{\mathit{\oldGamma}}$ preserves the equations for the
morphisms in $\square$ is direct except for the three naturality equations
$k_{I}\circ f=\mathsf{suc}\,f\circ k_{J}$,
$\mathsf{R}_{I}\circ\mathsf{suc}\,f=f\circ\mathsf{R}_{J}$ and
$\mathsf{S}_{I}\circ\mathsf{suc}\,(\mathsf{suc}\,f)=\mathsf{suc}\,(\mathsf{suc}\,f)\circ\mathsf{S}_{J}$
which follow from the $n=0$ cases of the above three equations.

We also prove by induction on $f$ that for any $\sigma$, $\ulcorner
f\urcorner_{\sigma}:\ulcorner
f\urcorner_{\mathit{\oldGamma}}\circ\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\sigma=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}\sigma\circ\ulcorner
f\urcorner_{\mathit{\oldDelta}}.$

Now we construct the weak morphism on which we will glue for canonicity. This
can be seen as a cubical nerve functor.

###### Problem 5.3 (Global section functor).

We construct a weak morphism $\mathsf{G}$ from
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$
to $\mathsf{PSh}(\square)$.

###### Construction.

$\displaystyle\mathsf{G}:\mathsf{Con}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\rightarrow\mathsf{Con}_{\mathsf{PSh}(\square)}\hskip
80.00012pt$
$\displaystyle\mathsf{G}:\mathsf{Sub}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,{\mathit{\oldDelta}}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Sub}_{\mathsf{PSh}(\square)}\,(\mathsf{G}\,{\mathit{\oldDelta}})\,(\mathsf{G}\,{\mathit{\oldGamma}})$
$\displaystyle\mathsf{G}\,{\mathit{\oldGamma}}\,I:=\mathsf{Sub}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\,{\mathit{\oldGamma}})$
$\displaystyle\mathsf{G}\,\sigma\,\delta^{I}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\,\sigma\circ\delta^{I}$
$\displaystyle\gamma^{I}[f]_{\mathsf{G}\,{\mathit{\oldGamma}}}:=\ulcorner
f\urcorner_{\mathit{\oldGamma}}\circ\gamma^{I}$

The functor laws for $\mathsf{G}\,{\mathit{\oldGamma}}$ follow from the
definition of $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\urcorner_{\mathit{\oldGamma}}$ and from the categorical laws in
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$.
Naturality of $\mathsf{G}\,\sigma$ is a consequence of $\ulcorner
f\urcorner_{\sigma}$. On types and terms:

$\displaystyle\mathsf{G}:\mathsf{Ty}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,{\mathit{\oldGamma}}\rightarrow\mathsf{Ty}_{\mathsf{PSh}(\square)}\,(\mathsf{G}\,{\mathit{\oldGamma}})$
$\displaystyle\mathsf{G}:\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,{\mathit{\oldGamma}}\,A\rightarrow\mathsf{Tm}_{\mathsf{PSh}(\square)}\,(\mathsf{G}\,{\mathit{\oldGamma}})\,(\mathsf{G}\,A)$
$\displaystyle\mathsf{G}\,A\,I\,\gamma^{I}:=\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\,A[\gamma^{I}])\hskip
60.00009pt$
$\displaystyle\mathsf{G}\,t\,\gamma^{I}:=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\,t[\gamma^{I}]$
$\displaystyle a^{I}[f]_{\mathsf{G}\,A}:=\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\gamma^{I},a^{I}]$

The functor laws for $\mathsf{G}\,A$ follow directly and naturality for
$\mathsf{G}\,t$ is proven as follows.

$\displaystyle\mathsf{G}\,t\,\gamma^{I}[f]_{\mathsf{G}\,A}=\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\gamma^{I},\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}t[\gamma^{I}]]=\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(\mathsf{id},t)][\gamma^{I}]\overset{\ulcorner
f\urcorner_{\sigma}}{=}\mathsf{q}[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}(\mathsf{id},t)][\ulcorner
f\urcorner_{{\mathit{\oldGamma}}}][\gamma^{I}]=$
$\displaystyle\mathsf{q}[\mathsf{id},\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}t][\ulcorner
f\urcorner_{{\mathit{\oldGamma}}}][\gamma^{I}]=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}t[\ulcorner
f\urcorner_{\mathit{\oldGamma}}\circ\gamma^{I}]=\mathsf{G}\,t\,(\gamma^{I}[f]_{\mathsf{G}\,{\mathit{\oldGamma}}})$

It is easy to see that $\mathsf{G}$ is a functor, it is more interesting that
it preserves substitution of types:

$\displaystyle\mathsf{G}\,(A[\sigma])\,I\,\delta^{I}=\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(A[\sigma])[\delta^{I}])=\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}A[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\sigma][\delta^{I}])=\mathsf{G}\,A\,I\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\sigma\circ\delta^{I})=$
$\displaystyle\mathsf{G}\,A\,I\,(G\,\sigma\,\delta^{I})=\mathsf{G}\,A[G\,\sigma]\,I\,\delta^{I}$
$\displaystyle a^{I}[f]_{\mathsf{G}\,(A[\sigma])}=\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldDelta}}\mathop{\triangleright}A[\sigma]}][\delta^{I},a^{I}]=\mathsf{q}[\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{J}(\sigma\uparrow)][\ulcorner
f\urcorner_{{\mathit{\oldDelta}}\mathop{\triangleright}A[\sigma]}][\delta^{I},a^{I}]\overset{\ulcorner
f\urcorner_{\sigma\uparrow}}{=}$ $\displaystyle\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(\sigma\uparrow)][\delta^{I},a^{I}]=\mathsf{q}[\ulcorner
f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}\sigma\circ\delta^{I},a^{I}]=a^{I}[f]_{\mathsf{G}\,A[\mathsf{G}\,\sigma]}$

A similar proof shows that $\mathsf{G}$ preserves term substitution. We define
preservation of $\diamond$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\mathop{\triangleright}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ as
follows. In the latter case we replace a metatheoretic pairing operation with
a syntactic extended substitution former.

$\displaystyle\mathsf{G}_{\diamond}^{-1}:\mathsf{Sub}_{\mathsf{PSh}(\square)}\,\diamond\,(\mathsf{G}\,\diamond)\hskip
50.00008pt$
$\displaystyle\mathsf{G}_{\mathop{\triangleright}}^{-1}:\mathsf{Sub}_{\mathsf{PSh}(\square)}\,(\mathsf{G}\,{\mathit{\oldGamma}}\mathop{\triangleright}\mathsf{G}\,A)\,(\mathsf{G}\,({\mathit{\oldGamma}}\mathop{\triangleright}A))$
$\displaystyle\mathsf{G}_{\diamond}^{-1}\,\\_:=\epsilon_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}$
$\displaystyle\mathsf{G}_{\mathop{\triangleright}}^{-1}\,(\gamma^{I},a^{I}):=(\gamma^{I},_{\mathop{\triangleright}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}}a^{I})$

They obviously satisfy the necessary equations using the universal properties
of $\diamond$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\mathop{\triangleright}\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$.

We verify that $\mathsf{G}$ preserves
$\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}$
and commutes with
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}$,
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$.
$\mathsf{G}$ commutes with $\forall$ on contexts

$\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})\,I=\mathsf{Sub}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}))=\mathsf{Sub}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+I}{\mathit{\oldGamma}})=\mathsf{G}\,{\mathit{\oldGamma}}\,(1+I)=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,{\mathit{\oldGamma}})\,I$
$\gamma^{1+I}[f]_{\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}})}=\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}}\circ\gamma^{1+I}=\ulcorner\mathsf{suc}\,f\urcorner_{{\mathit{\oldGamma}}}\circ\gamma^{1+I}=\gamma^{1+I}[\mathsf{suc}\,f]_{\mathsf{G}\,{\mathit{\oldGamma}}}=\gamma^{1+I}[f]_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,{\mathit{\oldGamma}})},$

substitutions

$\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\sigma)\,\delta^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}\sigma)\circ\delta^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+I}\sigma\circ\delta^{1+I}=\mathsf{G}\,\sigma\,\delta^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,\sigma)\,\delta^{1+I},$

types

$\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}A)\,I\,\gamma^{1+I}=\mathsf{Tm}\,\diamond\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+I}A[\gamma^{1+I}])=\mathsf{G}\,A\,(1+I)\,\gamma^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,A)\,I\,\gamma^{1+I}$
$a^{1+I}[f]_{\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}A)}=\mathsf{q}[\ulcorner
f\urcorner_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}{\mathit{\oldGamma}}\mathop{\triangleright}\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}A}][\gamma^{1+I},a^{1+I}]=\mathsf{q}[\ulcorner\mathsf{suc}\,f\urcorner_{{\mathit{\oldGamma}}\mathop{\triangleright}A}][\gamma^{1+I},a^{1+I}]=a^{1+I}[f]_{\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,A)},$

and terms

$\mathsf{G}\,(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}t)\,\gamma^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}(\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}t)[\gamma^{1+I}]=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{1+I}t[\gamma^{1+I}]=\mathsf{G}\,t\,\gamma^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}(\mathsf{G}\,t)\,\gamma^{1+I}.$

Preservation of
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}$
is given by

$\mathsf{G}\,{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}\,\gamma^{1+I}=\mathord{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\forall}}}^{I}{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathit{\oldGamma}}\circ\gamma^{1+I}=\ulcorner
k_{I}\urcorner_{\mathit{\oldGamma}}\circ\gamma^{1+I}=\gamma^{1+I}[{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{I}]_{\mathsf{G}\,{\mathit{\oldGamma}}}={\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{k}}_{\mathsf{G}\,{\mathit{\oldGamma}}}\,\gamma^{1+I},$

preservation of
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{R}}}$
and
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{S}}}$
are shown analogously. ∎

###  5.4. Reaping the Fruits

###### Theorem 5.4 (Canonicity).

In the local or global syntax, for a $t:\mathsf{Tm}\,\diamond\,\mathsf{Bool}$,
we have $t=\mathsf{true}$ or $t=\mathsf{false}$.

###### Proof.

By gluing along the global section functor, we obtain a displayed model over
the syntax of the global theory, and given a
$t:\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,\mathsf{Bool}$,
by induction of
${\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}$,
we get a

$\mathsf{Tm}_{\mathsf{PSh}(\square)}\,(\mathsf{G}\,\diamond\mathop{\triangleright}\top)\,(\Sigma\,\mathsf{Bool}\,(\mathsf{Eq}\,(\mathsf{ite}\,\mathsf{q}\,(\mathsf{G}\,\mathsf{true}[\mathsf{p}])\,(\mathsf{G}\,\mathsf{false}[\mathsf{p}]))\,(\mathsf{G}\,t[\mathsf{p}]))),$

and providing the $\mathsf{id}_{\diamond}:\mathsf{G}\,\diamond\,\diamond$ and
the element of the metatheoretic unit set as input we obtain

$(b:\mathbbm{2})\times\mathsf{if}\,b\,\mathsf{then}\,\mathsf{true}\,\mathsf{else}\,\mathsf{false}=t.$

Given a term in the local syntax
$t:\mathsf{Tm}_{\mathsf{Syn}}\,\diamond\,\mathsf{Bool}$, we have
$\alpha\,t:\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,(\alpha\,\diamond)\,(\alpha\,\mathsf{Bool})$
where $\alpha$ is the map from the global syntax to the local syntax defined
in Section 4.4. As $\alpha$ does not affect the core syntax this is
$\alpha\,t:\mathsf{Tm}_{{\color[rgb]{0.8,0.25,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.25,0.33}{\mathsf{Syn}}}}\,\diamond\,\mathsf{Bool}$
and we learn from canonicity say that $\alpha\,t=\mathsf{true}$. Now applying
$\beta$ to such an equation we obtain
$t=\beta\,(\alpha\,t)=\beta\,\mathsf{true}=\mathsf{true}$ as $\beta$ also does
not affect that core calculus. ∎

##  6\. Future work

We presented a type theory with internal parametricity, a presheaf model and a
canonicity proof. It can be seen as a baby version of higher observational
type theory (HOTT). To obtain HOTT, we plan to add the following additional
features to our theory:

  * •

a bridge type which can be seen as an indexed version of $\forall$,

  * •

Reedy fibrancy, which replaces spans by relations,

  * •

a strictification construction which turns the isomorphism for $\Pi$ types
into a definitional equality (in case of bridge, we also need the same for
$\Sigma$),

  * •

Kan fibrancy, which adds transport and turns the bridge type into a proper
identity type. This would also change the correspondence between
$\forall\mathsf{U}$ and spans into $\forall\mathsf{U}$ and equivalences.

We would also like to include general (higher) inductive and coinductive
types. Concerning the metatheory, we plan to use internal language techniques
(Sterling, 2022; Bocquet et al., 2023) to obtain a higher level canonicity
proof, and extend it to normalisation.

Several of our constructions in this paper follow a generic pattern: most of
the global theory and gluing should be derivable from the 2-category in Figure
1 similarly to the way it is done for multimodal type theory (Gratzer, 2023).

###### Acknowledgements.

We thank the anonymous reviewers for their comments and suggestions. We thank
Rafaël Bocquet, Hugo Herbelin, András Kovács and Christian Sattler for
discussions related to the topics of this paper. The first and third authors
were supported by project no. Grant #TKP2021-NVA-29 which has been implemented
with the support provided by the Sponsor Ministry of Culture and Innovation of
Hungary from the National Research, Development and Innovation Fund , financed
under the TKP2021-NVA funding scheme. This material is based upon work
supported by the Sponsor Air Force Office of Scientific Research  under award
number Grant #FA9550-21-1-0009.

## References

  * (1)
  * Altenkirch et al. (2016) Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016\.  Extending Homotopy Type Theory with Strict Equality. In _25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France_ _(LIPIcs, Vol. 62)_ , Jean-Marc Talbot and Laurent Regnier (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:17.  https://doi.org/10.4230/LIPIcs.CSL.2016.21
  * Altenkirch and Kaposi (2015) Thorsten Altenkirch and Ambrus Kaposi. 2015.  Towards a Cubical Type Theory without an Interval. In _21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia_ _(LIPIcs, Vol. 69)_ , Tarmo Uustalu (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 3:1–3:27.  https://doi.org/10.4230/LIPIcs.TYPES.2015.3
  * Altenkirch and Kaposi (2016) Thorsten Altenkirch and Ambrus Kaposi. 2016.  Type theory in type theory using quotient inductive types. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016_ , Rastislav Bod1́k and Rupak Majumdar (Eds.). ACM, 18–29.  https://doi.org/10.1145/2837614.2837638
  * Angiuli et al. (2021) Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. 2021.  Syntax and models of Cartesian cubical type theory.  _Math. Struct. Comput. Sci._ 31, 4 (2021), 424–468.  https://doi.org/10.1017/S0960129521000347
  * Annenkov et al. (2017) Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. 2017\.  Two-Level Type Theory and Applications.  _CoRR_ abs/1705.03307 (2017).  arXiv:1705.03307 http://arxiv.org/abs/1705.03307
  * Bernardy et al. (2015) Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. 2015\.  A Presheaf Model of Parametric Type Theory. In _The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015_ _(Electronic Notes in Theoretical Computer Science, Vol. 319)_ , Dan R. Ghica (Ed.). Elsevier, 67–82.  https://doi.org/10.1016/j.entcs.2015.12.006
  * Bernardy et al. (2010) Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2010\.  Parametricity and dependent types. In _Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010_ , Paul Hudak and Stephanie Weirich (Eds.). ACM, 345–356.  https://doi.org/10.1145/1863543.1863592
  * Bernardy and Moulin (2012) Jean-Philippe Bernardy and Guilhem Moulin. 2012.  A Computational Interpretation of Parametricity. In _Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012_. IEEE Computer Society, 135–144.  https://doi.org/10.1109/LICS.2012.25
  * Bernardy and Moulin (2013) Jean-Philippe Bernardy and Guilhem Moulin. 2013.  Type-theory in color. In _ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013_ , Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 61–72.  https://doi.org/10.1145/2500365.2500577
  * Bezem et al. (2013) Marc Bezem, Thierry Coquand, and Simon Huber. 2013\.  A Model of Type Theory in Cubical Sets. In _19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France_ _(LIPIcs, Vol. 26)_ , Ralph Matthes and Aleksy Schubert (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 107–128.  https://doi.org/10.4230/LIPIcs.TYPES.2013.107
  * Bocquet et al. (2023) Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. 2023\.  For the Metatheory of Type Theory, Internal Sconing Is Enough. In _8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy_ _(LIPIcs, Vol. 260)_ , Marco Gaboardi and Femke van Raamsdonk (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 18:1–18:23.  https://doi.org/10.4230/LIPIcs.FSCD.2023.18
  * Booij et al. (2016) Auke Bart Booij, Mart1́n Hötzel Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. 2016.  Parametricity, Automorphisms of the Universe, and Excluded Middle. In _22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia_ _(LIPIcs, Vol. 97)_ , Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 7:1–7:14.  https://doi.org/10.4230/LIPICS.TYPES.2016.7
  * Boulier et al. (2017) Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017.  The next 700 syntactical models of type theory. In _Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017_ , Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 182–194.  https://doi.org/10.1145/3018610.3018620
  * Buchholtz and Morehouse (2017) Ulrik Buchholtz and Edward Morehouse. 2017.  Varieties of Cubical Sets. In _Relational and Algebraic Methods in Computer Science - 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings_ _(Lecture Notes in Computer Science, Vol. 10226)_ , Peter Höfner, Damien Pous, and Georg Struth (Eds.). 77–92.  https://doi.org/10.1007/978-3-319-57418-9_5
  * Castellan et al. (2019) Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2019\.  Categories with Families: Unityped, Simply Typed, and Dependently Typed.  _CoRR_ abs/1904.00827 (2019).  arXiv:1904.00827 http://arxiv.org/abs/1904.00827
  * Cavallo (2021) Evan Cavallo. 2021\.  _Higher Inductive Types and Internal Parametricity for Cubical Type Theory_.  Ph. D. Dissertation. Carnegie Mellon University, USA.  https://doi.org/10.1184/r1/14555691
  * Cavallo and Harper (2021) Evan Cavallo and Robert Harper. 2021.  Internal Parametricity for Cubical Type Theory.  _Log. Methods Comput. Sci._ 17, 4 (2021).  https://doi.org/10.46298/lmcs-17(4:5)2021
  * Cohen et al. (2015) Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2015.  Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In _21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia_ _(LIPIcs, Vol. 69)_ , Tarmo Uustalu (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 5:1–5:34.  https://doi.org/10.4230/LIPICS.TYPES.2015.5
  * Coquand (2018) Thierry Coquand. 2018\.  Presheaf model of type theory. (2018).  https://www.cse.chalmers.se/~coquand/presheaf.pdf.
  * Gratzer (2023) Daniel Gratzer. 2023\.  Normalization for multimodal type theory.  _CoRR_ abs/2301.11842 (2023).  https://doi.org/10.48550/arXiv.2301.11842 arXiv:2301.11842
  * Gratzer et al. (2021) Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021.  Multimodal Dependent Type Theory.  _Log. Methods Comput. Sci._ 17, 3 (2021).  https://doi.org/10.46298/lmcs-17(3:11)2021
  * Hofmann (1997) Martin Hofmann. 1997\.  Syntax and Semantics of Dependent Types. In _Semantics and Logics of Computation_. Cambridge University Press, 79–130.
  * Kaposi et al. (2019a) Ambrus Kaposi, Simon Huber, and Christian Sattler. 2019a.  Gluing for Type Theory. In _4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany_ _(LIPIcs, Vol. 131)_ , Herman Geuvers (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 25:1–25:19.  https://doi.org/10.4230/LIPIcs.FSCD.2019.25
  * Kaposi et al. (2019b) Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. 2019b.  Constructing quotient inductive-inductive types.  _Proc. ACM Program. Lang._ 3, POPL (2019), 2:1–2:24.  https://doi.org/10.1145/3290315
  * Kovács and Kaposi (2020) András Kovács and Ambrus Kaposi. 2020.  Large and Infinitary Quotient Inductive-Inductive Types. In _LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020_ , Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 648–661.  https://doi.org/10.1145/3373718.3394770
  * Kraus and Sattler (2017) Nicolai Kraus and Christian Sattler. 2017.  Space-Valued Diagrams, Type-Theoretically (Extended Abstract).  _CoRR_ abs/1704.04543 (2017).  arXiv:1704.04543 http://arxiv.org/abs/1704.04543
  * Muylder et al. (2024) Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. 2024\.  Internal and Observational Parametricity for Cubical Agda. In _To appear in: Proceedings of the 51st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2024, London, UK, January 17 - 19, 2024_. ACM.
  * Nuyts and Devriese (2018) Andreas Nuyts and Dominique Devriese. 2018.  Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. In _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018_ , Anuj Dawar and Erich Grädel (Eds.). ACM, 779–788.  https://doi.org/10.1145/3209108.3209119
  * Nuyts et al. (2017) Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017\.  Parametric quantifiers for dependent type theory.  _Proc. ACM Program. Lang._ 1, ICFP (2017), 32:1–32:29.  https://doi.org/10.1145/3110276
  * Reynolds (1983) John C. Reynolds. 1983\.  Types, Abstraction and Parametric Polymorphism. In _Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983_ , R. E. A. Mason (Ed.). North-Holland/IFIP, 513–523.
  * Sterling (2022) Jonathan Sterling. 2022\.  _First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory_.  Ph. D. Dissertation. Carnegie Mellon University, USA.  https://doi.org/10.1184/r1/19632681.v1
  * Uemura (2019) Taichi Uemura. 2019\.  A General Framework for the Semantics of Type Theory.  _CoRR_ abs/1904.04097 (2019).  arXiv:1904.04097 http://arxiv.org/abs/1904.04097
  * Vezzosi et al. (2021) Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2021\.  Cubical Agda: A dependently typed programming language with univalence and higher inductive types.  _J. Funct. Program._ 31 (2021), e8.  https://doi.org/10.1017/S0956796821000034
  * Wadler (1990) Philip Wadler. 1990\.  Recursive types for free! (1990).  https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt.