# Internal Category with Families in Presheaves

Jason Z. S. Hu
McGill University
<EMAIL_ADDRESS>
###### Abstract

In this note, we review a construction of category with families (CwF) in a
presheaf category. When the base category of a presheaf category is a CwF, we
internalize this CwF structure in the CwF of the presheaf category. This note
assumes working knowledge on category theory.

##  1 Category with Families

Category with families (CwF) [Dybjer, 1995] is a categorical structure to
model dependent type theories. Essentially it characterizes substitution
invariance of dependent type theories in a categorical language.

######  Definition 1.1.

A category $\mathcal{D}$ is a category with families if it has

  1. 1.

a terminal object $\top$ and $!$ is the unique morphism to $\top$,

  2. 2.

a functor $\texttt{Ty}:\mathcal{D}^{op}\Rightarrow\texttt{Set}$; given
$\Gamma,\Delta:\mathcal{D},A:\texttt{Ty}(\Gamma),\sigma:\Delta\Rightarrow\Gamma$,
then we write the functorial action of Ty as
$A\\{\sigma\\}:\texttt{Ty}(\Delta)$,

  3. 3.

given $\Gamma:\mathcal{D},A:\texttt{Ty}(\Gamma)$, a set
$\texttt{Tm}(\Gamma,A)$; given
$\Gamma,\Delta:\mathcal{D},A:\texttt{Ty}(\Gamma),\sigma:\Delta\Rightarrow\Gamma,M:\texttt{Tm}(\Gamma,A)$,
then $M\\{\sigma\\}:\texttt{Tm}(\Delta,A\\{\sigma\\})$,

  4. 4.

given $\Gamma:\mathcal{D},A:\texttt{Ty}(\Gamma)$, their context comprehension
$\Gamma.A\in D$,

  5. 5.

given $\Gamma:\mathcal{D},A:\texttt{Ty}(\Gamma)$, the projection morphism
$p_{A}:\Gamma.A\Rightarrow\Gamma$,

  6. 6.

given $\Gamma:\mathcal{D},A:\texttt{Ty}(\Gamma)$, the variable projection
$v_{A}:\texttt{Tm}(\Gamma.A,A\\{p_{A}\\})$, and

  7. 7.

given
$\Gamma,\Delta:\mathcal{D},A:\texttt{Ty}(\Gamma),\sigma:\Delta\Rightarrow\Gamma,M:\texttt{Tm}(\Delta,A\\{\sigma\\})$,
then a substitution extension
$\langle\sigma,M\rangle:\Delta\Rightarrow\Gamma.A$,

such that the following equations hold

  1. 1.

$p_{A}\circ\langle\sigma,M\rangle=\sigma$,

  2. 2.

$v_{A}\\{\langle\sigma,M\rangle\\}=M$, and

  3. 3.

for $\sigma:\Delta\Rightarrow\Gamma.A$, $\sigma=\langle
p_{A}\circ\sigma,v_{A}\\{\sigma\\}\rangle$.

Intuitively, CwFs are “substitution-oriented”. Objects in $\mathcal{D}$ model
contexts in type theories and morphisms model substitutions between the
contexts. Hence we need the terminal object to model the empty context.
$\texttt{Ty}(\Gamma)$ represents the set of semantic types in context $\Gamma$
and given $A:\texttt{Ty}(\Gamma)$, $\texttt{Tm}(\Gamma,A)$ is the set of
semantic terms of type $A$ in $\Gamma$. Comprehensions extend contexts. The
operations like projections and extensions are used to manipulate
substitutions. $v$ is sometimes called the second projection, which models
variables.

##  2 Presheaves as CwFs

[Hofmann, 1997] showed that any given presheaf category has a CwF structure.
Here we assume any given base category $\mathcal{D}$ and specify the
construction in details.

Conventionally, we refer to the presheaf category as $\widehat{\mathcal{D}}$.
Moreover, we put iterative applications in a single pair of parentheses,
namely

$\displaystyle f(x_{1},\cdots,x_{n}):=f(x_{1})\cdots(x_{n})$

###  2.1 Terminal Object

All presheaf category has a terminal object. This is defined via

$\displaystyle\top$ $\displaystyle:\mathcal{D}^{op}\Rightarrow\texttt{Set}$
$\displaystyle\top(d:\mathcal{D})$ $\displaystyle:=\\{*\\}$
$\displaystyle\top(\delta:\mathcal{D}(d,d^{\prime}))$
$\displaystyle:=*\mapsto*:\\{*\\}\to\\{*\\}$

The unique morphism into $\top$ is a natural transformation:

$\displaystyle!$ $\displaystyle:\texttt{Nat}(\Gamma,\top)$
$\displaystyle!(d:\mathcal{D})$ $\displaystyle:=s\mapsto*:\Gamma(d)\to\\{*\\}$

Since the codomain is $\\{*\\}$, we know that $!$ must be unique.

###  2.2 Types

Semantic types is modelled by the presheaf functor
$\texttt{Ty}:\widehat{\mathcal{D}}\Rightarrow\texttt{Set}$. Here the intension
is to define the codomain as the set presheaf over the category of elements,
as specified below.

######  Definition 2.1.

Given $\Gamma:\widehat{\mathcal{D}}$, the category of elements
$\smallint\Gamma$ has the following data:

  1. 1.

objects are $\Sigma(d:\mathcal{D})\Gamma(d)$,

  2. 2.

morphisms between
$(d:\mathcal{D},s:\Gamma(d))\Rightarrow(d^{\prime}:\mathcal{D},s^{\prime}:\Gamma(d^{\prime}))$
is a morphism $\delta:d\Rightarrow d^{\prime}$, such that
$\Gamma(\delta,s^{\prime})=s$. Set theoretically, we write

$\displaystyle(d:\mathcal{D},s:\Gamma(d))\Rightarrow(d^{\prime}:\mathcal{D},s^{\prime}:\Gamma(d^{\prime})):=\\{\delta:d\Rightarrow
d^{\prime}|\Gamma(\delta,s^{\prime})=s\\}$

  3. 3.

identities and compositions are inherited from $\mathcal{D}$. The well-
definedness of compositions follows from the functoriality of $\Gamma$.

Since identities and compositions are inherited from $\mathcal{D}$, the
categorical laws are also inherited from $\mathcal{D}$.

Here we employ some type theoretical notions to ease the discussion. We can
easily port the language to a more set theoretical one, if necessary.

Notice that, given $s^{\prime}:\Gamma(d^{\prime})$, we can extend
$\delta:\mathcal{D}(d,d^{\prime})$ to a morphism in $\smallint\Gamma$:
$\delta:(d,\Gamma(\sigma,s^{\prime}))\Rightarrow(d^{\prime},s^{\prime})$. This
observation will come in handy later.

We then move on to define Ty:

Ty $\displaystyle:\widehat{\mathcal{D}}\Rightarrow\texttt{Set}$
$\displaystyle\texttt{Ty}(\Gamma)$
$\displaystyle:=(\smallint\Gamma)^{op}\Rightarrow\texttt{Set}$
$\displaystyle\\_\\{\\_\\}$
$\displaystyle:\texttt{Ty}(\Gamma)\to\Delta\Rightarrow\Gamma\to\texttt{Ty}(\Delta)$
$\displaystyle A\\{\sigma\\}(d:\mathcal{D},s:\Delta(d))$
$\displaystyle:=A(d,\sigma(d,s))$ $\displaystyle
A\\{\sigma\\}(\delta:(d,s)\Rightarrow(d^{\prime},s^{\prime}))$
$\displaystyle:=A(\delta):A\\{\sigma\\}(d,s)\to
A\\{\sigma\\}(d^{\prime},s^{\prime})$

As mentioned in the definition of CwFs, we write $A\\{\sigma\\}$ for
$\texttt{Ty}(\sigma,A)$ so we have given both components of Ty. Now we need to
verify the well-definedness of this definition. First, we need to examine
$A\\{\sigma\\}(\delta)$ is well defined. It is well-defined only when $u$ and
$u^{\prime}$ in
$\delta:(d,u:\Gamma(d))\Rightarrow(d^{\prime},u^{\prime}:\Gamma(d^{\prime}))$
are clearly specified on the right hand side. This can be done by requiring

$\displaystyle u$ $\displaystyle:=\sigma(d,s)$ $\displaystyle u^{\prime}$
$\displaystyle:=\sigma(d^{\prime},s^{\prime})$

which also aligns with the object part of $A\\{\sigma\\}$. We also need to
prove $\Gamma(\delta,u^{\prime})=u$ knowing $\Delta(\delta,s^{\prime})=s$. We
analyze as follows:

$\displaystyle\Gamma(\delta,u^{\prime})$
$\displaystyle=\Gamma(\delta,\sigma(d^{\prime},s^{\prime}))$
$\displaystyle=\sigma(d,\Delta(\delta,s^{\prime}))$ by naturality of $\sigma$
$\displaystyle=\sigma(d,s)$ by the equation above $\displaystyle=u$

That concludes that $A\\{\sigma\\}$ is well defined.

Given both components of Ty, we then move on to examine the functorial laws of
Ty. Since the morphism part of $A\\{\sigma\\}$ directly inherits from $A$, we
only need to examine the object part. Consider the identity law

$\displaystyle A\\{id\\}(d,s)$ $\displaystyle=A(d,id(d,s))=A(d,s)$

Next we examine the composition law:

$\displaystyle A\\{\sigma\circ\sigma^{\prime}\\}(d,s)$
$\displaystyle=A(d,(\sigma\circ\sigma^{\prime})(d,s))$
$\displaystyle=A(d,\sigma(d,\sigma^{\prime}(d,s)))$ $\displaystyle
A\\{\sigma\\}\\{\sigma^{\prime}\\}(d,s)$
$\displaystyle=A\\{\sigma\\}(d,\sigma^{\prime}(d,s))$
$\displaystyle=A(d,\sigma(d,\sigma^{\prime}(d,s)))$

Thus they agree. At this point, we can conclude Ty is a presheaf.

###  2.3 Terms

Semantic terms are dependent objects which are indexed semantic contexts and
semantic types. We define the set of terms as follows:

$\displaystyle\texttt{Tm}(\Gamma,A):=\\{$ $\displaystyle
M:(o:\Sigma(d:\mathcal{D})\Gamma(d))\to A(o)$
$\displaystyle|\forall\delta:d^{\prime}\Rightarrow
d,s:\Gamma(d).A(\delta,M(d,s))=M(d^{\prime},\Gamma(\delta,s))\\}$

Now consider term substitutions. As typically done, we overload the notation
for type substitutions:

$\displaystyle\\_\\{\\_\\}$
$\displaystyle:\texttt{Tm}(\Gamma,A)\to(\sigma:\Delta\Rightarrow\Gamma)\to\texttt{Tm}(\Delta,A\\{\sigma\\})$
$\displaystyle M\\{\sigma\\}(d,s:\Delta(d))$
$\displaystyle:=M(d,\sigma(d,s):\Gamma(d))$

There are two things to verify for this definition. We need to show that the
right hand side is in the set $A\\{\sigma\\}(d,s)$ and that the set
specification holds. The first item holds by definition. Now we examine the
set specification.

The set specification requires that given $\delta:d^{\prime}\Rightarrow d$ and
$s:\Delta(d)$,
$A\\{\sigma\\}(\delta,M\\{\sigma\\}(d,s))=M\\{\sigma\\}(d^{\prime},\Delta(\delta,s))$
holds. Let us consider the left hand side:

$\displaystyle A\\{\sigma\\}(\delta,M\\{\sigma\\}(d,s))$
$\displaystyle=A\\{\sigma\\}(\delta,M(d,\sigma(d,s)))$ by definition of
$M\\{\sigma\\}$ $\displaystyle=A(\delta,M(d,\sigma(d,s)))$ by definition of
$A\\{\sigma\\}$ $\displaystyle=M(d^{\prime},\Gamma(\delta,\sigma(d,s)))$ by
$M$’s specification

Now we analyze the right hand side:

$\displaystyle M\\{\sigma\\}(d^{\prime},\Delta(\delta,s))$
$\displaystyle=M(d^{\prime},\sigma(d^{\prime},\Delta(\delta,s)))$ by
definition

Both sides would agree if
$\Gamma(\delta,\sigma(d,s))=\sigma(d^{\prime},\Delta(\delta,s))$, and this
holds due to the naturality of $\sigma$.

This concludes that $M\\{\sigma\\}$ is a well-defined semantic term.

###  2.4 Context Comprehension

Context comprehension models extension of context in the syntax. The operator
. joins a context $\Gamma$ and a type $A$, forming another context $\Gamma.A$.
Given $\Gamma:\widehat{\mathcal{D}}$ and $A:\texttt{Ty}(\Gamma)$, we need to
give $\Gamma.A:\widehat{\mathcal{D}}=\mathcal{D}^{op}\Rightarrow\texttt{Set}$.

$\displaystyle\Gamma.A$ $\displaystyle:\widehat{\mathcal{D}}$
$\displaystyle\Gamma.A(d\in\mathcal{D}^{op})$
$\displaystyle:=\Sigma(s:\Gamma(d))A(d,s)$
$\displaystyle\Gamma.A(\delta:\mathcal{D}^{op}(d,d^{\prime}))(s:\Gamma(d),a:A(d,s))$
$\displaystyle:=(\Gamma(\delta,s),A(\delta,a)):\Sigma(s^{\prime}:\Gamma(d^{\prime}))A(d^{\prime},s^{\prime})$

Now we examine the well-definedness of this presheaf. We need to ensure that
the morphism part is well defined, in particular the second component of the
result indeed resides in
$A(d^{\prime},s^{\prime})=A(d^{\prime},\Gamma(\delta,s))$.

Notice that $\delta:D^{op}(d,d^{\prime})=D(d^{\prime},d)$ and we are given
$s:\Gamma(d)$. Recall in the previous subsection, we discussed that $\delta$
can be extended to a morphism in $\smallint\Gamma$, so we know
$\delta:\smallint\Gamma((d^{\prime},\Gamma(\delta,s)),(d,s))$. Since $A$ is a
presheaf over $\smallint\Gamma$, then $A(\delta)$ is a set function $A(d,s)\to
A(d^{\prime},\Gamma(\delta,s))$. This justifies that $A(\delta,a)$ does reside
in $A(d^{\prime},\Gamma(\delta,s))$.

Now we examine the functorial laws. This is immediate because $\Gamma.A$
simply combines $\Gamma$ and $A$, and thus the functoriality is induced from
the functoriality of $\Gamma$ and $A$.

###  2.5 Projection

Given $\Gamma$ and $A:\texttt{Ty}(\Gamma)$, the projection morphism
$p_{A}:\Gamma.A\Rightarrow\Gamma$ models the weakening substitution. Since it
is a morphism between two presheaves, it is a natural transformation. Its
definition is easily given due to the definition of $\Gamma.A$:

$\displaystyle p_{A}$ $\displaystyle:\Gamma.A\Rightarrow\Gamma$ $\displaystyle
p_{A}(d)(s:\Gamma(d),\\_)$ $\displaystyle:=s$

This definition is obviously natural.

###  2.6 Variables

Given $\Gamma$ and $A:\texttt{Ty}(\Gamma)$,
$v_{A}:\texttt{Tm}(\Gamma.A,A\\{p_{A}\\})$ models the first variable in the
context. Combining the projection morphism, we can model any variables. In the
presheaf category, we can model this term as:

$\displaystyle v_{A}$ $\displaystyle:\texttt{Tm}(\Gamma.A,A\\{p_{A}\\})$
$\displaystyle v_{A}(d:\mathcal{D},(s:\Gamma(d),a:A(d,s)))$ $\displaystyle:=a$

Now we need to show that $a:A\\{p_{A}\\}(d,(s,a))$. We expand the set by
definition:

$\displaystyle A\\{p_{A}\\}(d,(s,a))$ $\displaystyle=A(d,p_{A}(s,a))=A(d,s)$

Next we shall examine that this definition complies with the set specification
given by Tm. Assuming $\delta:d^{\prime}\Rightarrow d$, $s:\Gamma(d)$ and
$a:A(d,s)$, we need that
$A\\{p_{A}\\}(\delta,v_{A}(d,(s,a)))=v_{a}(d^{\prime},\Gamma.A(\delta,(s,a)))$.
We analyze each side:

$\displaystyle A\\{p_{A}\\}(\delta,v_{A}(d,(s,a)))$
$\displaystyle=A\\{p_{A}\\}(\delta,a)$ by definition of $v_{A}$
$\displaystyle=A(\delta,a)$ by definition of $A\\{p_{A}\\}$ $\displaystyle
v_{a}(d^{\prime},\Gamma.A(\delta,(s,a)))$
$\displaystyle=v_{a}(d^{\prime},(\Gamma(\delta,s),A(\delta,a)))$ by definition
of $\Gamma.A$ $\displaystyle=A(\delta,a)$ by definition of $v_{A}$

Thus the specification is satisfied.

###  2.7 Substitution Extension

The last piece of data is the substitution extension. Given
$\sigma:\Delta\Rightarrow\Gamma$, $A:\texttt{Ty}(\Gamma)$ and
$M:\texttt{Tm}(\Delta,A\\{\sigma\\})$, we want to obtain
$\langle\sigma,M\rangle:\Delta\Rightarrow\Gamma.A$.

$\displaystyle\langle\sigma,M\rangle$
$\displaystyle:\Delta\Rightarrow\Gamma.A$
$\displaystyle\langle\sigma,M\rangle(d:\mathcal{D},s:\Delta(s))$
$\displaystyle:=(\sigma(d,s),M(d,s)):\Gamma.A(d)=\Sigma(s^{\prime}:\Gamma(d))A(d,s^{\prime})$

Next we shall see that $\langle\sigma,M\rangle$ is natural. This is to examine
that given $\delta:\mathcal{D}^{op}(d,d^{\prime})$ and $s:\Delta(d)$, we have
the equation
$\langle\sigma,M\rangle(d^{\prime},\Delta(\delta,s))=\Gamma.A(\delta,\langle\sigma,M\rangle(d,s))$.
We analyze both sides:

$\displaystyle\langle\sigma,M\rangle(d^{\prime},\Delta(\delta,s))$
$\displaystyle=(\sigma(d^{\prime},\Delta(\delta,s)),M(d^{\prime},\Delta(\delta,s)))$
by definition of $\langle\sigma,M\rangle$
$\displaystyle\Gamma.A(\delta,\langle\sigma,M\rangle(d,s))$
$\displaystyle=\Gamma.A(\delta,(\sigma(d,s),M(d,s)))$ by definition of
$\langle\sigma,M\rangle$
$\displaystyle=(\Gamma(\delta,\sigma(d,s)),A(\delta,M(d,s)))$ by definition of
$\Gamma.A$
$\displaystyle=(\sigma(d^{\prime},\Delta(\sigma,s)),A(\delta,M(d,s)))$ by
naturality of $\sigma$
$\displaystyle=(\sigma(d^{\prime},\Delta(\delta,s)),M(d^{\prime},\Delta(\delta,s)))$
by specification of $M$

Thus $\langle\sigma,M\rangle$ is natural.

###  2.8 Laws

The definition of CwFs also requires laws to hold. Next we examine each of
them. In the following discussion, we assume $\sigma:\Delta\Rightarrow\Gamma$,
$A:\texttt{Ty}(\Gamma)$ and $M:\texttt{Tm}(\Delta,A\\{\sigma\\})$.

$\displaystyle(p_{A}\circ\langle\sigma,M\rangle)(d,s)=p_{A}(\langle\sigma,M\rangle(d,s))=\sigma(d,s)$

Thus $p_{A}\circ\langle\sigma,M\rangle=\sigma$.

$\displaystyle v_{A}\\{\langle\sigma,M\rangle\\}(d,s)$
$\displaystyle=v_{A}(d,\langle\sigma,M\rangle(d,s))$ by definition of term
substitution $\displaystyle=M(d,s)$ by definition of $\langle\sigma,M\rangle$
and $v_{A}$

Thus $v_{A}\\{\langle\sigma,M\rangle\\}=M$.

Given $\sigma^{\prime}:\Delta\Rightarrow\Gamma.A$, we have

$\displaystyle\ \langle
p_{A}\circ\sigma^{\prime},v_{A}\\{\sigma^{\prime}\\}\rangle(d,s)$
$\displaystyle=$ $\displaystyle\
((p_{A}\circ\sigma^{\prime})(d,s),v_{A}\\{\sigma^{\prime}\\}(d,s))$ by
definition of substitution extension $\displaystyle=$ $\displaystyle\
(\pi_{1}(\sigma^{\prime}(d,s)),v_{A}\\{\sigma^{\prime}\\}(d,s))$ $\pi_{1}$ is
the first projection of a $\Sigma$ set $\displaystyle=$ $\displaystyle\
(\pi_{1}(\sigma^{\prime}(d,s)),\pi_{2}(\sigma^{\prime}(d,s)))$ by definition
of $v_{A}\\{\sigma^{\prime}\\}$ and $\pi_{2}$ is the second projection of a
$\Sigma$ $\displaystyle=$ $\displaystyle\ \sigma^{\prime}(d,s)$ extensionality
of $\Sigma$

This gives $\langle
p_{A}\circ\sigma^{\prime},v_{A}\\{\sigma^{\prime}\\}\rangle=\sigma^{\prime}$.

##  3 Internal CwFs

Let us consider the situation where the (small) base category $\mathcal{D}$ is
a CwF. To avoid confusions with notations, we employ the following
conventions:

| Contexts | Set of Types | Types | Set of Terms | Terms
---|---|---|---|---|---
Base $\mathcal{D}$ | $\Phi,\Psi$ | Ty | $S,T,U$ | Tm | $s,t,u$
Presheaves $\widehat{\mathcal{D}}$ | $\Gamma,\Delta$ | $\widehat{\texttt{Ty}}$ | $A,B$ | $\widehat{\texttt{Tm}}$ | $M,N$
Internal CwF in $\widehat{\mathcal{D}}$ | $\Phi,\Psi$ | Ty | $S,T,U$ | Tm | $s,t,u$

Before entering the discussion, we would like to fix the terminologies. There
are types and terms referring to those in three different contexts. We use
semantic types (resp. terms) for the types (resp. terms) in
$\widehat{\mathcal{D}}$. We refer to types (resp. terms) in the internal CwF
as internal types (resp. terms). When referring to those in $\mathcal{D}$, we
will explicitly call them types (resp. terms) in $\mathcal{D}$.

Our purpose in this section is to _internalize_ the CwF structure of
$\mathcal{D}$ in the presheaf category $\widehat{\mathcal{D}}$. We call this
internal structure the internal CwF. Now in the categorical part, there are
two CwF structures: the one of $\mathcal{D}$ and the one of
$\widehat{\mathcal{D}}$ specified in the previous section. Therefore,
following the convention, we use Ty and Tm to represent the semantic types and
terms in $\mathcal{D}$, respectively, and we put hats over and use
$\widehat{\texttt{Ty}}$ and $\widehat{\texttt{Tm}}$ for semantic types and
terms in $\widehat{\mathcal{D}}$, respectively. In the later part of the
section, we need to define the internalized version of CwF of $\mathcal{D}$,
the types and terms of which are represented by $\widehat{\texttt{Ty}}$ and
$\widehat{\texttt{Tm}}$.

To be more specific, by internalizing the CwF of $\mathcal{D}$, we mean to be
able to study the CwF inside of $\widehat{\mathcal{D}}$. That requires to
represent types and terms of $\mathcal{D}$ in $\widehat{\mathcal{D}}$.
Judgmentally, we should define semantic types and terms which can suitably
interpret the following judgments: * ⊢Ctx type

* Ψ: Ctx, Φ: Ctx ⊢Hom(Ψ, Φ) type

* Ψ: Ctx ⊢ Ty(Ψ)  type

* Ψ: Ctx, A : Ty(Ψ) ⊢ Tm(Ψ, A)  type

Now we construct suitable semantic types in $\widehat{\mathcal{D}}$ for
interpreting these syntactic types.

###  3.1 Internal Contexts

Now we define the internalized representation for objects in $\mathcal{D}$.

Ctx $\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top})$
$\displaystyle\texttt{Ctx}(\\_)$ $\displaystyle:=Obj(\mathcal{D})$
$\displaystyle\texttt{Ctx}(\delta)$ $\displaystyle:=\Psi\mapsto\Psi$

To actually show that this definition does represent the objects of
$\mathcal{D}$, we need to show that
$\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})\simeq Obj(\mathcal{D})$.

By definition,

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})=\\{$
$\displaystyle
M:(o:\Sigma(\Psi:\mathcal{D})\widehat{\top}(\Psi))\to\texttt{Ctx}(o)$
$\displaystyle|\forall\delta:\Phi\Rightarrow\Psi,s:\widehat{\top}(\Psi).\texttt{Ctx}(\delta,M(\Psi,s))=M(\Phi,\widehat{\top}(\delta,s))\\}$

After simplification, we have

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})=\\{$
$\displaystyle M:(o:\Sigma(\Psi:\mathcal{D})\\{*\\})\to Obj(\mathcal{D})$
$\displaystyle\forall\delta:\Phi\Rightarrow\Psi,s:\\{*\\}.M(\Psi,s)=M(\Phi,s)\\}$

That is, $M$ is invariant under different $\Psi$. Since we know $\mathcal{D}$
is a CwF, we know it must have a terminal object $\top$. Now we can show the
intended isomorphism:

$\displaystyle f$
$\displaystyle:\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})\to
Obj(\mathcal{D})$ $\displaystyle f(M)$ $\displaystyle:=M(\top,*)$
$\displaystyle g$
$\displaystyle:Obj(\mathcal{D})\to\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})$
$\displaystyle g(\Psi)(\\_)$ $\displaystyle:=\Psi$

Clearly, $f$ and $g$ do form an isomorphism and thus this representation of
Ctx is as intended.

We can generalize the construction in this subsection. Reviewing the reason
why $\widehat{\texttt{Tm}}(\widehat{\top},\texttt{Ctx})\simeq
Obj(\mathcal{D})$, we realize that if a $\widehat{\texttt{Ty}}$ is defined
without considering the first projection in the object part, then the
$\widehat{\texttt{Tm}}$ is automatically isomorphic to the specified set given
by $\widehat{\texttt{Ty}}$. Moreover, the morphism part then must be identity
function. We will also see this pattern in the following subsections.

###  3.2 Internal Hom

Since $\mathcal{D}$ is a CwF, the morphisms in it are substitutions. We can
also model this in $\widehat{\mathcal{D}}$.

Hom
$\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\})$
$\displaystyle\textsf{Hom}(\\_,(*,\Psi,\Phi))$
$\displaystyle:=\texttt{Hom}(\Psi,\Phi)$ $\displaystyle\textsf{Hom}(\delta)$
$\displaystyle:=\delta^{\prime}\mapsto\delta^{\prime}$

Here we have two notions of Homs and we distinguish them by fonts. Hom
represents the Hom-set in $\mathcal{D}$ while Hom is its internalization.
Again, here we will make use of the observation at the end of the last
subsection. Since the definition of the object part of Hom is independent of
the first projection, we know that its $\widehat{\texttt{Tm}}$ is
automatically isomorphic to $\texttt{Hom}(\Psi,\Phi)$. We can verify this
observation more formally.

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\},\textsf{Hom})=\\{$
$\displaystyle
M:(o:\Sigma(\Psi:\mathcal{D})(\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\}(\Psi)))\to\textsf{Hom}(o)$
$\displaystyle|$
$\displaystyle\forall\delta:\Phi\Rightarrow\Psi,s:\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\}(\Psi).$
$\displaystyle\textsf{Hom}(\delta,M(\Psi,s))=M(\Phi,\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\}(\delta,s))\\}$

Let us analyze the specification, the left hand side equals to $M(\Psi,s)$. By
definition of context comprehension, we know
$s=(*,\Psi^{\prime},\Phi^{\prime})$ for some $\Psi^{\prime}$ and
$\Phi^{\prime}$. The right hand side becomes

$\displaystyle\
M(\Phi,\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\}(\delta,s))$
$\displaystyle=$ $\displaystyle\
M(\Phi,\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\}(\delta,(*,\Psi^{\prime},\Phi^{\prime})))$
extensionality for $s$ $\displaystyle=$ $\displaystyle\
M(\Phi,(*,\Psi^{\prime},\Phi^{\prime}))$ functorial actions of
$\widehat{\top}$ and Ctx are identity $\displaystyle=$ $\displaystyle\
M(\Phi,s)$

That is, again, $M$ is invariant under different $\Psi$. That allows us to
conclude
$\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx}.\texttt{Ctx}\\{p_{\texttt{Ctx}}\\},\textsf{Hom})\simeq(\Psi,\Phi:\mathcal{D})\to\texttt{Hom}(\Psi,\Phi)$.

###  3.3 Internal Category

Before moving on, we shall see that the whole categorical structure of
$\mathcal{D}$ can be internalized in $\widehat{\mathcal{D}}$. That is to say
we should find semantic terms that can interpret the following judgments: * Ψ:
Ctx ⊢id_Ψ : Hom(Ψ, Ψ)

* Ψ: Ctx, Ψ’ : Ctx, Ψ”, Ctx, σ’ : Hom(Ψ’, Ψ”), σ: Hom(Ψ, Ψ’) ⊢σ’ ∘σ : Hom(Ψ, Ψ”)

These two terms correspond to the following terms (after expanding the
definitions of functorial actions):

$\displaystyle id$
$\displaystyle:\Sigma(\Phi:\mathcal{D})(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))\to\texttt{Hom}(\Psi,\Psi)$
$\displaystyle id(\\_,(*,\Psi))$ $\displaystyle:=id_{\Psi}$
$\displaystyle\circ$
$\displaystyle:\Sigma(\Phi:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))(\Psi^{\prime}:\mathcal{D}))(\Psi^{\prime\prime}:\mathcal{D}))$
$\displaystyle\ \
(\sigma^{\prime}:\texttt{Hom}(\Psi^{\prime},\Psi^{\prime\prime})))(\sigma:\texttt{Hom}(\Psi,\Psi^{\prime})))$
$\displaystyle\ \ \to\texttt{Hom}(\Psi,\Psi^{\prime\prime})$
$\displaystyle\circ(\\_,(*,\Psi,\Psi^{\prime},\Psi^{\prime\prime},\sigma^{\prime},\sigma))$
$\displaystyle:=\sigma^{\prime}\circ\sigma$

In above definitions, $id_{\Psi}$ and $\sigma^{\prime}\circ\sigma$ on the
right hand side are in $\mathcal{D}$. Based on this definition, we can see
that the categorical laws hold internally as well. These definitions are valid
semantic terms because they do not depend on the first projection, and by the
analysis above this already implies the validity of the definitions as terms.
In later constructions of semantic terms in this section, we always ignore the
first projection and thus they are always valid. For this reason, we will omit
the same explanation.

###  3.4 Internal Types

Next we internalize Ty to $\widehat{\mathcal{D}}$, which is represented by Ty.

Ty $\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top}.\texttt{Ctx})$
$\displaystyle\textsf{Ty}(\\_,(*,\Psi))$ $\displaystyle:=\texttt{Ty}(\Psi)$
$\displaystyle\textsf{Ty}(\delta)$ $\displaystyle:=S\mapsto S$

Similarly, we should also examine
$\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx},\textsf{Ty})$. By
definition

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx},\textsf{Ty})=\\{$
$\displaystyle
M:(o:\Sigma(\Psi:\mathcal{D})\widehat{\top}.\texttt{Ctx}(\Psi))\to\textsf{Ty}(o)$
$\displaystyle|\forall\delta:\Phi\Rightarrow\Psi,s:\widehat{\top}.\texttt{Ctx}(\Psi).\textsf{Ty}(\delta,M(\Psi,s))=M(\Phi,\widehat{\top}.\texttt{Ctx}(\delta,s))\\}$

Similarly, we can show that $M$ is invariant under different $\Psi$ and thus
we obtain the isomorphism
$\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx},\textsf{Ty})\simeq(\Psi:\mathcal{D})\to\texttt{Ty}(\Psi)$.

Next, we should show that substitution can also be internalized. We are
looking to internalize the following judgment:

$\displaystyle\inferrule*{}{\Psi:\texttt{Ctx},\Phi:\texttt{Ctx},T:\textsf{Ty}(\Phi),\sigma:\textsf{Hom}(\Psi,\Phi)\vdash
T\\{\sigma\\}:\textsf{Ty}(\Psi)}$

This correspond to defining the following function $M$:

$\displaystyle M$
$\displaystyle:\Sigma(\Psi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))(\Phi:\mathcal{D}))$
$\displaystyle\ \
(T:\texttt{Ty}(\Phi)))\texttt{Hom}(\Psi,\Phi))\to\texttt{Ty}(\Psi)$
$\displaystyle M(\\_,(*,\Psi,\Phi,T,\sigma))$ $\displaystyle:=T\\{\sigma\\}$

The substitution on the right hand side is given by the type substitution of
CwF of $\mathcal{D}$.

###  3.5 Internal Terms

In the same spirit, we can internalize Tm to $\widehat{\mathcal{D}}$:

Tm
$\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top}.\texttt{Ctx}.\textsf{Ty})$
$\displaystyle\textsf{Tm}(\\_,(*,\Psi,S))$
$\displaystyle:=\texttt{Tm}(\Psi,S)$ $\displaystyle\textsf{Tm}(\delta)$
$\displaystyle:=s\mapsto s$

Moreover, we can also show
$\widehat{\texttt{Tm}}(\widehat{\top}.\texttt{Ctx}.\textsf{Ty},\textsf{Tm})\simeq(\Psi:\mathcal{D})(S:\texttt{Ty}(\Psi))\to\texttt{Tm}(\Psi,S)$.

We can also formulate term substitutions. Our target is the following
judgment:

$\displaystyle\inferrule*{}{\Psi:\texttt{Ctx},\Phi:\texttt{Ctx},T:\textsf{Ty}(\Phi),t:\textsf{Tm}(\Phi,T),\sigma:\textsf{Hom}(\Psi,\Phi)\vdash
t\\{\sigma\\}:\textsf{Tm}(\Psi,A\\{\sigma\\})}$

We can define the corresponding semantic term $M$ as follows:

$\displaystyle M$
$\displaystyle:\Sigma(\Psi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))(\Phi:\mathcal{D}))$
$\displaystyle\ \
(T:\texttt{Ty}(\Phi)))(t:\texttt{Tm}(\Phi,T)))(\sigma:\texttt{Hom}(\Psi,\Phi)))$
$\displaystyle\ \ \to\texttt{Tm}(\Psi,T\\{\sigma\\})$ $\displaystyle
M(\\_,(*,\Psi,\Phi,T,t,\sigma))$ $\displaystyle:=t\\{\sigma\\}$

The substitution on the right hand side is given by the CwF structure in
$\mathcal{D}$.

###  3.6 Internal Context Comprehension

After finish internalizing all necessary components, we will show how to
internalize other operators. First let us consider context comprehension.
Syntactically, we look at internalizing the following judgment: * Ψ: Ctx, T :
Ty (Ψ) ⊢Ψ.T : Ctx That is, we need to find a term to represent $\Psi.T$ when
$\Psi$ and $T$ are given:

$\displaystyle M$
$\displaystyle:\Sigma(\Phi:\mathcal{D})(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))\texttt{Ty}(\Psi))\to\mathcal{D}$
$\displaystyle M(\\_,(*,\Psi,T))$ $\displaystyle:=\Psi.T$

where the comprehension on the right hand side is given by the CwF structure
of $\mathcal{D}$. This gives us the internal context comprehension.

###  3.7 Internal Projection

Next we show the existence of an internalized projection morphism. We consider
a term corresponding to the following judgment: * Ψ: Ctx, T : Ty(Ψ) ⊢p_T :
Hom(Ψ.T, Ψ) We define the following term $p$:

$\displaystyle p$
$\displaystyle:\Sigma(\Phi:\mathcal{D})(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))\texttt{Ty}(\Psi))\to\texttt{Hom}(\Psi.A,\Psi)$
$\displaystyle p(\\_,(*,\Psi,T))$ $\displaystyle:=p_{T}$

$p_{T}$ on the right hand side is given by the CwF of $\mathcal{D}$ as before.

###  3.8 Internal Variables

We consider the internalized version of variable projection: * Ψ: Ctx, T :
Ty(Ψ) ⊢v_T : Tm(Ψ.T, T{p_T}) We define the following term $v$:

$\displaystyle v$
$\displaystyle:\Sigma(\Phi:\mathcal{D})(\Sigma(\Sigma(s:\\{*\\})(\Psi:\mathcal{D}))\texttt{Ty}(\Psi))\to\texttt{Tm}(\Gamma.T,T\\{p_{T}\\})$
$\displaystyle v(\\_,(*,\Psi,T))$ $\displaystyle:=v_{T}$

That is, $v$ is defined in terms of $v_{T}$ of $\mathcal{D}$.

###  3.9 Internal Substitution Extension

Next we consider internalized substitution extensions: * Φ: Ctx, Ψ: Ctx, T :
Ty(Ψ) , σ: Hom(Φ, Ψ), t : Tm(Φ, T{σ}) ⊢⟨σ, t ⟩ : Hom(Φ, Ψ.T)

We define the following term:

$\displaystyle M$
$\displaystyle:\Sigma(\Phi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(\Sigma(s:\\{*\\})(\Phi:\mathcal{D}))(\Psi:\mathcal{D}))$
$\displaystyle\ \
(T:\texttt{Ty}(\Phi)))(\sigma:\texttt{Hom}(\Psi,\Phi)))(t:\texttt{Tm}(\Phi,T\\{\sigma\\})))$
$\displaystyle\ \ \to\texttt{Hom}(\Phi,\Psi.T)$ $\displaystyle
M(\\_,(*,\Phi,\Psi,T,\sigma,t))$ $\displaystyle:=\langle\sigma,t\rangle$

Here the right hand side is given by $\mathcal{D}$.

###  3.10 Programming $\mathcal{D}$ in $\widehat{\mathcal{D}}$

Previously, we have given the internalized version of the CwF structure of
$\mathcal{D}$ in as types and terms in $\widehat{\mathcal{D}}$. A natural
consequence of the construction above is that we can reason about
$\mathcal{D}$ within $\widehat{\mathcal{D}}$ completely internally and that
the result of reasoning is totally faithful.

Consider a special morphism in any CwF structure. Given
$\sigma:\textsf{Hom}(\Phi,\Psi)$ and $T:\textsf{Ty}(\Psi)$, we can define a
morphism $q(\sigma,T)$ by

$\displaystyle q(\sigma,T)$
$\displaystyle:\textsf{Hom}(\Phi.T\\{\sigma\\},\Phi.T)$ $\displaystyle
q(\sigma,T)$ $\displaystyle:=\langle\sigma\circ
p_{T\\{\sigma\\}},v_{T\\{\sigma\\}}\rangle$

If we assume that this definition is given in a syntactic type theory of
$\widehat{\mathcal{D}}$ which complies with the judgments and the
interpretations listed above, then by interpreting this definition, we
effectively obtain the following semantic term $M$ after expanding all
definitions:

$\displaystyle M$
$\displaystyle:\Sigma(\Phi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(s:\\{*\\})(\Phi:\mathcal{D}))(\Psi:\mathcal{D}))$
$\displaystyle\ \
(\sigma:\texttt{Hom}(\Phi,\Psi)))(T:\texttt{Ty}(\Psi)))\to\texttt{Hom}(\Phi.T\\{\sigma\\},\Psi.T)$
$\displaystyle M(\\_,(*,\Phi,\Psi,\sigma,T))$
$\displaystyle=\langle\sigma\circ p_{T\\{\sigma\\}},v_{T\\{\sigma\\}}\rangle$

Here the right hand side lives in $\mathcal{D}$. That is, the definition in a
syntactic form of $\widehat{\mathcal{D}}$ is reflected as is in the semantics
in $\mathcal{D}$.

##  4 $\Pi$ Types in Presheaves

In this section, let us consider another typical type former, $\Pi$ types. As
indicated by its name, $\Pi$ types model dependent function space of dependent
type theory. Again, each presheaf category has $\Pi$ types and we will review
this fact in this section.

###  4.1 Definition

$\Pi$ types are an additional structure over a CwF.

######  Definition 4.1.

A CwF $\mathcal{D}$ has $\Pi$ types if it has the following data:

  1. 1.

Given $A:\texttt{Ty}(\Gamma)$ and $\texttt{Ty}(\Gamma.A)$,
$\Pi(A,B):\texttt{Ty}(\Gamma)$,

  2. 2.

Given $M:\texttt{Tm}(\Gamma.A,B)$, $\Lambda(M):\texttt{Tm}(\Gamma,\Pi(A,B))$,

  3. 3.

Given $M:\texttt{Tm}(\Gamma,\Pi(A,B))$ and $N:\texttt{Tm}(\Gamma,A)$,
$\texttt{App}(M,N):\texttt{Tm}(\Gamma,B\\{id_{\Gamma},N\\})$,

such that given $\sigma:\Delta\Rightarrow\Gamma$, the following laws hold:

  1. 1.

$\Pi(A,B)\\{\sigma\\}=\Pi(A\\{\sigma\\},B\\{q(\sigma,A)\\})$,

  2. 2.

Given $M:\texttt{Tm}(\Gamma.A,B)$,
$\Lambda(M)\\{\sigma\\}=\Lambda(M\\{q(\sigma,A)\\})$,

  3. 3.

Given $M:\texttt{Tm}(\Gamma,\Pi(A,B))$ and $N:\texttt{Tm}(\Gamma,A)$,
$\texttt{App}(M,N)\\{\sigma\\}=\texttt{App}(M\\{\sigma\\},N\\{\sigma\\})$,

  4. 4.

Given $M:\texttt{Tm}(\Gamma.A,B)$ and $N:\texttt{Tm}(\Gamma,A)$,
$\texttt{App}(\Lambda(M),N)=M\\{\langle id_{\Gamma},N\rangle\\}$.

This definition models the invariance of types and terms of $\Pi$ under
substitutions as well as $\beta$ equivalence.

###  4.2 An Incorrect Construction in Presheaves

Given the definition of $\Pi$ types in a CwF, we are interested in revising
the constructions in Section 2. Before considering a correct construction, let
us first check an incorrect construction and understand why we need a slightly
more complex definition.

We can get a first intuition by looking at how to derive from
$M:\widehat{\texttt{Tm}}(\Gamma.A,B)$
$\widehat{\Lambda}(M):\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$. We
put hats on top of $\Pi$ and $\Lambda$ to indicate that the $\Pi$ types are
constructed in $\widehat{\mathcal{D}}$.

$\displaystyle\widehat{\texttt{Tm}}(\Gamma.A,B)=\\{$ $\displaystyle
M:(o:\Sigma(\Psi:\mathcal{D})(\Sigma(s:\Gamma(\Psi))A(\Psi,s)))\to B(o)$
$\displaystyle|$ $\displaystyle\
\forall\delta:\Phi\Rightarrow\Psi,s:\Gamma(\Psi),a:A(\Psi,s).$ $\displaystyle
B(\delta,M(\Psi,(s,a)))=M(\Phi,(\Gamma(\delta,s),A(\delta,a)))\\}$

For an overly simple-minded assumption, if $\widehat{\Lambda}(M)$ corresponds
to currying, it might be the following function:

$\displaystyle(o:\Sigma(\Psi:\mathcal{D})(s:\Gamma(\Psi)))\to((a:A(\Psi,s))\to
B(\Psi,s,a))$

This suggests the following formulation of $\widehat{\Pi}$ types:

$\displaystyle\widehat{\Pi}(A,B)$
$\displaystyle:(\smallint\Gamma)^{op}\Rightarrow\texttt{Set}$
$\displaystyle\widehat{\Pi}(A,B)(\Psi,s)$ $\displaystyle:=(a:A(\Psi,s))\to
B(\Psi,s,a)$

However, this formulation is problematic because $(\Psi,s)$ occurs both in
covariant and contravariant position, and therefore we are not able to define
the morphism part of this functor. The solution to this problem turns out to
be very similar to Kripke model constructions of programming languages: if we
view $\mathcal{D}$ as some sort of Kripke structure, then we can generalize
the object part to a function space which is coherent under this Kripke
relation, which is shown in the next subsection.

###  4.3 A Correct Construction

####  4.3.1 Definition of $\widehat{\Pi}$

As shown in the previous subsection, the definition of $\widehat{\Pi}(A,B)$
must be covariant in both $A$ and $B$. This can be achieved by defining a
function space which has coherence property w.r.t. $\mathcal{D}$-morphisms.

$\displaystyle\widehat{\Pi}(A,B)$
$:(\smallint\Gamma)^{op}\Rightarrow\texttt{Set}$
$\displaystyle\widehat{\Pi}(A,B)(\Psi,s)$ $\displaystyle:=\\{$ $\displaystyle
f:(\Phi:\mathcal{D})(\delta:\mathcal{D}^{op}(\Psi,\Phi))(a:A(\Phi,\Gamma(\delta,s)))\to
B(\Phi,(\Gamma(\delta,s),a))$ $\displaystyle\ |\ P(A,B,\Psi,s,f)\\}$

Here $P$ is a predicate over the function space, ensuring coherence of $f$.
This coherence condition is required in demonstrating right to left effect of
the isomorphism
$\widehat{\texttt{Tm}}(\Gamma.A,B)\simeq\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$
below. Intuitively, it means $f$ is “natural”: if the argument moves along the
Kripke relation, then the result also moves along the Kripke relation.

$\displaystyle P(A,B,\Psi,s,f):=$ $\displaystyle\
\forall\Phi:\mathcal{D},\delta:\mathcal{D}^{op}(\Psi,\Phi),a:A(\Phi,\Gamma(\delta,s)),\Phi^{\prime}:\mathcal{D},\delta^{\prime}:\mathcal{D}^{op}(\Phi,\Phi^{\prime}).$
$\displaystyle\
f(\Phi^{\prime},\delta^{\prime}\circ\delta,A(\delta^{\prime},a))=B(\delta^{\prime},f(\Phi,\delta,a))$

We examine the well-definedness of this predicate. $\delta^{\prime}$ induces a
morphism in $(\smallint\Gamma)^{op}$:
$(\smallint\Gamma)^{op}((\Phi,\Gamma(\delta,s)),(\Phi^{\prime},\Gamma(\delta^{\prime}\circ\delta,s)))$.
Therefore this gives

$\displaystyle A(\delta^{\prime},a)$
$\displaystyle:A(\Phi^{\prime},\Gamma(\delta^{\prime}\circ\delta,s))$
$\displaystyle
f(\Phi^{\prime},\delta^{\prime}\circ\delta,A(\delta^{\prime},a))$
$\displaystyle:B(\Phi^{\prime},\Gamma(\delta^{\prime}\circ\delta,s),A(\delta^{\prime},a))$

On the right hand side, $\delta^{\prime}$ induces a morphism in
$(\smallint(\Gamma.A))^{op}$, from which we have the following analysis:

$\displaystyle\delta^{\prime}$
$\displaystyle:(\smallint(\Gamma.A))^{op}((\Phi,\Gamma(\delta,s),a),(\Phi^{\prime},\Gamma(\delta^{\prime},\Gamma(\delta,s)),A(\delta^{\prime},a)))$
$\displaystyle f(\Phi,\delta,a)$ $\displaystyle:B(\Phi,(\Gamma(\delta,s),a))$
$\displaystyle B(\delta^{\prime},f(\Phi,\delta,a))$
$\displaystyle:B(\Phi^{\prime},\Gamma(\delta^{\prime},\Gamma(\delta,s)),A(\delta^{\prime},a))$

Thus $P$ is well-defined.

Now we define the morphism part:

$\displaystyle\widehat{\Pi}(A,B)$
$\displaystyle(\delta:(\smallint\Gamma)^{op}((\Psi,s),(\Psi^{\prime},\Gamma(\delta,s))))$
$\displaystyle(f:(\Phi:\mathcal{D})(\delta:\mathcal{D}^{op}(\Psi,\Phi))(a:A(\Phi,\Gamma(\delta,s)))\to
B(\Phi,(\Gamma(\delta,s),a)))$
$\displaystyle(\Phi,\delta^{\prime}:\mathcal{D}^{op}(\Psi^{\prime},\Phi),a:A(\Phi,\Gamma(\delta^{\prime},\Gamma(\delta,s))))$
$\displaystyle:=$ $\displaystyle\
f(\Phi,\delta^{\prime}\circ\delta,a):B(\Phi,(\Gamma(\delta^{\prime},\Gamma(\delta,s)),a))$

Notice that
$\Gamma(\delta^{\prime}\circ\delta,s)=\Gamma(\delta^{\prime},\Gamma(\delta,s))$
due to compositionality of $\Gamma$. Since $\widehat{\Pi}(A,B)(\delta,f)$ is
defined in terms of $f$,
$P(A,B,\Psi^{\prime},\Gamma(\delta,s),\widehat{\Pi}(A,B)(\delta,f))$ is
inherited from $P(A,B,\Psi,s,f)$. Thus the morphism part of
$\widehat{\Pi}(A,B)$ is well-defined.

####  4.3.2 Definition of $\widehat{\Lambda}$

Now let us define $\widehat{\Lambda}(M)$ for
$M:\widehat{\texttt{Tm}}(\Gamma.A,B)$, the expansion of which is given in the
last subsection. Now we define
$\widehat{\Lambda}(M):\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$:

$\displaystyle\widehat{\Lambda}(M)$
$\displaystyle:\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$
$\displaystyle\widehat{\Lambda}(M)(\Psi,s)(\Phi,\delta:\mathcal{D}^{op}(\Psi,\Phi),a:A(\Phi,\Gamma(\delta,s)))$
$\displaystyle:=M(\Phi,(\Gamma(\delta,s),a))$

Let us verify $P(A,B,\Psi,s,\widehat{\Lambda}(M)(\Psi,s))$. Given
$\Phi^{\prime},\delta^{\prime}:\mathcal{D}^{op}(\Phi,\Phi^{\prime})$, we
should prove

$\displaystyle
M(\Phi^{\prime},(\Gamma(\delta^{\prime}\circ\delta,s),A(\delta^{\prime},a)))=B(\delta^{\prime},M(\Phi,(\Gamma(\delta,s),a)))$

This equation is directly proven by the specification of $M$.

Let us verify the set specification for $\widehat{\Lambda}(M)$. It is required
that the following equation holds given any
$\delta^{\prime}:\Psi^{\prime}\Rightarrow\Psi,s:\Gamma(\Psi)$:

$\displaystyle\widehat{\Pi}(A,B)(\delta^{\prime},\widehat{\Lambda}(M)(\Psi,s))=\widehat{\Lambda}(M)(\Psi^{\prime},\Gamma(\delta^{\prime},s))$

We fully apply both sides:

$\displaystyle\widehat{\Pi}(A,B)(\delta^{\prime},\widehat{\Lambda}(M)(\Psi,s))(\Phi,\delta,a)=\widehat{\Lambda}(M)(\Psi^{\prime},\Gamma(\delta^{\prime},s))(\Phi,\delta,a)$

We analyze the left hand side:

$\displaystyle\widehat{\Pi}(A,B)(\delta^{\prime},\widehat{\Lambda}(M)(\Psi,s))(\Phi,\delta,a)$
$\displaystyle=$ $\displaystyle\
\widehat{\Lambda}(M)(\Psi,s)(\Phi,\delta\circ\delta^{\prime},a)$ by morphism
part of $\widehat{\Pi}(A,B)$ $\displaystyle=$ $\displaystyle\
M(\Phi,(\Gamma(\delta\circ\delta^{\prime},s),a))$ by definition of
$\widehat{\Lambda}(M)$

Then the right hand side:

$\displaystyle\widehat{\Lambda}(M)(\Psi^{\prime},\Gamma(\delta^{\prime},s))(\Phi,\delta,a)$
$\displaystyle=$ $\displaystyle\
M(\Phi,(\Gamma(\delta,\Gamma(\delta^{\prime},s)),a))$ by definition of
$\widehat{\Lambda}(M)$ $\displaystyle=$ $\displaystyle
M(\Phi,(\Gamma(\delta\circ\delta^{\prime},s),a))$ by functoriality of $\Gamma$

We have shown that $\widehat{\Lambda}(M)$ does reside in set
$\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$.

####  4.3.3
$\widehat{\texttt{Tm}}(\Gamma.A,B)\simeq\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$

Next, we show that $\widehat{\texttt{Tm}}(\Gamma.A,B)$ and
$\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$ are isomorphic. We have
obtained the left to right directly via $\widehat{\Lambda}$. Now let us
consider the other direction $\widehat{\Lambda^{-1}}$.

Assuming $M^{\prime}:\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$, we
have

$\displaystyle\widehat{\Lambda^{-1}}(M^{\prime})$
$\displaystyle:\widehat{\texttt{Tm}}(\Gamma.A,B)$
$\displaystyle\widehat{\Lambda^{-1}}(M^{\prime})(\Psi,(s,a))$
$\displaystyle:=M^{\prime}(\Psi,s)(\Psi,id_{\Psi},a)$

The specification requires that given any
$\delta:\mathcal{D}^{op}(\Psi,\Psi^{\prime}),s:\Gamma(\Psi),a:A(\Psi,s)$:

$\displaystyle
B(\delta,\widehat{\Lambda^{-1}}(M^{\prime})(\Psi,(s,a)))=\widehat{\Lambda^{-1}}(M^{\prime})(\Psi^{\prime},\Gamma.A(\delta,(s,a)))$

We expand this equation and get:

$\displaystyle
B(\delta,M^{\prime}(\Psi,s)(\Psi,id_{\Psi},a))=M^{\prime}(\Psi^{\prime},\Gamma(\delta,s))(\Psi^{\prime},id_{\Psi^{\prime}},A(\delta,a))$

We analyze the left hand side:

$\displaystyle\ B(\delta,M^{\prime}(\Psi,s)(\Psi,id_{\Psi},a))$
$\displaystyle=$ $\displaystyle\ M^{\prime}(\Psi,s)(\Psi^{\prime},\delta\circ
id_{\Psi},A(\delta,a))$ $M^{\prime}(\Psi,s)$ satisfies $P$ $\displaystyle=$
$\displaystyle\
M^{\prime}(\Psi^{\prime},\Gamma(\delta,s))(\Psi^{\prime},id_{\Psi^{\prime}},A(\delta,a))$
by specification of $M^{\prime}$

This concludes $\widehat{\Lambda^{-1}}(M^{\prime})$ is well defined.

Now we proceed to proving that $\widehat{\Lambda}$ and
$\widehat{\Lambda^{-1}}$ do form the effects of the isomorphism
$\widehat{\texttt{Tm}}(\Gamma.A,B)\simeq\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$.

Given $M:\widehat{\texttt{Tm}}(\Gamma.A,B)$,

$\displaystyle\widehat{\Lambda^{-1}}(\widehat{\Lambda}(M))(\Psi,(s,a))$
$\displaystyle=\widehat{\Lambda}(M)(\Psi,s)(\Psi,id_{\Psi},a)$ by definition
of $\widehat{\Lambda^{-1}}$ $\displaystyle=M(\Psi,(s,a))$ by definition of
$\widehat{\Lambda}$

Given $M^{\prime}:\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$,

$\displaystyle\widehat{\Lambda}(\widehat{\Lambda^{-1}}(M^{\prime}))(\Psi,s)(\Phi,\delta,a)$
$\displaystyle=\widehat{\Lambda^{-1}}(M^{\prime})(\Phi,(\Gamma(\delta,s),a))$
by definition of $\widehat{\Lambda}$
$\displaystyle=M^{\prime}(\Phi,\Gamma(\delta,s))(\Phi,id_{\Phi},a)$ by
definition of $\widehat{\Lambda^{-1}}$
$\displaystyle=M^{\prime}(\Psi,s)(\Phi,\delta,a)$ by specification of
$M^{\prime}$

We conclude the intended isomorphism.

####  4.3.4 Definition of $\widehat{\texttt{App}}$

Finally we define the semantic applications. Given
$M:\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$ and
$N:\widehat{\texttt{Tm}}(\Gamma,A)$ we define

$\displaystyle\widehat{\texttt{App}}(M,N)$
$\displaystyle:\widehat{\texttt{Tm}}(\Gamma,B\\{\langle
id_{\Gamma},N\rangle\\})$ $\displaystyle\widehat{\texttt{App}}(M,N)$
$\displaystyle:=\widehat{\Lambda^{-1}}(M)\\{\langle id_{\Gamma},N\rangle\\}$

###  4.4 Laws

We have got all the definitions. The next step is to verify that the
definitions satisfy the laws. We verify the laws in the order as given in
Section 4.1. We assume a substitution morphism
$\sigma:\Delta\Rightarrow\Gamma$ when necessary.

  1. 1.

We shall show the following equation of substitution of $\widehat{\Pi}$ types:

$\displaystyle\widehat{\Pi}(A,B)\\{\sigma\\}=\widehat{\Pi}(A\\{\sigma\\},B\\{q(\sigma,A)\\})$

We expand the left hand side:

$\displaystyle\ \widehat{\Pi}(A,B)\\{\sigma\\}(\Psi,s)$ $\displaystyle=$
$\displaystyle\ \widehat{\Pi}(A,B)(\Psi,\sigma(\Psi,s))$ by definition of type
substitutions $\displaystyle=$ $\displaystyle\
\\{f:(\Phi:\mathcal{D})(\delta:\mathcal{D}^{op}(\Psi,\Phi))(a:A(\Phi,\Gamma(\delta,\sigma(\Psi,s))))$
$\displaystyle\ \ \to B(\Phi,(\Gamma(\delta,\sigma(\Psi,s)),a))\ |\
P(A,B,\Psi,\sigma(\Psi,s),f)\\}$

By naturality of $\sigma$, we have
$\Gamma(\delta,\sigma(\Psi,s))=\sigma(\Phi,\Delta(\delta,s))$. Thus

$\displaystyle\ \widehat{\Pi}(A,B)\\{\sigma\\}(\Psi,s)$ $\displaystyle=$
$\displaystyle\
\\{f:(\Phi:\mathcal{D})(\delta:\mathcal{D}^{op}(\Psi,\Phi))(a:A(\Phi,\sigma(\Phi,\Delta(\delta,s))))$
$\displaystyle\ \ \to B(\Phi,(\sigma(\Phi,\Delta(\delta,s)),a))\ |\
P(A,B,\Psi,\sigma(\Psi,s),f)\\}$ $\displaystyle=$ $\displaystyle\
\\{f:(\Phi:\mathcal{D})(\delta:\mathcal{D}^{op}(\Psi,\Phi))(a:A\\{\sigma\\}(\Phi,\Delta(\delta,s)))$
$\displaystyle\ \ \to B\\{q(\sigma,A)\\}(\Phi,(\Delta(\delta,s),a))\ |\
P(A,B,\Psi,\sigma(\Psi,s),f)\\}$

The function signature matches up. We just need to show that
$P(A,B,\Psi,\sigma(\Psi,s),f)$ and
$P(A\\{\sigma\\},B\\{q(\sigma,A)\\},\Psi,s,f)$ are equivalent. We can see that
these two propositions are essentially the same. This is because

    1. (a)

Naturality of $\sigma$ leads to
$A(\Phi,\Gamma(\delta,\sigma(\Psi,s)))=A(\Phi,\sigma(\Phi,\Delta(\delta,s)))$
and thus the arguments of $a$ in both propositions are the same;

    2. (b)

$B\\{\sigma\\}(\delta^{\prime})=B(\delta^{\prime})$ by definition.

Now we conclude the target equation.

  2. 2.

For $M:\widehat{\texttt{Tm}}(\Gamma.A,B)$, we should prove
$\widehat{\Lambda}(M)\\{\sigma\\}=\widehat{\Lambda}(M\\{q(\sigma,A)\\})$. We
fully apply and expand both sides:

$\displaystyle\ \widehat{\Lambda}(M)\\{\sigma\\}(\Psi,s)(\Phi,\delta,a)$
$\displaystyle=$ $\displaystyle\
\widehat{\Lambda}(M)(\Psi,\sigma(\Psi,s))(\Phi,\delta,a)$ by definition of
term substitutions $\displaystyle=$ $\displaystyle\
M(\Phi,(\Gamma(\delta,\sigma(\Psi,s)),a))$ by definition of
$\widehat{\Lambda}$ $\displaystyle\
\widehat{\Lambda}(M\\{q(\sigma,A)\\})(\Psi,s)(\Phi,\delta,a)$ $\displaystyle=$
$\displaystyle\ M\\{q(\sigma,A)\\}(\Phi,(\Gamma(\delta,s),a))$ by definition
of $\widehat{\Lambda}$ $\displaystyle=$ $\displaystyle\
M(\Phi,(\Gamma(\delta,\sigma(\Psi,s)),a))$ by definition of term substitutions

Thus the target equation holds.

  3. 3.

For $M:\texttt{Tm}(\Gamma,\Pi(A,B))$ and $N:\texttt{Tm}(\Gamma,A)$,
$\texttt{App}(M,N)\\{\sigma\\}=\texttt{App}(M\\{\sigma\\},N\\{\sigma\\})$. We
extend both sides:

$\displaystyle\ \texttt{App}(M,N)\\{\sigma\\}$ $\displaystyle=$
$\displaystyle\ \widehat{\Lambda^{-1}}(M)\\{\langle
id_{\Gamma},N\rangle\\}\\{\sigma\\}$ by definition of App $\displaystyle=$
$\displaystyle\
\widehat{\Lambda^{-1}}(M)\\{\langle\sigma,N\\{\sigma\\}\rangle\\}$ property of
substitution extension
$\displaystyle\texttt{App}(M\\{\sigma\\},N\\{\sigma\\})=\widehat{\Lambda^{-1}}(M\\{\sigma\\})\\{\langle
id_{\Delta},N\\{\sigma\\}\rangle\\}$ by definition of App

We prove a more general statement in order to conclude the target equation.
Given $\sigma^{\prime}:\Delta\Rightarrow\Gamma$ and
$N^{\prime}:\widehat{\texttt{Tm}}(\Delta,A\\{\sigma\\})$, the following
equation holds:

$\displaystyle\widehat{\Lambda^{-1}}(M)\\{\langle\sigma,N^{\prime}\rangle\\}=\widehat{\Lambda^{-1}}(M\\{\sigma\\})\\{\langle
id_{\Delta},N^{\prime}\rangle\\}$

We fully apply and expand both sides:

$\displaystyle\
\widehat{\Lambda^{-1}}(M)\\{\langle\sigma,N^{\prime}\rangle\\}(\Psi,(s,a))$
$\displaystyle=$ $\displaystyle\
\widehat{\Lambda^{-1}}(M)(\Psi,(\sigma(\Psi,s),N^{\prime}(\Psi,a)))$ by term
substitution and substitution extension $\displaystyle=$ $\displaystyle\
M(\Psi,\sigma(\Psi,s))(\Psi,id_{\Psi},N^{\prime}(\Psi,a))$ by definition of
$\widehat{\Lambda^{-1}}$ $\displaystyle\
\widehat{\Lambda^{-1}}(M\\{\sigma\\})\\{\langle
id_{\Delta},N^{\prime}\rangle\\}(\Psi,(s,a))$ $\displaystyle=$ $\displaystyle\
\widehat{\Lambda^{-1}}(M\\{\sigma\\})(\Psi,(s,N^{\prime}(\Psi,a)))$ by term
substitution and substitution extension $\displaystyle=$ $\displaystyle\
M\\{\sigma\\}(\Psi,s)(\Psi,id_{\Psi},N^{\prime}(\Psi,a))$ by definition of
$\widehat{\Lambda^{-1}}$ $\displaystyle=$ $\displaystyle\
M(\Psi,\sigma(\Psi,s))(\Psi,id_{\Psi},N^{\prime}(\Psi,a))$ by term
substitution

That concludes the statement and thus the target equation.

  4. 4.

$\widehat{\texttt{App}}(\widehat{\Lambda}(M),N)=M\\{\langle id,N\rangle\\}$
holds automatically due to the isomorphism
$\widehat{\texttt{Tm}}(\Gamma.A,B)\simeq\widehat{\texttt{Tm}}(\Gamma,\widehat{\Pi}(A,B))$.

###  4.5 Internal $\Pi$ Types

In this section we consider internalizing $\Pi$ types. In the previous
section, we showed that all presheaf categories have CwF structures equipped
with $\widehat{\Pi}$ types. Continuing the discussion in Section 3, by
assuming $\Pi$ types in $\mathcal{D}$, we can also internalize $\Pi$ types and
related terms in $\widehat{\mathcal{D}}$ as well. Internalization implies
providing interpretation for the following judgments: * Ψ: Ctx, S : Ty(Ψ) , T
: Ty(Ψ.S) ⊢Π(S, T) : Ty(Ψ)

* Ψ: Ctx, S : Ty(Ψ) , T : Ty(Ψ.S) , t : Tm(Ψ.S, T) ⊢Λ(t) : Tm(Ψ, Π(S, T))

* Ψ: Ctx, S : Ty(Ψ) , T : Ty(Ψ.S) , t : Tm(Ψ, Π(S, T)) , s : Tm(Ψ, S) ⊢App(t, s) : Tm(Ψ, T{⟨id_Ψ, s ⟩})

All these judgments correspond to semantic terms in $\widehat{\mathcal{D}}$ of
the matching types. We define the terms in the style given in Section 3. Let
us first define the term $M$ for $\Pi$:

$\displaystyle M$
$\displaystyle:\Sigma(\Psi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\\_:\\{*\\})(\Psi:\mathcal{D}))$
$\displaystyle\ \
(S:\texttt{Ty}(\Psi)))(T:\texttt{Ty}(\Psi.S)))\to\texttt{Ty}(\Psi)$
$\displaystyle M(\\_,(*,\Psi,S,T))$ $\displaystyle:=\Pi(S,T)$

Next we give the term $M^{\prime}$ for the internal $\Lambda$:

$\displaystyle M^{\prime}$
$\displaystyle:\Sigma(\Psi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(\\_:\\{*\\})(\Psi:\mathcal{D}))$
$\displaystyle\ \
(S:\texttt{Ty}(\Psi)))(T:\texttt{Ty}(\Psi.S)))(t:\texttt{Tm}(\Psi.S,T)))\to\texttt{Tm}(\Psi,\Pi(S,T))$
$\displaystyle M^{\prime}(\\_,(*,\Psi,S,T,t))$ $\displaystyle:=\Lambda(t)$

Next we give the term $M^{\prime\prime}$ for the internal App:

$\displaystyle M^{\prime\prime}$
$\displaystyle:\Sigma(\Psi^{\prime}:\mathcal{D})(\Sigma(\Sigma(\Sigma(\Sigma(\Sigma(\\_:\\{*\\})(\Psi:\mathcal{D}))(S:\texttt{Ty}(\Psi)))$
$\displaystyle\ \
(T:\texttt{Ty}(\Psi.S)))(t:\texttt{Tm}(\Psi,\Pi(S,T))))(s:\texttt{Tm}(\Psi,S)))$
$\displaystyle\ \ \to\texttt{Tm}(\Psi,T\\{\langle id_{\Psi},s\rangle\\})$
$\displaystyle M^{\prime\prime}(\\_,(*,\Psi,S,T,t,s))$
$\displaystyle:=\textsf{App}(t,s)$

$\Pi$, $\Lambda$ and App on the right are given by the $\Pi$ structure of
$\mathcal{D}$. Thus the $\Pi$ structure of $\mathcal{D}$ can also be
internalized.

##  5 Internalize Closed Types and Terms

In Section 3, we showed that the presheaf category can internalize
$\mathcal{D}$ and its CwF structure. These internal types and terms are
relative to an internal context in the base category and thus these internal
types and terms can be potentially open. To obtain closed types and terms, we
can set the internal context to be the empty one: * ⊢ Ty(⊤)  type

* T : Ty(⊤) ⊢ Tm(⊤, T)  type

###  5.1 Closed Types

There is another way to define semantic types to represent closed internal
types and terms. Notice that in Section 3, all the semantic types are defined
by ignoring the first projection. If we view the base category $\mathcal{D}$
as an index category for a Kripke relation, then that means the semantic types
we defined in Section 3 are invariant under the Kripke relation. This allows
us to faithfully internalize all structures of $\mathcal{D}$ in
$\widehat{\mathcal{D}}$. Hence, it is interesting to consider what if a
semantic type respects the Kripke relation? This motivates a different way to
internalize types and terms in $\mathcal{D}$ in $\widehat{\mathcal{D}}$.

$\displaystyle\textsf{Ty}^{\prime}$
$\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top})$
$\displaystyle\textsf{Ty}^{\prime}(\Psi,*)$ $\displaystyle:=\texttt{Ty}(\Psi)$
$\displaystyle\textsf{Ty}^{\prime}(\delta:(\smallint\widehat{\top})^{op}((\Psi,*),(\Phi,*)))$
$\displaystyle:=S\mapsto S\\{\delta\\}:\texttt{Ty}(\Psi)\to\texttt{Ty}(\Phi)$

This semantic type interprets the following judgment: * ⊢ Ty ’ type Now let us
examine what constitutes its semantic terms. By definition,

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}^{\prime})=\\{$
$\displaystyle M:\Sigma(\Psi:\mathcal{D})\\{*\\}\to\texttt{Ty}(\Psi)$
$\displaystyle|\
\forall\Phi:\mathcal{D},\delta:\mathcal{D}^{op}(\Psi,\Phi).M(\Psi,*)\\{\delta\\}=M(\Phi,*)\\}$

That is, if $M:\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}^{\prime})$,
then $M(\Psi,*)$ is a valid type in $\mathcal{D}$ for all $\Psi$ and is
coherent with substitution in $\mathcal{D}$. Effectively, this implies $M$
represents a _closed_ type in $\mathcal{D}$, because once $M(\top,*)$ is
fixed, $M(\Psi,*)$ for any $\Psi$ is induced due to uniqueness of
$\Psi\Rightarrow\top$. Thus we have

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}^{\prime})\simeq\texttt{Ty}(\top)\simeq\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}(\top))$

That is $\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}^{\prime})$ is
isomorphic to $\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}(\top))$.

###  5.2 Closed Terms

We can construct closed internal terms in a very similar way. The
corresponding syntactic type is * T : Ty ’ ⊢ Tm ’(T) type This semantic type
is constructed as follows:

$\displaystyle\textsf{Tm}^{\prime}$
$\displaystyle:\widehat{\texttt{Ty}}(\widehat{\top}.\textsf{Ty}^{\prime})$
$\displaystyle\textsf{Tm}^{\prime}(\Psi,(*,T))$
$\displaystyle:=\texttt{Tm}(\Psi,T)$
$\displaystyle\textsf{Tm}^{\prime}(\delta:(\smallint(\widehat{\top}.\textsf{Ty}^{\prime}))^{op}((\Psi,(*,T)),(\Phi,(*,T\\{\delta\\}))))$
$\displaystyle:=s:\texttt{Tm}(\Psi,T)\mapsto
s\\{\delta\\}:\texttt{Tm}(\Psi,T\\{\delta\\})$

Similar to $\textsf{Ty}^{\prime}$, the morphism part of the functorial action
of $\textsf{Tm}^{\prime}$ is substitutions. Let us consider the semantic terms
of $\textsf{Tm}^{\prime}$:

$\displaystyle\widehat{\texttt{Tm}}(\widehat{\top}.\textsf{Ty}^{\prime},\textsf{Tm}^{\prime})=\\{$
$\displaystyle
M:\Sigma(\Psi:\mathcal{D})(\Sigma\\{*\\}(T:\texttt{Ty}(\Psi)))\to\texttt{Tm}(\Psi,T)$
$\displaystyle|\
\forall\Phi:\mathcal{D},\delta:\mathcal{D}^{op}(\Psi,\Phi),T:\texttt{Ty}(\Psi).$
$\displaystyle\ \ M(\Psi,(*,T))\\{\delta\\}=M(\Phi,(*,T\\{\delta\\}))\\}$

We are not able to show that
$\widehat{\texttt{Tm}}(\widehat{\top}.\textsf{Ty}^{\prime},\textsf{Tm}^{\prime})$
corresponds to closed terms from the specifications directly, because we do
not know $T$ is a (weakened) closed type. Nevertheless, we can be sure about
this because the definition of
$\widehat{\texttt{Tm}}(\widehat{\top},\textsf{Ty}^{\prime})$ implicitly
requires $T$ to be closed, as previously discussed.

###  5.3 Closed versus Open

Now we see that Ty and Tm are strictly more expressive than
$\textsf{Ty}^{\prime}$ and $\textsf{Tm}^{\prime}$. In particular,
$\textsf{Ty}^{\prime}$ and $\textsf{Tm}^{\prime}$ are closed, so there cannot
be any frontend syntax for any binding construct. What can they be used for?
Since they are closed, one kind of systems they can model is typed
combinatorics. Since we do not need variables in combinatorics, we only need
to talk about closed programs. Moreover, the operations for
$\textsf{Ty}^{\prime}$ and $\textsf{Tm}^{\prime}$ are much limited. We are not
able to express internal substitutions and their operations because we have no
direct access to the underlying $\mathcal{D}$-morphisms.

##  6 Constant Presheaves

All previous constructions are coherent with $\mathcal{D}$-morphisms due to
functoriality or set specifications. In this section, we consider a special
class of functors which have a “world” fixed:

$\displaystyle\square$
$\displaystyle:\widehat{\mathcal{D}}\Rightarrow\widehat{\mathcal{D}}$
$\displaystyle\square(\Gamma)(\Psi:\mathcal{D})$ $\displaystyle:=\Gamma(\top)$
$\displaystyle\square(\Gamma)(\delta,s)$ $\displaystyle:=s$

We refer to this functor as $\square$ because it is a comonadic modality. We
can easily see this by construction:

$\displaystyle\square\square(\Gamma)$ $\displaystyle=\square\Gamma$
$\displaystyle\epsilon_{\square}$
$\displaystyle:\square(\Gamma)\Rightarrow\Gamma$
$\displaystyle\epsilon_{\square}(\Psi:\mathcal{D},s:\Gamma(\top))$
$\displaystyle:=\Gamma(!,s)$

$\square$ is a definitionally idempotent comonad, which is not the most
general necessity modality. In the following definitions, we make use of the
idempotency, so the construction is not generally applicable to other
comonadic modality. A general formulation is left for future investigation.

###  6.1 Semantic Types and Terms

Next we consider some constructions. Given a semantic type
$A:\widehat{\texttt{Ty}}(\Gamma)$, we obtain

$\displaystyle\square A$ $\displaystyle:\widehat{\texttt{Ty}}(\square\Gamma)$
$\displaystyle\square A(\Psi,s:\Gamma(\top))$ $\displaystyle:=A(\top,s)$
$\displaystyle\square A(\delta)$ $\displaystyle:=M\mapsto M$

When we apply context comprehension to $\square\Gamma$ and $\square A$, we
have

$\displaystyle\square\Gamma.\square A(\Psi)$
$\displaystyle=\Sigma(s:\Gamma(\top))A(\top,s)$
$\displaystyle\square\Gamma.\square A(\delta)(s,a)$ $\displaystyle=(s,a)$

Thus we have $\square\Gamma.\square A=\square(\Gamma.A)$.

Given a semantic term $M:\widehat{\texttt{Tm}}(\Gamma,A)$, we have

$\displaystyle\square M$
$\displaystyle:\widehat{\texttt{Tm}}(\square\Gamma,\square A)$
$\displaystyle\square M(\Psi,(s:\Gamma(\top),a:A(\top,s)))$
$\displaystyle:=M(\top,(s,a))$

Since the morphism action of $\square T$ is identity, the specification of
$\square M$ is trivially true.

###  6.2 Interpreting Introduction Rule

We can interpret the introduction rule for necessity: * Δ; ⋅ ⊢M : A Δ; Γ⊢box M
: □A We interpret the global context to $\square\Delta$ and $\Delta;\Gamma$ to
$\square\Delta;\Gamma$ in $\widehat{\mathcal{D}}$, where ; in the semantic
means concatenation. This operation is defined by recursively interpreting
$\Gamma$:

$\displaystyle\Delta;\top$ $\displaystyle:=\Delta$
$\displaystyle\Delta;(\Gamma.A)$ $\displaystyle:=(\Delta;\Gamma).A$

The operator ; has lower precedence than context comprehension. That means
$\Delta;\Gamma.A$ means $\Delta;(\Gamma.A)$. Given
$M:\widehat{\texttt{Tm}}(\square\Delta,A)$ and $k=|\Gamma|$, we obtain

$\displaystyle\texttt{box}(M)$
$\displaystyle:\widehat{\texttt{Tm}}(\square\Delta;\Gamma,\square
A\\{p^{k}\\})$ $\displaystyle\texttt{box}(M)$ $\displaystyle:=\square
M\\{p^{k}\\}$

This formulation is special and takes advantage of the idempotency of
$\square$, because we implicitly make use of
$\square\square\Delta=\square\Delta$.

###  6.3 Interpreting Elimination Rule

For the eliminator, we can explore two different flavors: Δ; ⋅ ⊢A type

* Δ; Γ, x : □A ⊢B type
Δ; Γ⊢M : □A
Δ, u : A ; Γ⊢N : B[box u/x] Δ; Γ⊢$\textsf{let box }u=M\textsf{ in }N$ : B[M/x]

The formulation is given by [Shulman, 2018]. Let us interpret the syntax to
the model.

Given $A:\widehat{\texttt{Ty}}(\square\Delta)$,
$B:\widehat{\texttt{Ty}}(\square\Delta;\Gamma.\square A\\{p^{k}\\})$ for
$k=|\Gamma|$, $M:\widehat{\texttt{Tm}}(\square\Delta;\Gamma,\square
A\\{p^{k}\\})$ and
$N:\widehat{\texttt{Tm}}(\square(\Delta.A);\Gamma\\{p\\},B\\{\langle
q(p,\Gamma),v_{\square A}\\{p^{k}\\}\rangle\\})$, we want to construct
$\texttt{letbox}(M,N):\widehat{\texttt{Tm}}(\square\Delta;\Gamma,B\\{\langle
id_{\square\Delta;\Gamma},M\rangle\\})$. When stating the semantic term of
$N$, we used certain generalizations, which we make explicit below.
$q(\sigma,\Gamma)$ is a generalization of $q(\sigma,A)$ defined in Section
3.10. $\Gamma\\{\sigma\\}$ is the generalization of type substitution. Given
$\sigma:\Delta^{\prime}\Rightarrow\Delta$ and that $\Delta;\Gamma$ is a valid
context, we define
$q(\sigma,\Gamma):\Delta^{\prime};\Gamma\\{\sigma\\}\Rightarrow\Delta;\Gamma$
and $\Delta^{\prime};\Gamma\\{\sigma\\}$ mutually:

$\displaystyle q(\sigma,\top)$ $\displaystyle:=\sigma$ $\displaystyle
q(\sigma,\Gamma.A)$ $\displaystyle:=q(q(\sigma,\Gamma),A)$
$\displaystyle\Delta^{\prime};\top\\{\sigma\\}$
$\displaystyle:=\Delta^{\prime}$
$\displaystyle\Delta^{\prime};(\Gamma.A)\\{\sigma\\}$
$\displaystyle:=\Delta^{\prime};\Gamma\\{\sigma\\}.A\\{q(\sigma,\Gamma)\\}$

Next we can move on to defining $\texttt{letbox}(M,N)$:

$\displaystyle\texttt{letbox}(M,N)$
$\displaystyle:\widehat{\texttt{Tm}}(\square\Delta;\Gamma,B\\{\langle
id_{\square\Delta;\Gamma},M\rangle\\})$
$\displaystyle\texttt{letbox}(M,N)(\Psi,(s:\Delta(\top),s^{\prime}:\Gamma(\Psi)))$
$\displaystyle:=N(\Psi,(s,M(\Psi,(s,s^{\prime})):A(\top,s),s^{\prime}))$

Since we interpret global contexts as $\square$ contexts, $M$ of type $\square
A$ can be directly applied to $A$ in the global context $\square(\Delta.A)$.
This allows us to directly plug in $M(\Psi,(s,s^{\prime}))$ in an argument of
$N$. This gives us one model for necessity.

##  7 Conclusion

In this note, we reviewed a construction of CwF structure in any presheaf
category using category of elements. We showed that any syntactic type theory
interpreting the CwF structure of a presheaf category can be used to reason
about the base category. Moreover, the syntactic representation of the base
category is faithful. We also showed that this construction extends to $\Pi$
types. We also consider a idempotent comonadic modality in a presheaf
category.

## References

  * [Dybjer, 1995] Dybjer, P. (1995).  Internal type theory.  In Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, pages 120–134.
  * [Hofmann, 1997] Hofmann, M. (1997).  Syntax and semantics of dependent types, pages 13–54.  Springer London, London.
  * [Shulman, 2018] Shulman, M. (2018).  Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.  Math. Struct. Comput. Sci., 28(6):856–941.


LSTM-Con CAT | Cascade Utt | $29.37\pm 0.37$ | $33.62\pm 0.38$ | $38.41\pm 0.4$ | $43.07\pm 0.43$ | $46.55\pm 0.44$ | ✓
Conformer CM | Audio Baseline | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | -
Conformer CM | Vanilla | $34.91\pm 0.43$ | $41.29\pm 0.43$ | $48.96\pm 0.45$ | $60.59\pm 0.5$ | $98.34\pm 0.05$ | ✗
Conformer CM | Cascade Utt | $27.89\pm 0.37$ | $29.06\pm 0.38$ | $30.2\pm 0.39$ | $31.05\pm 0.4$ | $31.56\pm 0.4$ | ✓
Conformer CM | Dropout Utt | $33.11\pm 0.43$ | $48.17\pm 0.47$ | $61.14\pm 0.48$ | $74.43\pm 0.46$ | $45.43\pm 0.47$ | ✗
Table 27: Robustness to $\mathcal{T}_{\textit{rate}}$ for $0$db. Columns three to eight represent the amount of dropped video frames. Architecture | Method | $0$ | $\frac{1}{128}$ | $\frac{1}{32}$ | $\frac{1}{8}$ | $\frac{1}{2}$ | $1$ | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | Audio Baseline | $33.54\pm 0.43$ | $33.54\pm 0.43$ | $33.54\pm 0.43$ | $33.54\pm 0.43$ | $33.54\pm 0.43$ | $33.54\pm 0.43$ | -
Conformer CAT | Vanilla | $24.96\pm 0.35$ | $24.94\pm 0.35$ | $24.95\pm 0.35$ | $25.08\pm 0.35$ | $25.9\pm 0.35$ | $35.51\pm 0.43$ | ✗
Conformer CAT | Vanilla (25L) | $24.75\pm 0.35$ | $24.76\pm 0.35$ | $24.79\pm 0.35$ | $24.91\pm 0.35$ | $26.78\pm 0.37$ | $34.88\pm 0.43$ | -
Conformer CAT | Cascade Utt | $26.12\pm 0.36$ | $26.13\pm 0.36$ | $26.25\pm 0.36$ | $26.72\pm 0.37$ | $28.73\pm 0.39$ | $31.08\pm 0.4$ | ✓
Conformer CAT | Dropout Utt | $24.33\pm 0.34$ | $24.35\pm 0.34$ | $24.36\pm 0.34$ | $24.49\pm 0.34$ | $26.66\pm 0.36$ | $31.67\pm 0.4$ | ✓
Conformer CAT | Cascade Frame | $28.04\pm 0.38$ | $28.05\pm 0.38$ | $28.08\pm 0.38$ | $28.23\pm 0.39$ | $30.14\pm 0.42$ | $34.17\pm 0.44$ | ✗
Conformer CAT | Dropout Frame | $27.58\pm 0.37$ | $27.47\pm 0.37$ | $27.11\pm 0.36$ | $26.51\pm 0.36$ | $27.56\pm 0.38$ | $32.54\pm 0.41$ | ✗
Conformer CAT | AV Dropout Utt | $23.64\pm 0.33$ | $23.62\pm 0.33$ | $23.63\pm 0.33$ | $23.8\pm 0.33$ | $25.36\pm 0.35$ | $33.55\pm 0.41$ | ✓
Conformer CAT | Two-Pass | $30.06\pm 0.42$ | $30.05\pm 0.42$ | $30.11\pm 0.42$ | $30.47\pm 0.43$ | $31.91\pm 0.43$ | $33.54\pm 0.43$ | ✓
Con-LSTM CAT | Cascade Utt | $27.9\pm 0.39$ | $27.96\pm 0.39$ | $28.11\pm 0.39$ | $28.84\pm 0.39$ | $30.7\pm 0.41$ | $31.4\pm 0.41$ | ✓
LSTM CAT | Audio Baseline | $46.38\pm 0.44$ | $46.38\pm 0.44$ | $46.38\pm 0.44$ | $46.38\pm 0.44$ | $46.38\pm 0.44$ | $46.38\pm 0.44$ | -
LSTM CAT | Vanilla | $30.93\pm 0.39$ | $30.94\pm 0.39$ | $31.16\pm 0.39$ | $32.06\pm 0.4$ | $37.19\pm 0.44$ | $51.53\pm 0.45$ | ✗
LSTM CAT | Cascade Utt | $33.67\pm 0.4$ | $33.71\pm 0.4$ | $34.15\pm 0.4$ | $35.9\pm 0.41$ | $42.15\pm 0.44$ | $46.55\pm 0.44$ | ✓
LSTM CAT | Dropout Utt | $33.41\pm 0.4$ | $33.47\pm 0.4$ | $33.78\pm 0.4$ | $35.11\pm 0.41$ | $41.79\pm 0.44$ | $48.13\pm 0.44$ | ✗
LSTM-Con CAT | Cascade Utt | $29.37\pm 0.37$ | $29.42\pm 0.37$ | $29.72\pm 0.38$ | $30.96\pm 0.38$ | $37.42\pm 0.42$ | $46.55\pm 0.44$ | ✓
Conformer CM | Audio Baseline | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | $31.79\pm 0.42$ | -
Conformer CM | Vanilla | $34.91\pm 0.43$ | $35.03\pm 0.43$ | $35.68\pm 0.44$ | $38.48\pm 0.45$ | $51.29\pm 0.51$ | $98.34\pm 0.05$ | ✗
Conformer CM | Cascade Utt | $27.89\pm 0.37$ | $27.9\pm 0.37$ | $27.98\pm 0.38$ | $28.48\pm 0.38$ | $30.99\pm 0.4$ | $31.56\pm 0.4$ | ✓
Conformer CM | Dropout Utt | $33.11\pm 0.43$ | $33.46\pm 0.42$ | $35.82\pm 0.44$ | $46.46\pm 0.51$ | $68.24\pm 0.5$ | $45.43\pm 0.47$ | ✗

##  Appendix F Experiments on TED LRS3

We present additional results on the TED LRS3 dataset for just the Conformer
CAT and LSTM CAT Cascade Utt models. The architectural configurations are the
same as the ones detailed in Section 5, with the exception of differences in
optimization. The models are trained with a constant learning rate of $0.0001$
at batch size $512$ for $35$k steps. Like Afouras et al. (2018) and Ma et al.
(2021b), we initialize our models from pre-trained weights. This was done
using the training data described in Section 5. Like in the main paper, we
augment the TED LRS3 test set with artificially added babble noise from the
NoiseX corpus (Varga & Steeneken, 1993) at different SNR levels: clean,
$20$db, $10$db, $0$db. Like in the main paper, all the Cascade Utt models were
found to be robust on all the test suites. To our knowledge, the $0.92$ WER we
are reporting on the clean TED LRS3 test set by the Conformer CAT Cascade Utt
model is also the best number that has been reported on this dataset.

Table 28: Robustness to $\mathcal{T}_{\textit{berUtt}}$ for Conformer and LSTM Cascade Utt models. Columns three to seven represent the amount of dropped video frames. Architecture | Noise | $0.0$ | $0.25$ | $0.5$ | $0.75$ | $1.0$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $0.9\pm 0.25$ | $0.99\pm 0.27$ | $0.95\pm 0.26$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $2.69\pm 0.47$ | $3.32\pm 0.49$ | $4.16\pm 0.58$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $1.0\pm 0.26$ | $1.04\pm 0.26$ | $1.03\pm 0.26$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $2.64\pm 0.45$ | $3.26\pm 0.51$ | $4.16\pm 0.57$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.13\pm 0.27$ | $1.16\pm 0.28$ | $1.11\pm 0.27$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $3.31\pm 0.52$ | $4.62\pm 0.6$ | $5.57\pm 0.68$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $2.53\pm 0.43$ | $3.22\pm 0.5$ | $3.91\pm 0.55$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $8.95\pm 0.99$ | $14.41\pm 1.31$ | $20.79\pm 1.44$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓
Table 29: Robustness to $\mathcal{T}_{\textit{berFrame}}$ for Conformer and LSTM Cascade Utt models. Columns three to seven represent the amount of dropped video frames. Architecture | Noise | $0.0$ | $0.25$ | $0.5$ | $0.75$ | $1.0$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $1.0\pm 0.26$ | $1.0\pm 0.27$ | $0.99\pm 0.27$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $2.07\pm 0.36$ | $2.85\pm 0.44$ | $3.69\pm 0.49$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $0.95\pm 0.25$ | $0.97\pm 0.26$ | $1.03\pm 0.27$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $2.25\pm 0.39$ | $2.92\pm 0.44$ | $3.95\pm 0.52$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.12\pm 0.28$ | $1.13\pm 0.27$ | $1.27\pm 0.29$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $2.93\pm 0.45$ | $3.66\pm 0.5$ | $5.02\pm 0.64$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $2.32\pm 0.4$ | $3.38\pm 0.51$ | $4.0\pm 0.55$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $8.26\pm 0.82$ | $12.93\pm 1.03$ | $19.69\pm 1.3$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓
Table 30: Robustness to $\mathcal{T}_{\textit{start}}$ for Conformer and LSTM Cascade Utt models. Columns three to seven represent the amount of dropped video frames. Architecture | Noise | $0.0$ | $0.25$ | $0.5$ | $0.75$ | $1.0$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $0.93\pm 0.25$ | $1.05\pm 0.27$ | $1.06\pm 0.27$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $3.04\pm 0.46$ | $4.03\pm 0.53$ | $4.6\pm 0.58$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $0.99\pm 0.26$ | $1.04\pm 0.26$ | $1.09\pm 0.27$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $3.1\pm 0.48$ | $4.13\pm 0.56$ | $5.01\pm 0.62$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.08\pm 0.27$ | $1.15\pm 0.28$ | $1.3\pm 0.29$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $3.61\pm 0.5$ | $4.87\pm 0.6$ | $6.31\pm 0.7$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $2.62\pm 0.43$ | $3.32\pm 0.5$ | $3.88\pm 0.56$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $9.76\pm 0.88$ | $16.05\pm 1.19$ | $22.26\pm 1.44$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓
Table 31: Robustness to $\mathcal{T}_{\textit{mid}}$ for Conformer and LSTM Cascade Utt models. Columns three to seven represent the amount of dropped video frames. Architecture | Noise | $0.0$ | $0.25$ | $0.5$ | $0.75$ | $1.0$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $1.04\pm 0.27$ | $1.09\pm 0.28$ | $1.04\pm 0.27$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $2.63\pm 0.42$ | $3.46\pm 0.49$ | $4.37\pm 0.57$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $1.02\pm 0.26$ | $1.08\pm 0.27$ | $1.01\pm 0.26$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $2.52\pm 0.42$ | $3.59\pm 0.5$ | $4.58\pm 0.59$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.09\pm 0.27$ | $1.28\pm 0.29$ | $1.26\pm 0.28$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $3.28\pm 0.48$ | $4.8\pm 0.6$ | $6.0\pm 0.7$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $2.76\pm 0.45$ | $3.26\pm 0.49$ | $4.2\pm 0.58$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $10.57\pm 0.94$ | $16.98\pm 1.23$ | $22.22\pm 1.39$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓
Table 32: Robustness to $\mathcal{T}_{\textit{end}}$ for Conformer and LSTM Cascade Utt models. Columns three to seven represent the amount of dropped video frames. Architecture | Noise | $0.0$ | $0.25$ | $0.5$ | $0.75$ | $1.0$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $1.02\pm 0.27$ | $1.04\pm 0.28$ | $1.06\pm 0.28$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $1.92\pm 0.36$ | $2.78\pm 0.43$ | $3.74\pm 0.52$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $0.95\pm 0.26$ | $1.01\pm 0.27$ | $1.04\pm 0.27$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $2.0\pm 0.37$ | $2.79\pm 0.45$ | $3.96\pm 0.54$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.09\pm 0.27$ | $1.11\pm 0.27$ | $1.2\pm 0.28$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $2.33\pm 0.38$ | $3.65\pm 0.52$ | $5.31\pm 0.66$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $2.59\pm 0.42$ | $3.39\pm 0.49$ | $3.95\pm 0.54$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $7.76\pm 0.72$ | $13.45\pm 1.01$ | $20.08\pm 1.31$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓
Table 33: Robustness to $\mathcal{T}_{\textit{rate}}$ for Conformer and LSTM Cascade Utt models. Columns three to eight represent the amount of dropped video frames. Architecture | Noise | $0$ | $\frac{1}{128}$ | $\frac{1}{32}$ | $\frac{1}{8}$ | $\frac{1}{2}$ | $1$ | AO Baseline | Robust
---|---|---|---|---|---|---|---|---|---
Conformer CAT | clean | $0.92\pm 0.26$ | $0.92\pm 0.26$ | $0.94\pm 0.26$ | $0.94\pm 0.26$ | $0.98\pm 0.26$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | ✓
LSTM CAT | clean | $1.8\pm 0.35$ | $1.77\pm 0.35$ | $1.76\pm 0.35$ | $1.94\pm 0.36$ | $2.47\pm 0.39$ | $4.9\pm 0.61$ | $4.82\pm 0.61$ | ✓
Conformer CAT | 20db | $1.02\pm 0.26$ | $1.02\pm 0.26$ | $1.0\pm 0.26$ | $1.02\pm 0.26$ | $1.01\pm 0.27$ | $0.99\pm 0.26$ | $1.11\pm 0.29$ | ✓
LSTM CAT | 20db | $1.8\pm 0.35$ | $1.78\pm 0.35$ | $1.76\pm 0.35$ | $1.94\pm 0.36$ | $2.59\pm 0.41$ | $5.25\pm 0.65$ | $5.16\pm 0.64$ | ✓
Conformer CAT | 10db | $1.1\pm 0.27$ | $1.1\pm 0.27$ | $1.11\pm 0.27$ | $1.07\pm 0.27$ | $1.08\pm 0.26$ | $1.19\pm 0.28$ | $1.41\pm 0.31$ | ✓
LSTM CAT | 10db | $2.11\pm 0.38$ | $2.12\pm 0.38$ | $2.15\pm 0.4$ | $2.33\pm 0.4$ | $3.1\pm 0.45$ | $6.79\pm 0.74$ | $6.6\pm 0.73$ | ✓
Conformer CAT | 0db | $1.9\pm 0.36$ | $1.9\pm 0.36$ | $1.95\pm 0.37$ | $2.35\pm 0.41$ | $2.91\pm 0.46$ | $4.41\pm 0.58$ | $4.41\pm 0.57$ | ✓
LSTM CAT | 0db | $4.32\pm 0.55$ | $4.33\pm 0.55$ | $4.77\pm 0.61$ | $5.95\pm 0.67$ | $11.93\pm 1.02$ | $25.04\pm 1.5$ | $24.54\pm 1.45$ | ✓