# A Category Theoretic View of Contextual Types: from Simple Types to
Dependent Types

Jason Z. S. Hu<EMAIL_ADDRESS>McGill UniversityMcConnell
Engineering Bldg. 3480 University St.,MontréalQuébecCanadaH3A 0E9 ,  Brigitte
Pientka<EMAIL_ADDRESS>McGill UniversityMcConnell Engineering Bldg.
3480 University St.,MontréalQuébecCanadaH3A 0E9 and  Ulrich Schöpp
<EMAIL_ADDRESS>fortiss GmbHMunichGermany

(2021)

###### Abstract.

We describe the categorical semantics for a simply typed variant and a
simplified dependently typed variant of Cocon, a contextual modal type theory
where the box modality mediates between the weak function space that is used
to represent higher-order abstract syntax (HOAS) trees and the strong function
space that describes (recursive) computations about them. What makes Cocon
different from standard type theories is the presence of first-class contexts
and contextual objects to describe syntax trees that are closed with respect
to a given context of assumptions. Following M. Hofmann’s work, we use a
presheaf model to characterise HOAS trees. Surprisingly, this model already
provides the necessary structure to also model Cocon. In particular, we can
capture the contextual objects of Cocon using a comonad $\flat$ that restricts
presheaves to their closed elements. This gives a simple semantic
characterisation of the invariants of contextual types (e.g. substitution
invariance) and identifies Cocon as a type-theoretic syntax of presheaf
models. We further extend this characterisation to dependent types using
categories with families and show that we can model a fragment of Cocon
without recursor in the Fitch-style dependent modal type theory presented by
Birkedal et. al..

category theory, type theory, contextual types, dependent types

††copyright: acmcopyright††journalyear: 2021††ccs: Theory of computation Modal
and temporal logics††ccs: Theory of computation Type theory

##  1\. Introduction

A fundamental question when defining, implementing, and working with languages
and logics is: How do we represent and analyse syntactic structures? Higher-
order abstract syntax (Pfenning and Elliott, 1988) (or lambda-tree syntax
(Miller and Palamidessi, 1999)) provides a deceptively simple answer to this
question. The basic idea to represent syntactic structures is to map uniformly
binding structures in our object language (OL) to the function space in a
meta-language thereby inheriting $\alpha$-renaming and capture-avoiding
substitution. In the logical framework LF (Harper et al., 1993), for example,
we can define a small functional programming language consisting of functions,
function application, and let-expressions using a type tm as follows:

⬇

lam : (tm $\rightarrow~{}$ tm) $\rightarrow~{}$ tm. letv: tm $\rightarrow~{}$
(tm $\rightarrow~{}$ tm) $\rightarrow~{}$ tm. app : tm $\rightarrow~{}$ tm
$\rightarrow~{}$ tm.

The object-language term
$(\mathsf{lam}\;x.\,\mathsf{lam}\;y.\,\mathsf{let}\;w=x\;y\;\mathsf{in}\;w\;y)$
is then encoded as lam \x.lam \y.letv (app x y) \w.app w y using the LF
abstractions to model binding. Object-level substitution is modelled through
LF application; for instance, the fact that $((\mathsf{lam}~{}x.M)~{}N)$
reduces to $[N/x]M$ in our object language is expressed as (app (lam M) N)
reducing to (M N).

This approach is elegant and can offer substantial benefits: we can treat
objects equivalent modulo renaming and do not need to define object-level
substitution.

However, we not only want to just construct HOAS trees, but also to analyse
them and to select sub-trees. This is challenging, as sub-trees are context
sensitive. For example, the term letv (app x y) \w.app w y only makes sense in
a context x:tm,y:tm. Moreover, one cannot simply extend LF to allow syntax
analysis. If one simply added a recursion combinator to LF, then it could be
used to define many functions M: tm $\rightarrow~{}$ tm for which lam M would
not represent an object-level syntax term (Hofmann, 1999).

Contextual types (Nanevski et al., 2008; Pientka, 2008; Gabbay and Nanevski,
2013) offer a type-theoretic solution to these problems by reifying the typing
judgement, i.e. that letv (app x y) \w.app w y has type tm in the context
x:tm,y:tm, as a _contextual type_ $\lceil
x{:}\texttt{tm},y{:}\texttt{tm}\vdash\texttt{tm}\rceil$. The contextual type
$\lceil x{:}\texttt{tm},y{:}\texttt{tm}\vdash\texttt{tm}\rceil$ describes a
set of terms of type tm that may contain variables $x$ and $y$. In particular,
the contextual object $\lceil
x,y\vdash\mathtt{letv}~{}(\mathtt{app}~{}x~{}y)~{}\lambda
w.\mathtt{app}~{}w~{}y\rceil$ has the given contextual type. By abstracting
over contexts and treating contexts as first-class, we can now recursively
analyse HOAS trees (Pientka, 2008; Pientka and Dunfield, 2008; Pientka and
Abel, 2015). Recently, Pientka et al. (2019) further generalised these ideas
and presented a contextual modal type theory, Cocon, where we can mix HOAS
trees and computations, i.e. we can use (recursive) computations to analyse
and traverse (contextual) HOAS trees and we can embed computations within HOAS
trees. This line of work provides a syntactic perspective to the question of
how to represent and analyse syntactic structures with binders, as it focuses
on decidability of type checking and normalisation. However, its semantics
remains not well-understood. What is the semantic meaning of a contextual
type? Can we semantically justify the given induction principles? What is the
semantics of a first-class context?

While a number of closely related categorical models of abstract syntax with
bindings (Hofmann, 1999; Fiore et al., 1999; Gabbay and Pitts, 1999) were
proposed around 2000, the relationship of these models to concrete type-
theoretic languages for computing with HOAS structures was tenuous. In this
paper, we give a category-theoretic semantics for Cocon. This provides
semantic perspective of contextual types and first-class contexts. Maybe
surprisingly, the presheaf model introduced by Hofmann (1999) already provides
the necessary structure to also model contextual modal type theory. Besides
the standard structure of this model, we only rely on two key concepts: a box
(necessity) modality which is the same modality discussed by Hofmann (1999,
Section 6) and a cartesian closed universe of representables. In the first
half of this paper, we focus on the special case of Cocon where the HOAS trees
are simply-typed. Concentrating on the simply-typed setting allows us to
introduce the main idea without the additional complexity that type
dependencies bring with them. The dependently-typed case is reserved in
Section 6, in which we study the semantics using a categorical framework for
dependent types, categories with families (CwFs). We extend the model in the
simply typed case such that the domain category is a CwF, the structure of
which is preserved by the Yoneda embedding. In Section 7, we study Cocon’s
relation with a Fitch-style system and show their similarity.

Our work provides a semantic foundation to Cocon and can serve as a starting
point to investigate connections to similar work. First, our work connects
Cocon to other work on internal languages for presheaf categories with a
$\flat$-modality, such as spatial type theory (Shulman, 2018) or crisp type
theory (Licata et al., 2018). Second, it may help to understand the relations
of Cocon to type theories that use a modality for metaprogramming and
intensional recursion, such as (Kavvos, 2017). While Cocon is built on the
same general ideas, a main difference seems to be that Cocon distinguishes
between HOAS trees and computations, even though it allows mixed use of them.
We hope to clarify the relation by providing a semantical perspective.

This paper is an extended version of the conference paper (Pientka and Schöpp,
2020).

##  2\. Presheaves for Higher-Order Abstract Syntax

Our work begins with the presheaf models for HOAS of Hofmann (1999); Fiore et
al. (1999). The key idea of those approaches is to integrate substitution-
invariance in the computational universe in a controlled way. For the
representation of abstract syntax, one wants to allow only substitution-
invariant constructions. For example, lam M represents an object-level
abstraction if and only if M is a function that uses its argument in a
substitution-invariant way. For computation with abstract syntax, on the other
hand, one wants to allow non-substitution-invariant constructions too.
Presheaf categories allow one to choose the desired amount of substitution-
invariance.

Let $\mathbb{D}$ be a small category. The presheaf category
$\widehat{\mathbb{D}}$ is defined to be the category
$\mathrm{Set}^{{\mathbb{D}}^{\mathrm{op}}}$. Its objects are functors
$F\colon{\mathbb{D}}^{\mathrm{op}}\to\mathrm{Set}$, which are also called
_presheaves_. Such a functor $F$ is given by a set $F(\Psi)$ for each object
$\Psi$ of $\mathbb{D}$ together with a function $F(\sigma)\colon F(\Phi)\to
F(\Psi)$ for any object $\Phi$ and $\sigma\colon\Psi\to\Phi$ in $\mathbb{D}$,
subject to the functor laws. The intuition is that $F$ defines sets of
elements in various $\mathbb{D}$-contexts, together with a
$\mathbb{D}$-substitution action. A morphism $f\colon F\to G$ is a natural
transformation, which is a family of functions $f_{\Psi}\colon F(\Psi)\to
G(\Psi)$ for any $\Psi$. This family of functions must be natural, i.e.
commute with substitution $f_{\Psi}\circ F(\sigma)=G(\sigma)\circ f_{\Phi}$.

For the purposes of modelling higher-order abstract syntax, $\mathbb{D}$ will
typically be the term model of some domain-level lambda-calculus. By domain-
level, we mean the calculus that serves as the meta-level for object-language
encodings. It is the calculus that contains constants like lam and app from
the Introduction. We call it domain-level to avoid possible confusion between
different meta-levels later. For simplicity, let us for now use a simply-typed
lambda-calculus with functions and products as the domain language. It is
sufficient to encode the example from the Introduction and allows us to
explain the main idea underlying our approach.

The term model of the simply-typed domain-level lambda-calculus forms a
cartesian closed category $\mathbb{D}$. The objects of $\mathbb{D}$ are
contexts $x_{1}{:}\,A_{1},\dots,x_{n}{:}\,A_{n}$ of simple types. We use
$\Phi$ and $\Psi$ to range over such contexts. A morphism from
$x_{1}{:}\,A_{1},\dots,x_{n}{:}\,A_{n}$ to
$x_{1}{:}\,B_{1},\dots,x_{m}{:}\,B_{m}$ is a tuple $(t_{1},\dots,t_{m})$ of
terms $x_{1}{:}\,A_{1},\dots,x_{n}{:}\,A_{n}\vdash t_{i}\colon B_{i}$ for
$i=1,\dots,m$. A morphism of type $\Psi\to\Phi$ in $\mathbb{D}$ thus amounts
to a (domain-level) substitution that provides a (domain-level) term in
context $\Psi$ for each of the variables in $\Phi$. Terms are identified up to
$\alpha\beta\eta$-equality. One may achieve this by using a de Bruijn
encoding, for example, but the specific encoding is not important for this
paper. The terminal object is the empty context, which we denote by $\top$,
and the product $\Phi\times\Psi$ is defined by context concatenation. It is
not hard to see that any object $x_{1}{:}\,A_{1},\dots,x_{n}{:}\,A_{n}$ is
isomorphic to an object that is given by a context with a single variable,
namely $x_{1}{:}\,(A_{1}\times\dots\times A_{n})$. This is to say that
contexts can be identified with product types. In view of this isomorphism, we
shall allow ourselves to consider the objects of $\mathbb{D}$ also as types
and vice versa. The category $\mathbb{D}$ is cartesian closed, the exponential
of $\Phi$ and $\Psi$ being given by the function type $\Phi\to\Psi$ (where the
objects are considered as types).

The presheaf category $\widehat{\mathbb{D}}$ is a computational universe that
both embeds the term model $\mathbb{D}$ and that can represent computations
about it. Note that we cannot just enrich $\mathbb{D}$ with terms for
computations if we want to use HOAS. In a simply-typed lambda-calculus with
just the constant terms app: tm $\rightarrow~{}$ tm $\rightarrow~{}$ tm and
lam: (tm $\rightarrow~{}$ tm) $\rightarrow~{}$ tm, each term of type tm
represents an object-level term. This would not be the true anymore, if we
were to allow computations in the domain language, since one could define M to
be something like (\x. if x represents an object-level application then M1
else M2) for distinct M1 and M2. In this case, lam M would not represent an
object-level term anymore. If we want to preserve a bijection between the
object-level terms and their representations in the domain-language, we cannot
allow case-distinction over whether a term represents an object-level an
application.

The category $\widehat{\mathbb{D}}$ unites syntax with computations by
allowing one to enforce various degrees of substitution-invariance. By
choosing objects with different substitution actions, one can control the
required amount of substitution-invariance.

In one extreme, a set $S$ can be regarded as a constant presheaf. Define the
constant presheaf $\Omega S$ by $\Omega S(\Psi)=S$ and $\Omega
S(\sigma)=\mathsf{id}$ for all $\Psi$ and $\sigma$. Since the substitution
action is trivial, a morphism $\Omega S\to\Omega T$ in $\widehat{\mathbb{D}}$
amounts to just a function from set $S$ to set $T$. Since $\Omega S$ is thus
essentially just the set $S$, we shall write just $S$ both for the set $S$ and
the presheaf $\Omega S$.

The Yoneda embedding represents the other extreme. For any object $\Phi$ of
$\mathbb{D}$, the presheaf
$\mathrm{y}(\Phi)\colon{\mathbb{D}}^{\mathrm{op}}\to\mathrm{Set}$ is defined
by $\mathrm{y}(\Phi)(\Psi)=\mathbb{D}(\Psi,\Phi)$, which is the set of
morphisms from $\Psi$ to $\Phi$ in $\mathbb{D}$. The functor action is pre-
composition. The presheaf $\mathrm{y}(\Phi)$ should be understood as the type
of all domain-level substitutions with codomain $\Phi$. An important example
is $y(\texttt{tm})$. In this case, $\mathrm{y}(\texttt{tm})(\Psi)$ is the set
of all morphisms of type $\Psi\to\texttt{tm}$ in $\mathbb{D}$. By the
definition of $\mathbb{D}$, these correspond to domain-level terms of type tm
in context $\Psi$. In this way, the presheaf $\mathrm{y}(\texttt{tm})$
represents the domain-level terms of type tm.

The Yoneda embedding does in fact embed $\mathbb{D}$ into
$\widehat{\mathbb{D}}$ fully and faithfully, where the action on morphisms is
post-composition. This means that $\mathrm{y}$ maps a morphism
$\sigma\colon\Psi\to\Phi$ in $\mathbb{D}$ to the natural transformation
$\mathrm{y}(\sigma)\colon\mathrm{y}(\Psi)\to\mathrm{y}(\Phi)$ that is defined
by post-composing with $\sigma$. This definition makes $\mathrm{y}$ into a
functor $\mathrm{y}\colon\mathbb{D}\to\widehat{\mathbb{D}}$ that is moreover
full and faithful: its action on morphisms is a bijection from
$\mathbb{D}(\Psi,\Phi)$ to
$\widehat{\mathbb{D}}(\mathrm{y}(\Psi),\mathrm{y}(\Phi))$ for any $\Psi$ and
$\Phi$. This is because a natural transformation
$f\colon\mathrm{y}(\Psi)\to\mathrm{y}(\Phi)$ is, by naturality, uniquely
determined by $f_{\Psi}(\mathsf{id})$, where
$\mathsf{id}\in\mathbb{D}(\Psi,\Psi)=\mathrm{y}(\Psi)(\Psi)$, and
$f_{\Psi}(\mathsf{id})$ is an element of
$y(\Phi)(\Psi)=\mathbb{D}(\Psi,\Phi)$.

Since $\mathbb{D}$ embeds into $\widehat{\mathbb{D}}$ fully and faithfully,
the term model of the domain language is available in $\widehat{\mathbb{D}}$.
Consider for example $\mathrm{y}(\texttt{tm})$. Since $\mathrm{y}$ is full and
faithful, the morphisms from $\mathrm{y}(\texttt{tm})$ to
$\mathrm{y}(\texttt{tm})$ in $\widehat{\mathbb{D}}$ are in one-to-one
correspondence with the morphisms from tm to tm in $\mathbb{D}$. These, in
turn, are defined to be substitutions and correspond to simply-typed (domain-
level) lambda terms with one free variable. This shows that substitution
invariance cuts down the morphisms from $\mathrm{y}(\texttt{tm})$ to
$\mathrm{y}(\texttt{tm})$ in $\widehat{\mathbb{D}}$ just as much as one would
like for HOAS encodings.

But $\widehat{\mathbb{D}}$ contains not just a term model of the domain
language. It can also represent computations about the domain-level syntax and
computations that are not substitution-invariant. For example, arbitrary
functions on terms can be represented as morphisms from the constant presheaf
$\Omega(\mathrm{y}(\texttt{tm})(\top))$ to $\mathrm{y}(\texttt{tm})$. Recall
that $\top$ is the empty context, so that $\mathrm{y}(\texttt{tm})(\top)$ is
the set $\mathbb{D}(\top,\texttt{tm})$, by definition, which is isomorphic to
the set of closed domain-level terms of type tm. The morphisms from
$\Omega(\mathrm{y}(\texttt{tm})(\top))$ to $\mathrm{y}(\texttt{tm})$ in
$\widehat{\mathbb{D}}$ correspond to arbitrary functions from closed terms to
closed terms, without any restriction of substitution invariance.

The restriction to the constant presheaf of closed terms can be generalised to
arbitrary presheaves. Define a functor
$\flat\colon\widehat{\mathbb{D}}\to\widehat{\mathbb{D}}$ by letting $\flat F$
be the constant presheaf $\Omega(F(\top))$, i.e. $\flat F(\Psi)=F(\top)$ and
$\flat F(\sigma)=\mathsf{id}$. Thus, $\flat$ restricts any presheaf to the set
of its closed elements. The functor $\flat$ defines a comonad where the counit
$\varepsilon_{F}\colon\flat F\to F$ is the obvious inclusion and the
comultiplication $\nu_{F}\colon\flat F\to\flat\flat F$ is the identity. The
latter means that the comonad $\flat$ is idempotent.

The category $\widehat{\mathbb{D}}$ not only embeds $\mathbb{D}$ and allows
control over how much substitution invariance is wanted in various
constructions, it also is very rich in structure, not least because it also
embeds $\mathpzc{Set}$. We will show that $\widehat{\mathbb{D}}$ models
contextual types and computations about them. We will gradually introduce the
structure of $\widehat{\mathbb{D}}$ that we need to this end. We begin here by
noting that $\widehat{\mathbb{D}}$ is cartesian closed, in order to introduce
the notation for this structure.

Finite products exist in $\widehat{\mathbb{D}}$ and are constructed pointwise.

$\displaystyle\top(\Gamma)$ $\displaystyle=\\{*\\}$ $\displaystyle(X\times
Y)(\Gamma)$ $\displaystyle=X(\Gamma)\times Y(\Gamma)$

The Yoneda embedding preserves finite products, i.e. $\mathrm{y}(X\times
Y)\cong\mathrm{y}(X)\times\mathrm{y}(Y)$.

The category $\widehat{\mathbb{D}}$ has exponentials. The exponential
$(X\Rightarrow Y)$ can be calculated using the Yoneda lemma. We recall that
the Yoneda lemma states that $Z(\Gamma)$ is naturally isomorphic to
$\widehat{\mathbb{D}}(\mathrm{y}(\Gamma),Z)$. With this, we have:

$(X\Rightarrow Y)(\Gamma)\ \cong\
\widehat{\mathbb{D}}(\mathrm{y}(\Gamma),X\Rightarrow Y)\ \cong\
\widehat{\mathbb{D}}(\mathrm{y}(\Gamma)\times X,Y)$

Since $\mathrm{y}$ preserves finite products, we have in particular
$(\mathrm{y}(A)\Rightarrow\mathrm{y}(B))(\Gamma)\cong\widehat{\mathbb{D}}(\mathrm{y}(\Gamma)\times\mathrm{y}(A),\mathrm{y}(B))\cong\widehat{\mathbb{D}}(\mathrm{y}(\Gamma\times
A),\mathrm{y}(B))\cong\mathbb{D}(\Gamma\times A,B)$. In the case where
$A=B=\texttt{tm}$, this shows that the exponential
$\texttt{tm}\Rightarrow\texttt{tm}$ represents terms with an additional bound
variable. Given exponentials in $\widehat{\mathbb{D}}$, $y$ also preserves
exponentials, i.e. $\mathrm{y}(X\Rightarrow
Y)\cong\mathrm{y}(X)\Rightarrow\mathrm{y}(Y)$.

##  3\. Internal Language

To explain how $\widehat{\mathbb{D}}$ models higher-order abstract syntax and
contextual types, we need to expose more of its structure. Presenting it
directly in terms of functors and natural transformations is somewhat
laborious and the technical details may obscure the basic idea of our
approach. We therefore use dependent types as an internal language for working
with $\widehat{\mathbb{D}}$.

It is well-known that presheaf categories like $\widehat{\mathbb{D}}$ furnish
a model of a dependent type theory that supports dependent products, dependent
sums and extensional identity types, among others, see e.g. (Jacobs, 1993). In
this section we outline this dependent type theory and how it is related to
$\widehat{\mathbb{D}}$. Since the constructions are largely standard, our aim
here is mainly to fix the notation for the later sections.

With the cartesian closed structure defined above, it is already possible to
use the simply-typed lambda-calculus for working with $\widehat{\mathbb{D}}$.
Morphisms of type $X_{1}\times\dots\times X_{n}\to Y$ in
$\widehat{\mathbb{D}}$ can be considered as terms
$x_{1}{:}\,X_{1},\dots,x_{n}{:}\,X_{n}\vdash t{:}\,Y$ of the simply-typed
lambda calculus. The cartesian closed structure of $\widehat{\mathbb{D}}$ is
enough to interpret abstraction and application terms. With this
correspondence, the simply-typed lambda calculus may be used as a language for
defining morphisms $\widehat{\mathbb{D}}$. Notice in particular that morphisms
$X_{1}\times\dots\times X_{n}\to Y_{1}\times\dots\times Y_{m}$ correspond to a
list of terms $(t_{1},\dots,t_{m})$ of type
$x_{1}{:}\,X_{1},\dots,x_{n}{:}\,X_{n}\vdash t_{i}{:}\,Y_{i}$ for all $i$.
Thus, morphisms $X_{1}\times\dots\times X_{n}\to Y_{1}\times\dots\times Y_{m}$
can be considered as substitutions $(t_{1}/y_{1},\dots,t_{m}/y_{m})$ of terms
in context $x_{1}{:}\,X_{1},\dots,x_{n}{:}\,X_{n}$ for the variables in
$y_{1}{:}\,Y_{1},\dots,y_{m}{:}\,Y_{m}$.

The category $\widehat{\mathbb{D}}$ has enough structure to extend this idea
to a dependently-typed lambda-calculus in a similar way. Let us first explain
how contexts, types and terms relate to the structure of
$\widehat{\mathbb{D}}$.

  * •

Contexts: Typing contexts $\Gamma$, $\Delta$ still correspond to objects of
$\widehat{\mathbb{D}}$. Also, the morphisms $\Gamma\to\Delta$ in
$\widehat{\mathbb{D}}$ still correspond to substitutions, just like in the
simply-typed case.

  * •

Types: Due to type dependencies, the types are not simply objects anymore. For
each context $\Gamma$, the set of types in context $\Gamma$ is specified by a
set $\widehat{\mathsf{Ty}}(\Gamma)$. The elements of
$\widehat{\mathsf{Ty}}(\Gamma)$ do not directly appear in
$\widehat{\mathbb{D}}$, but they induce morphisms in $\widehat{\mathbb{D}}$.
Each type $X\in\widehat{\mathsf{Ty}}(\Gamma)$ determines an object $\Gamma.X$
and a _projection map_ $p_{X}\colon\Gamma.X\to\Gamma$. The intention is that
$\Gamma.X$ represents the context $\Gamma,x{:}\,X$ and that the projection
maps represent the weakening substitution $\Gamma,x{:}\,X\to\Gamma$.

  * •

Terms: A term $\Gamma\vdash m{:}\,X$ appear as morphisms
$m\colon\Gamma\to\Gamma.X$ in $\widehat{\mathbb{D}}$ with the property
$\mathsf{id}=p_{X}\circ m$. In essence it is a substitution for the variables
in $\Gamma,x{:}\,X$ that is the identity on all variables other than $x$.

Concretely, we define the set $\widehat{\mathsf{Ty}}(\Gamma)$ to consist of
presheaves ${{\scriptstyle\int}\Gamma}^{\mathrm{op}}\to\mathpzc{Set}$, where
$\scriptstyle\int\\!\Gamma$ is the _category of elements_ of $\Gamma$, which
is defined as follows: the objects of $\scriptstyle\int\\!\Gamma$ are the set
$\\{(\Psi,g)\mid g\in\Gamma(\Psi)\\}$ and the morphisms $\sigma$ between
$(\Psi,g)\to(\Phi,g^{\prime})$ are induced from $\sigma:\Psi\to\Phi$ subject
to $g=\Gamma(\sigma,g^{\prime})$. We can show that this construction does form
a category. Intuitively, this construction use morphisms in $\mathbb{D}$ as
coherence conditions, which are respected in all other constructions in the
presheaf model.

For a presheaf $X:{{\scriptstyle\int}\Gamma}^{\mathrm{op}}\to\mathpzc{Set}$ in
$\widehat{\mathsf{Ty}}(\Gamma)$, we define the presheaf $\Gamma.X$ in
$\widehat{\mathbb{D}}$ by $(\Gamma.X)(\Phi)=\\{(g,x)\mid g\in\Gamma(\Phi),\
x\in X(\Phi,g)\\}$ with the canonical action on morphisms. The projection map
$p_{X}$ is just the first projection.

This interpretation of types generalizes the simply-typed case. Any object $X$
of $\widehat{\mathbb{D}}$ can be seen as a simple type. It can be lifted to a
presheaf in
$\overline{X}:{{\scriptstyle\int}\Gamma}^{\mathrm{op}}\to\mathpzc{Set}$ in
$\widehat{\mathsf{Ty}}(\Gamma)$ by letting $\overline{X}(\Phi,g)=X(\Phi)$.
Note that with this choice, $\Gamma.\overline{X}$ is identical to
$\Gamma\times X$, as one would expect from the simply-typed case.

With type dependencies, one needs a substitution operation on types. For any
$\sigma\colon\Delta\to\Gamma$, there is a type substitution function
$(-)\\{\sigma\\}$ from $\widehat{\mathsf{Ty}}(\Gamma)$ to
$\widehat{\mathsf{Ty}}(\Delta)$. It maps $X:\widehat{\mathsf{Ty}}(\Gamma)$ to

$\displaystyle
X\\{\sigma\\}(\Phi:\mathbb{D},d:\Delta(\Phi)):=X(\Phi,\sigma(\Phi,d))$

The definition of $\widehat{\mathsf{Ty}}(\Gamma)$ justifies the intuition of
contexts as types of tuples as in the simply-typed case. Consider, for
example, a context of the form $(\top.X).Y$ for some types
$X\in\widehat{\mathsf{Ty}}(\top)$ and $Y\in\widehat{\mathsf{Ty}}(\top.X)$. The
presheaf $(\top.X).Y$ is defined such that the elements of
$((\top.X).Y)(\Phi)$ have the form $((*,x),y)$ for some $x$ and $y$. $*$ is
the only element of a uniquely chosen singleton set in $\mathpzc{Set}$. One
should think of them as representing values of the variables of the context
$x{:}\,X,y{:}\,Y$.

All presheaf categories also support dependent function spaces (Hofmann,
1997). For $X:\widehat{\mathsf{Ty}}(\Gamma)$ and
$Y:\widehat{\mathsf{Ty}}(\Gamma.X)$, we write
$\widehat{\Pi}(X,Y):\widehat{\mathsf{Ty}}(\Gamma)$ for the dependent function
space. This is defined to be

$\displaystyle\widehat{\Pi}(X,Y)(\Phi:\mathbb{D},d:\Gamma(\Phi)):=\\{f$
$\displaystyle:(\Psi:\mathbb{D})(\delta:\Psi\to\Phi)(x:X(\Psi,\Gamma(\delta,d)))\to
Y(\Psi,(\Gamma(\delta,d),x))$
$\displaystyle\mid\forall\Psi,\delta,x,\Psi^{\prime},\delta^{\prime}:\Psi^{\prime}\to\Psi.\,f(\Psi^{\prime},\delta\circ\delta^{\prime},X(\delta^{\prime},x))=Y(\delta^{\prime},f(\Psi,\delta,x))\
\\}$

$\widehat{\Pi}(X,Y)$ is a set of functions the values of which are coherent
under the morphisms of the base category $\mathbb{D}$. We can show that this
definition of $\widehat{\Pi}$ types respect type substitutions.

This outlines how the structure of $\widehat{\mathbb{D}}$ relates to dependent
type theory, see e.g. (Jacobs, 1993) for more details. We will use this type
theory as a convenient internal language to work with the structure of
$\widehat{\mathbb{D}}$. It is well-known that $\widehat{\mathbb{D}}$ has
enough structure to support dependent sums and extensional identity types,
among others in its internal dependent type theory, see e.g. (Jacobs, 1993).
We do not need to spell out the details of their interpretation.

We use Agda notation for the types and terms of this internal dependent type
theory. We write $(x{:}\,S)\to T$ for a dependent function type and write
$\leftthreetimes x{:}\,S.m$ and $m\ n$ for the associated lambda-abstractions
and applications. As usual, we will sometimes also write $S\to T$ for
$(x{:}\,S)\to T$ if $x$ does not appear in $T$. However, to make it easier to
distinguish the function spaces at various levels, we will write $(x{:}\,S)\to
T$ by default even when $x$ does not appear in $T$. We use $\texttt{let}\ x=m\
\texttt{in}\ n$ as an abbreviation for $(\leftthreetimes x{:}\,T.n)~{}m$, as
usual. For two terms $m{:}\,T$ and $n{:}\,T$, we write $m=_{T}n$ or just $m=n$
for the associated identity type.

In the spirit of Martin-Löf type theory, we will identify the basic types and
terms needed for our constructions successively as they are needed. In the
following sections, we will expose the structure of $\widehat{\mathbb{D}}$
step by step until we have enough to interpret contextual types.

While much of the structure of $\widehat{\mathbb{D}}$ can be captured by
adding rules and constants to standard Martin-Löf type theory, for the comonad
$\flat$ such a formulation would not be very satisfactory. The issues are
discussed by Shulman (2018, p.7), for example. To obtain a more satisfactory
syntax for the comonad, we refine the internal type theory into a modal type
theory in which $\flat$ appears as a necessity modality. This approach goes
back to Benton et al. (1993); Barber and Plotkin (1996); Davies and Pfenning
(2001) and is also used by recent work of Shulman (2018); Licata et al. (2018)
and others on working with the $\flat$-modality in type theory.

We summarise here the typing rules for the $\flat$-modality which we will rely
on. To control the modality, one uses two kinds of variables. In addition to
standard variables $x{:}\,T$, one has a second kind of so-called _crisp_
variables $x{::}T$. Typing judgements have the form $\Delta\mid\Theta\vdash
m{:}\,T$, where $\Delta$ collects the crisp variables and $\Theta$ collects
the ordinary variables. In essence, a crisp variable $x{::}T$ represents an
assumption of the form $x{:}\,\flat T$. The syntactic distinction is useful,
since it leads to a type theory that is well-behaved with respect to
substitution (Davies and Pfenning, 2001; Shulman, 2018).

The typing rules are closely related to those in modal type systems (Davies
and Pfenning, 2001; Nanevski et al., 2008), where $\Delta$ is the typing
context for modal (global) assumptions and $\Theta$ for (local) assumptions,
and type systems for linear logic (Barber and Plotkin, 1996), where $\Delta$
is the typing context for non-linear assumptions and $\Theta$ for linear
assumptions.  * Δ, u::T, Δ’ ∣Θ⊢u : T

* Δ∣Θ, x: T, Θ’ ⊢x : T

* Δ∣⋅⊢m : T Δ∣Θ⊢box m : ♭T

* Δ∣Θ⊢m : ♭T
Δ, x::T ∣Θ⊢n : S Δ∣Θ⊢let box x = m in n : S  Given any term $m\colon T$ which
only depends on modal variable context $\Delta$, we can form the term
$\mathsf{box}~{}m\colon\flat T$. We have a let-term
$\texttt{let}~{}\texttt{box}~{}x=m\ \texttt{in}\ n$ that takes a term
$m\colon\flat T$ and binds it to a variable $x{::}T$. The rules maintain the
invariant that the free variables in a type $\flat T$ are all crisp variables
from the crisp context $\Delta$.

The model has other structures. For example, the rules for dependent products
are:

$\prooftree\Hypo{\Delta\mid\Theta,x{:}\,T\vdash m{:}\,S}\Infer
1[]{\Delta\mid\Theta\vdash\leftthreetimes x{:}T.m:(x{:}T)\to
S}\quad\prooftree\Hypo{\Delta\mid\Theta\vdash m{:}\,(y{:}T)\to
S\quad\Delta\mid\Theta\vdash n{:}\,T}\Infer 1[]{\Delta\mid\Theta\vdash
m~{}n{:}\,[n/y]S}$

Though the dependent function space is supported by the model, in our
interpretation, we only use the simple function space. It is also convenient
to have a crisp variant of abstractions and applications (Nanevski et al.,
2008):

$\prooftree\Hypo{\Delta,u{::}T\mid\Theta\vdash m{:}\,S}\Infer
1[]{\Delta\mid\Theta\vdash\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}u{::}T.m:(u{::}T)\to^{\flat}S}\quad\prooftree\Hypo{\Delta\mid\Theta\vdash
m{:}\,(u{::}T)\to^{\flat}S\quad\Delta\mid\cdot\vdash n{:}\,T}\Infer
1[]{\Delta\mid\Theta\vdash m~{}n{:}\,[n/u]S}$

The superscripts $\flat$ of $\leftthreetimes$ and $\to$ indicate that we are
referring to the crisp variant. Notice that in the application rule, $n$ is
necessarily closed, i.e. the local context of $n$ is empty. These rules allow
us to directly operate on crisp variables, and we will interpret computation-
level functions of Cocon to this crisp function space. Despite its
convenience, the full effect of introducing crisp functions to a comonadic
modality type theory is still unclear and we leave its investigation to the
future. In this paper, however, we do not make use of its full strength, but
just use the syntax as a notation for the semantic interpretation.

When $\Delta$ is empty, we shall write just $\Theta\vdash m{:}\,T$ for
$\Delta\mid\Theta\vdash m{:}\,T$.

Let us outline the categorical interpretation of the modality rules. First
recall from above that $\flat$ is a comonad on $\widehat{\mathbb{D}}$. For any
type $X\in\widehat{\mathsf{Ty}}(\Delta)$ we define the type $\flat
X\in\widehat{\mathsf{Ty}}(\flat\Delta)$ by $(\flat X)(\Phi,d)=X(\top,d)$.
Notice that this is well-defined, since $d\in(\flat\Delta)(\Psi)$ implies
$d\in\Delta(\top)$ for all $\Psi$, by definition of $\flat$. Notice that the
definition of $\flat X$ makes $\flat(\Delta.X)$ the same as $\flat\Delta.\flat
X$.

Since $\Delta$ only contains crisp variables, types in it are represented as
$\flat X$. In general, when a type $T$ appears in a context
$\Delta\mid\Theta$, it is a type in
$\widehat{\mathsf{Ty}}(()\flat\Delta.\Theta)$.

A variable lookup into the crisp context requires application of the counit
$\epsilon$. Consider

$\displaystyle v:\flat\Delta\to\flat\Delta.\flat T$

which is the variable projection of the crisp context. We further need to
unwrap $\flat T$ using $\epsilon:\flat T\to T$. Thus we need another natural
transformation:

$\displaystyle h$ $\displaystyle:\flat\Delta.\flat T\to\flat\Delta.T$
$\displaystyle h(\Psi)$ $\displaystyle=(id_{\flat\Delta},\epsilon_{\Psi})$

Thus we have $h\circ v:\flat\Delta\to\flat\Delta.T$. We can show that this
natural transformation is a section of the projection map, due to the first
component in $h$ is an identity morphism. General variable lookups in the
crisp context can then be obtained by weakening.

To model box, let us first consider a section natural transformation
$\flat\Delta\to\flat\Delta.\flat T$ given another section
$m:\flat\Delta\to\flat\Delta.T$. Though there might be a more general
formulation, we take advantage of the fact that $\flat$ is idempotent in our
model, and we can immediately have $\flat m$ to be the desired natural
transformation, because $\flat\flat\Delta=\flat\Delta$. The general box with
$\Theta$ can be obtained by weakening.

The interpretation of $\texttt{let}~{}\texttt{box}~{}x=m\ \texttt{in}\ n$ is
relatively easier. We consider as an example the special case where $\Theta$
is empty. Given $m:\flat\Delta\to\flat\Delta.\flat T$ and $n:\flat\Delta.\flat
T\to\flat\Delta.\flat T.S$, we can just apply $m$ as a substitution to $n$:
$n\\{m\\}:\flat\Delta\to\flat\Delta.S\\{m\\}$.

Thus we see that the syntax can be interpreted as categorical constructs. In
the rest of the paper, we use syntactic translations to simplify our
presentation.

##  4\. From Presheaves to Contextual Types

Armed with the internal type theory, we can now explore the structure of
$\widehat{\mathbb{D}}$.

###  4.1. A Universe of Representables

For our purposes, the main feature of $\widehat{\mathbb{D}}$ is that it embeds
$\mathbb{D}$ fully and faithfully via the Yoneda embedding. In the type theory
for $\widehat{\mathbb{D}}$, we may capture this embedding by means of a
Tarski-style universe. Such a universe is defined by a type of codes Obj for
the objects of $\mathbb{D}$ together with a decoding function that maps these
codes into types of the type theory for $\widehat{\mathbb{D}}$.

Let Obj be the set of objects of $\mathbb{D}$. Recall from above, that any set
can be considered as a constant presheaf with the trivial substitution action,
and thus as a type in the internal type theory of $\widehat{\mathbb{D}}$. The
terms of this type Obj represent objects of $\mathbb{D}$. The cartesian closed
structure of $\mathbb{D}$ gives us terms unit, times, arrow for the terminal
object $\top$, finite products $\times$ and the exponential (function type).
We also have a term for the domain-level type tm.

$\displaystyle\vdash\texttt{Obj}\ \text{type}$
$\displaystyle\vdash\texttt{tm}\colon\texttt{Obj}$
$\displaystyle\vdash\texttt{times}\colon(a{:}\,\texttt{Obj})\to(b{:}\,\texttt{Obj})\to\texttt{Obj}$
$\displaystyle\vdash\texttt{unit}\colon\texttt{Obj}$
$\displaystyle\vdash\texttt{arrow}\colon(a{:}\,\texttt{Obj})\to(b{:}\,\texttt{Obj})\to\texttt{Obj}$

Subsequently, we sometimes talk about objects of $\mathbb{D}$ when we intend
to describe terms of type Obj (and vice versa).

The morphisms of $\mathbb{D}$ could similarly be encoded as a presheaf with
many term constants, but this is in fact not necessary. Instead, we can use
the Yoneda embedding to decode elements of Obj into actual types. To this end,
we use the following:

$x{:}\,\texttt{Obj}\vdash\texttt{El}\,x\ \text{type}$

The type El is almost direct syntax for the Yoneda embedding. The
interpretation of El in $\widehat{\mathbb{D}}$, given in detail below, is such
that, for any object $A$ of $\mathbb{D}$, the type $\texttt{El}\,A$ is
interpreted by the presheaf $\mathrm{y}(A)$. Such a presheaf is called
_representable_. One can think of $\texttt{El}\,A$ as the type of all
morphisms of type $\Psi\to A$ in $\mathbb{D}$ for arbitrary $\Psi$. Recall
from above that a morphism of type $\Psi\to A$ in $\mathbb{D}$ amounts to a
domain-level term of type $A$ that may refer to variables in $\Psi$. In this
sense, one should think of $\texttt{El}\,A$ as a type of domain-level terms of
type $A$, both closed and open ones.

That $\texttt{El}\,A$ is interpreted by $\mathrm{y}A$ means that all
constructions on $\texttt{El}\,A$ in the internal type theory are guaranteed
to be substitution invariant. In particular, since the Yoneda embedding is
full and faithful, recall Section 2, the type of functions
$(x{:}\,\texttt{El}\,A)\to\texttt{El}\,B$ corresponds to the morphisms of type
$A\to B$ in $\mathbb{D}$. Any closed term of type
${(x:\texttt{El}\,A)}\to\texttt{El}\,B$ corresponds to such a morphism $A\to
B$ in $\mathbb{D}$ and vice versa. This is because $\texttt{El}\,A$ and
$\texttt{El}\,B$ correspond to $\mathrm{y}A$ and $\mathrm{y}B$ respectively
and the naturality requirements in $\widehat{\mathbb{D}}$ enforce
substitution-invariance, as outlined in Section 2. The type
$(x:\texttt{El}\,A)\to\texttt{El}\,B$ thus does not represent arbitrary
functions from terms of type $A$ to terms of type $B$, but only substitution-
invariant ones. If a function of this type maps a domain-level variable
$x{:}\,A$ (encoded as an element of $\texttt{El}\,A$) to some term $M{:}\,B$
(encoded as an element of $\texttt{El}\,B$), then it must map any other
$N{:}\,A$ to $[N/x]M$.

In more detail, the interpretation of
$\texttt{Obj}\in\widehat{\mathsf{Ty}}(\top)$ and
$\texttt{El}\,\in\widehat{\mathsf{Ty}}(\texttt{Obj})$ of the above types in
the internal type theory of $\widehat{\mathbb{D}}$ is given by:

$\displaystyle\texttt{Obj}(\Psi,*)$ $\displaystyle=\\{\Phi\mid\text{$\Phi$ is
an object of $\mathbb{D}$}\\}$ $\displaystyle\texttt{El}\,(\Psi,\Phi)$
$\displaystyle=\mathbb{D}(\Psi,\Phi)$ $\displaystyle\texttt{Obj}(\sigma)$
$\displaystyle:\Phi\mapsto\Phi$ $\displaystyle\texttt{El}\,(\sigma)$
$\displaystyle:f\mapsto f\circ\sigma$

Notice in particular that
$(\texttt{Obj}.\texttt{El}\,)(\Psi)=\\{(\Phi,f)\mid\text{$\Phi$ is object of
$\mathbb{D}$},f\in\mathbb{D}(\Psi,\Phi)\\}$. If, for any object $A$ in
$\mathbb{D}$, we substitute along the corresponding constant function
$A\colon\top\to\texttt{Obj}$, then we obtain
$(\top.\texttt{El}\,\\{A\\})(\Phi)=\\{(A,f)\mid f\in\mathbb{D}(\Phi,A)\\}$.
This presheaf is isomorphic to $\mathrm{y}A$.

We note that, while type dependencies often make it difficult to spell out
types directly in terms of the categorical structure of
$\widehat{\mathbb{D}}$, type dependencies on constant presheaves like Obj are
relatively easy to work with. This is because Obj is just a set, so that the
naturality constraints of $\widehat{\mathbb{D}}$ are vacuous for functions out
of Obj. Instead of working with the dependent type directly, we can just work
with all its instances. For example, a term of type
$(a{:}\,\texttt{Obj})\to(b{:}\,\texttt{Obj})\to(x{:}\,\texttt{El}\,a)\to\texttt{El}\,b$
is uniquely determined by a family of terms
$(x{:}\,\texttt{El}\,A)\to\texttt{El}\,B$ indexed by objects $A$ and $B$ in
$\mathbb{D}$. We have the following lemma, which states that functions out of
Obj have independent values for all arguments.

###### Lemma 4.1.

In the internal type theory of $\widehat{\mathbb{D}}$, a closed term
$t\colon(a{:}\,\texttt{Obj})\to X$ is in one-to-one correspondence with a
family of closed terms $(t_{A})_{A\in\texttt{Obj}}$ such that $t_{A}\colon
X[A/a]$. In particular, there is no uniformity condition on this family, i.e.
for different objects $A$ and $B$, the terms $t_{A}$ and $t_{B}$ may be
arbitrary unrelated terms of types $X[A/a]$ and $X[B/a]$.

Notice that such a lemma would not be true, e.g., with $\texttt{El}\,A$
instead of Obj. We have seen above that functions of type
$\texttt{El}\,A\to\texttt{El}\,B$ correspond to morphisms of type $A\to B$ in
$\mathbb{D}$. By definition of $\mathbb{D}$, a morphism $A\to B$ corresponds
to a domain-level term $x{:}\,A\vdash t\colon B$. Such terms are not in one-
to-one correspondence with families of closed terms of type $B$ indexed by
closed terms of type $A$.

To summarise this section, by considering the Yoneda embedding as a decoding
function El of a universe á la Tarski, we get access to $\mathbb{D}$ in the
internal type theory of $\widehat{\mathbb{D}}$. Since the universe consists of
the representable presheaves, we call it the _universe of representables_.

The following lemmas state that the embedding preserves terminal object,
binary products and the exponential.

###### Lemma 4.2.

The internal type theory of $\widehat{\mathbb{D}}$ has a term
$\vdash\texttt{terminal}\colon\texttt{El}\,\texttt{unit}$, such that
$x=\texttt{terminal}$ holds for any $x\colon\texttt{El}\,\texttt{unit}$.

###### Lemma 4.3.

The internal type theory of $\widehat{\mathbb{D}}$ justifies the terms below,
such that $\texttt{fst}\ (\texttt{pair}\ x\ y)=x$, $\texttt{snd}\
(\texttt{pair}\ x\ y)=y$, $z=\texttt{pair}\ (\texttt{fst}\ z)\ (\texttt{snd}\
z)$ for all $x,y,z$.

$\begin{aligned}
c{:}\,\texttt{Obj},\,d{:}\,\texttt{Obj}&\vdash\texttt{fst}\colon(z:\texttt{El}\,(\texttt{times}\
c\ d))\to\texttt{El}\,c\\\
c{:}\,\texttt{Obj},\,d{:}\,\texttt{Obj}&\vdash\texttt{snd}\colon(z:\texttt{El}\,(\texttt{times}\
c\ d))\to\texttt{El}\,d\\\
c{:}\,\texttt{Obj},\,d{:}\,\texttt{Obj}&\vdash\texttt{pair}\colon(x:\texttt{El}\,c)\to(y:\texttt{El}\,d)\to\texttt{El}\,(\texttt{times}\
c\ d)\end{aligned}$

###### Lemma 4.4.

The internal type theory of $\widehat{\mathbb{D}}$ justifies the terms below
such that $\texttt{arrow-i}\ (\texttt{arrow-e}\ f)=f$ and $\texttt{arrow-e}\
(\texttt{arrow-i}\ g)=g$ for all $f,g$.

$\begin{aligned}
c{:}\,\texttt{Obj},\,d{:}\,\texttt{Obj}&\vdash\texttt{arrow-e}\colon(x{:}\,\texttt{El}\,(\texttt{arrow}\
c\ d))\to(y{:}\,\texttt{El}\,c)\to\texttt{El}\,d\\\
c{:}\,\texttt{Obj},\,d{:}\,\texttt{Obj}&\vdash\texttt{arrow-i}\colon(y{:}\,(\texttt{El}\,c\to\texttt{El}\,d))\to\texttt{El}\,(\texttt{arrow}\
c\ d)\end{aligned}$

###### Proof.

Lemmas 4.2 and 4.3 are consequences of the preservation of limits of the
Yoneda embedding.

For Lemma 4.4, it suffices, by Lemma 4.1, to establish an isomorphism between
$\texttt{El}\,(\texttt{arrow}\ A\ B)$ and
$(y{:}\,\texttt{El}\,A)\to\texttt{El}\,B$ for all objects $A$ and $B$ of
$\mathbb{D}$. By definition of El , this amounts to preservation of
exponentials by $\mathrm{y}$. The goal follows because we have the following
isomorphisms, which are natural in $\Gamma$:

$\displaystyle(\mathrm{y}A\Rightarrow\mathrm{y}B)(\Gamma)$ $\displaystyle\
\cong\
\widehat{\mathbb{D}}(\mathrm{y}\Gamma,\mathrm{y}A\Rightarrow\mathrm{y}B)\
\cong\ \widehat{\mathbb{D}}(\mathrm{y}\Gamma\times\mathrm{y}A,\mathrm{y}B)$
$\displaystyle\ \cong\ \widehat{\mathbb{D}}(\mathrm{y}(\Gamma\times
A),\mathrm{y}B)\ \cong\ \mathbb{D}(\Gamma\times A,B)$ $\displaystyle\ \cong\
\mathbb{D}(\Gamma,A\Rightarrow B)\ \cong\
\widehat{\mathbb{D}}(\mathrm{y}\Gamma,\mathrm{y}(A\Rightarrow B))\ \cong\
\mathrm{y}(A\Rightarrow B)(\Gamma)$

∎

###  4.2. Higher-Order Abstract Syntax

The last lemma in the previous section states that
$\texttt{El}\,A\to\texttt{El}\,B$ is isomorphic to
$\texttt{El}\,(\texttt{arrow}\ A\ B)$. This is particularly useful to lift
HOAS-encodings from $\mathbb{D}$ to $\widehat{\mathbb{D}}$. For instance, the
domain-level term constant lam: (tm $\rightarrow~{}$ tm) $\rightarrow~{}$ tm
gives rise to an element of $\texttt{El}\,(\texttt{arrow}\ (\texttt{arrow}\
\texttt{tm}\ \texttt{tm})\ \texttt{tm})$. But this type is isomorphic to
$(\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm})\to\texttt{El}\,\texttt{tm}$,
by the lemma.

This means that the higher-order abstract syntax constants lift to
$\widehat{\mathbb{D}}$:

app
$\displaystyle\colon(m{:}\,\texttt{El}\,\texttt{tm})\to(n{:}\,\texttt{El}\,\texttt{tm})\to\texttt{El}\,\texttt{tm}$
lam
$\displaystyle\colon(m{:}\,(\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm}))\to\texttt{El}\,\texttt{tm}$

Once one recognises $\texttt{El}\,A$ as $\mathrm{y}(A)$, the adequacy of this
higher-order abstract syntax encoding lifts from $\mathbb{D}$ to
$\widehat{\mathbb{D}}$ as in Hofmann (1999). For example, an argument $M$ to
lam has type $\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm}$, which is
isomorphic to $\texttt{El}\,(\texttt{arrow}\ \texttt{tm}\ \texttt{tm})$. But
this type represents (open) domain-level terms
$t\colon\texttt{tm}\to\texttt{tm}$. The term $\texttt{lam}\
M\colon\texttt{El}\,\texttt{tm}$ then represents the domain-level term
$\texttt{lam}\ t\colon\texttt{tm}$, so it just lifts the domain-level.

###  4.3. Closed Objects

One should think of $\flat T$ as the type of ‘closed’ elements of $T$. In
particular, $\flat(\texttt{El}\,A)$ represents morphisms of type $\top\to A$
in $\mathbb{D}$, recall the definition of $\flat$ from Section 2 and that
$\texttt{El}\,A$ corresponds to $\mathrm{y}A$. In the term model $\mathbb{D}$,
the morphisms $\top\to A$ correspond to closed domain-language terms of type
$A$. Thus, while $\texttt{El}\,A$ represents both open and closed domain-level
terms, $\flat(\texttt{El}\,A)$ represents only the closed ones.

This applies also to the type $\texttt{El}\,A\to\texttt{El}\,B$. We have seen
above that $\texttt{El}\,A\to\texttt{El}\,B$ is isomorphic to
$\texttt{El}\,(\texttt{arrow}\ A\ B)$ and may therefore be thought of as
containing the terms of type $B$ with a distinguished variable of type $A$.
But, these terms may contain other free domain language variables. The type
$\flat(\texttt{El}\,A\to\texttt{El}\,B)$, on the other hand, contains only
terms of type $B$ that may contain (at most) one variable of type $A$.

Restricting to closed objects with the modality is useful because it disables
substitution-invariance. For example, the internal type theory for
$\widehat{\mathbb{D}}$ justifies a function $\texttt{is-
lam}\colon(x{:}\flat(\texttt{El}\,\texttt{tm}))\to\texttt{bool}$ that returns
true if and only if the argument represents an object language lambda
abstraction. We shall define it in the next section. Such a function cannot be
defined with type $\texttt{El}\,\texttt{tm}\to\texttt{bool}$, since it would
not be invariant under substitution. Its argument ranges over terms that may
be open; which particularly includes domain-level variables. The function
would have to return false for them, since a domain-level variable is not a
lambda-abstraction. But after substituting a lambda-abstraction for the
variable, it would have to return true, so it could not be substitution-
invariant.

We note that the type Obj consists only of closed elements and that Obj and
$\flat\texttt{Obj}$ happen to be definitionally equal types (an isomorphism
would suffice, but equality is more convenient).

###  4.4. Contextual Objects

Using function types and the modality, it is now possible to work with
contextual objects that represent domain level terms in a certain context,
much like in Pientka (2008); Pientka and Abel (2015). A contextual type
$\lceil\Psi\vdash A\rceil$ is a boxed function type of the form
$\flat(\texttt{El}\,\Psi\to\texttt{El}\,A)$. It represents domain-level terms
of type $A$ with variables from $\Psi$. Here, we consider the domain-level
context $\Psi$ as a term that encodes it. The interpretation will make this
precise.

For example, domain-level terms with up to two free variables now appear as
terms of type

$\flat(\texttt{El}\,((\texttt{times}\ (\texttt{times}\ \texttt{unit}\
\texttt{tm})\ \texttt{tm})\to\texttt{El}\,\texttt{tm}),$

as the following example illustrates.

$\begin{array}[]{ll}\mathsf{box}~{}(\leftthreetimes
u{:}\,\texttt{El}\,((\texttt{times}\ (\texttt{times}\ \texttt{unit}\
\texttt{tm})\ \texttt{tm}).&\texttt{let}\ x_{1}=\texttt{snd}\ (\texttt{fst}\
u)\ \texttt{in}\\\ &\texttt{let}\ x_{2}={\texttt{snd}\ u}\ \texttt{in}\\\
&\quad{\texttt{app}\ (\texttt{lam}\ (\leftthreetimes
x{:}\,\texttt{El}\,\texttt{tm}.\,\texttt{app}\ x_{1}\ x))\
x_{2}~{})}\end{array}$

Here, the variables $x_{1}$ and $x_{2}$ are bound at the meta level, i.e. the
internal language. As we will see in the next section, the example interprets
the open domain-level term $\texttt{app}\ (\texttt{lam}\ (\lambda
x.\texttt{app}\ x_{1}\ x))\ x_{2}$ with domain-level variables
$x_{1}{:}\texttt{tm}$ and $x_{2}{:}\texttt{tm}$.

This representation integrates substitution as usual. For example, given crisp
variables $m{::}\texttt{El}\,({\texttt{times}\ c\ \texttt{tm}})\to\texttt{tm}$
and $n{::}\texttt{El}\,c\to\texttt{tm}$ for contextual terms, the term
$\mathsf{box}~{}(\leftthreetimes u{:}\,\texttt{El}\,c.\,m\ (\texttt{pair}\ u\
(n\ u)))$ represents substitution of $n$ for the last variable in the context
of $m$.

For working with contextual objects, it is convenient to lift the constants
app and lam to contextual types.

$\displaystyle c{:}\,\texttt{Obj}$
$\displaystyle\vdash\texttt{app}^{\prime}\colon\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm})\to\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm})\to\flat{(\texttt{El}\,c\to\texttt{tm})}$
$\displaystyle c{:}\texttt{Obj}$
$\displaystyle\vdash\texttt{lam}^{\prime}\colon\flat(\texttt{El}\,(\texttt{times}\
c\
\texttt{tm})\to\texttt{El}\,\texttt{tm})\to\flat{(\texttt{El}\,c\to\texttt{El}\,\texttt{tm})}$

These terms are defined by:

$\begin{array}[]{lcl}\texttt{app}^{\prime}&:=&\leftthreetimes
m,n.\,\texttt{let}~{}\texttt{box}~{}{m^{\prime}}={m}\ \texttt{in}\
\texttt{let}~{}\texttt{box}~{}{n^{\prime}}={n}\ \texttt{in}\\\
&&\quad\quad\quad~{}~{}\mathsf{box}~{}(\leftthreetimes
u{:}\,\texttt{El}\,c.\,\texttt{app}\ (m^{\prime}\ u)\ (n^{\prime}\ u))\\\
\texttt{lam}^{\prime}&:=&\leftthreetimes
m.\,\texttt{let}~{}\texttt{box}~{}m^{\prime}=m\ \texttt{in}\
\mathsf{box}~{}(\leftthreetimes u{:}\,\texttt{El}\,c.\,\texttt{lam}\
(\leftthreetimes x{:}\,\texttt{El}\,\texttt{tm}.\,\ m^{\prime}\
(\texttt{pair}\ u\ x)))\end{array}$

A contextual type for domain-level variables (as opposed to arbitrary terms)
can be defined by restricting the function space in
$\flat(\texttt{El}\,\Psi\to\texttt{El}\,A)$ to consist only of projections.
Projections are functions of the form $\texttt{snd}\circ\texttt{fst}^{k}$,
where we write $\texttt{fst}^{k}$ for the $k$-fold iteration
$\texttt{fst}\circ\dots\circ\texttt{fst}$. Let us write
$\texttt{El}\,\Psi\to_{v}\texttt{El}\,A$ for the subtype of
$\texttt{El}\,\Psi\to\texttt{El}\,A$ consisting only of projections. The
contextual type $\flat(\texttt{El}\,\Psi\to_{v}\texttt{El}\,A)$ is then a
subtype of $\flat(\texttt{El}\,\Psi\to\texttt{El}\,A)$.

With these definitions, we can express a primitive recursion scheme for
contextual types. We write it in its general form where the result type $A$
can possibly depend on $x$. This is only relevant for the dependently typed
case; in the simply typed case, the only dependency is on $c$.

###### Lemma 4.5.

Let
$c{:}\,\texttt{Obj},\,x{:}\,\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm})\vdash
A\ c\ x\ \text{type}$ and define:

$\small\begin{aligned}
X_{\texttt{var}}&:=(c{:}\,\texttt{Obj})\to(x{:}\,\flat(\texttt{El}\,c\to_{v}\texttt{El}\,\texttt{tm}))\to
A\ {c}\ x\\\
X_{\texttt{app}}&:=(c{:}\,\texttt{Obj})\to(x,y{:}\,\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm}))\to\,A\
c\ x\to A\ {c}\ y\to A\ c\ (\texttt{app}^{\prime}~{}x~{}\ {y})\\\
X_{\texttt{lam}}&:=(c{:}\,\texttt{Obj})\to(x{:}\,\flat(\texttt{El}\,({\texttt{times}\
c\ \texttt{tm}})\to\texttt{El}\,\texttt{tm}))\to A\ (\texttt{times}\ c\
\texttt{tm})\ x\to A\ {c}\ (\texttt{lam}^{\prime}~{}x)\end{aligned}$

Then, $\widehat{\mathbb{D}}$ justifies a term

$\vdash\texttt{rec}\colon X_{\texttt{var}}\to X_{\texttt{app}}\to
X_{\texttt{lam}}\to(c{:}\,\texttt{Obj})\to(x{:}\,\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm}))\to\,A~{}c\
x$

such that the following equations are valid.

$\begin{array}[]{lcl}\texttt{rec}\ t_{\texttt{var}}\ t_{\texttt{app}}\
t_{\texttt{lam}}~{}c\ x&=&t_{\texttt{var}}~{}c\ x\text{\hskip 56.9055pt
\text{if $x{:}\,\flat(\texttt{El}\,c\to_{v}\texttt{El}\,\texttt{tm})$ }}\\\
\texttt{rec}\ t_{\texttt{var}}\ t_{\texttt{app}}\ t_{\texttt{lam}}~{}c\
(\texttt{app}^{\prime}~{}s~{}t)&=&t_{\texttt{app}}~{}c\ s\ t\\\ \texttt{rec}\
t_{\texttt{var}}\ t_{\texttt{app}}\ t_{\texttt{lam}}~{}c\
(\texttt{lam}^{\prime}~{}s)&=&t_{\texttt{lam}}~{}c\ s\end{array}$

###### outline.

To outline the proof idea, note first that a function of type
$(c{:}\,\texttt{Obj})\to(x{:}\,\flat(\texttt{El}\,c\to\texttt{El}\,\texttt{tm}))\to\,A\
c\ x$ in $\widehat{\mathbb{D}}$, corresponds to an inhabitant of $A\ \Phi\ t$
for each concrete object $\Phi$ of $\mathbb{D}$ and each inhabitant
$t\colon\flat(\texttt{El}\,\Phi\to\texttt{El}\,\texttt{tm})$. This is because
naturality constraints for boxed types are vacuous (and
$\texttt{Obj}=\flat\texttt{Obj}$). Next, note that inhabitants of
$\flat(\texttt{El}\,\Phi\to\texttt{El}\,\texttt{tm})$ correspond to domain-
level terms of type tm in context $\Phi$ up to $\alpha\beta\eta$-equality. We
can perform a case-distinction on whether it is a variable, abstraction or
application and depending on the result use $t_{\texttt{var}}$,
$t_{\texttt{app}}$ or $t_{\texttt{lam}}$ to define the required inhabitant of
$A\ \Phi\ t$. ∎

As a simple example for rec, we can define the function is-lam discussed above
by
$\texttt{rec}\ (\leftthreetimes c,x.\,\texttt{false})\ (\leftthreetimes
c,x,y,r_{x},r_{y}.\,\texttt{false})\ (\leftthreetimes
c,x,r_{x}.\,\texttt{true})$.

##  5\. Simple Contextual Modal Type Theory

We have outlined informally how the internal dependent type theory of
$\widehat{\mathbb{D}}$ can model contextual types. In this section, we make
this precise by giving the interpretation of Cocon (Pientka et al., 2019), a
contextual modal type theory where we can work with contextual HOAS trees and
computations about them, into $\widehat{\mathbb{D}}$. We will focus here on a
simply-typed version of Cocon where we use a simply-typed domain-language with
constants app and lam and also only allow computations about HOAS trees, but
do not consider, for example, universes. Concentrating on a stripped down,
simply-typed version of Cocon allows us to focus on the essential aspects,
namely how to interpret domain-level contexts and domain-level contextual
objects and types semantically. The generalisation to a dependently typed
domain-level such as LF in Section 6 will be conceptually straightforward,
although more technical. Handling universes is an orthogonal issue.

${{{{{{{{{{{{{{\begin{array}[]{p{4.8cm}@{~}l@{~}r@{~}l}Domain-level
types}}~{&A,B\hfil~{}&\;\mathrel{::=}~{}&\texttt{tm}\,\mid\,A\to B\\\ Domain-
level terms}}~{&M,N\hfil~{}&\;\mathrel{::=}~{}&\lambda x.M\mid M\,N\mid
x\mid\mathsf{lam}\,\mid\,\mathsf{app}\mid\lfloor t\rfloor_{\sigma}\\\ Domain-
level
contexts}}~{&\Psi,\Phi\hfil~{}&\;\mathrel{::=}~{}&\cdot\,\mid\,\psi\,\mid\,\Psi,x{:}A\\\
Domain-level context
(erased)}}~{&\widehat{\Psi},\widehat{\Phi}\hfil~{}&\;\mathrel{::=}~{}&\cdot\,\mid\,\psi\,\mid\,\widehat{\Psi},x\\\
Domain-level
substitutions}}~{&\sigma\hfil~{}&\;\mathrel{::=}~{}&\cdot\,\mid\,\mathsf{wk}_{\widehat{\Psi}}\,\mid\,\sigma,M\\\\[2.25pt]
\hline\cr}}~{\\\\[-6.75pt] Contextual
types}}~{&T\hfil~{}&\;\mathrel{::=}~{}&\Psi\vdash A\,\mid\,\Psi\vdash_{v}A\\\
Contextual objects}}~{&C\hfil~{}&\;\mathrel{::=}~{}&\widehat{\Psi}\vdash
M\\\\[2.25pt] \hline\cr}}~{\\\\[-6.75pt] Domain of
discourse}}~{&\breve{\tau}\hfil~{}&\;\mathrel{::=}~{}&\tau\,\mid\,\texttt{ctx}\\\
Types and Terms}}~{&\tau,{\mathcal{I}}\hfil~{}&\;\mathrel{::=}~{}&\lceil
T\rceil\,\mid\,(y:\breve{\tau}_{1})\Rightarrow\tau_{2}\\\
}}~{&t,s\hfil~{}&\;\mathrel{::=}~{}&y\,\mid\,\lceil
C\rceil\,\mid\,\mathsf{rec}^{{\mathcal{I}}}~{}{\vec{\mathcal{B}}}~{}\Psi~{}t\,\mid\,\mathsf{fn}\;y\Rightarrow
t\,\mid\,t_{1}~{}t_{2}\par\\\
Branches}}~{&{\mathcal{B}}\hfil~{}&\;\mathrel{::=}~{}&\Gamma\mapsto t\\\
Contexts}}~{&\Gamma\hfil~{}&\;\mathrel{::=}~{}&\cdot\,\mid\,\Gamma,y:\breve{\tau}\end{array}$
Figure 1. Syntax of Cocon with a fixed simply-typed domain tm

We first define our simply-typed domain-level with the type tm and the term
constants $\mathsf{lam}$ and $\mathsf{app}$ (see Fig. 1). Following Cocon, we
allow computations to be embedded into domain-level terms via unboxing. The
intuition is that if a program $t$ promises to compute a value of type $\lceil
x{:}\texttt{tm},y{:}\texttt{tm}\vdash\texttt{tm}\rceil$, then we can embed $t$
directly into a domain-level object writing $\mathtt{lam}~{}\lambda
x.\mathtt{lam}~{}\lambda y.\mathtt{app}~{}\lfloor t\rfloor~{}x$, unboxing $t$.
Domain-level objects (resp. types) can be packaged together with their domain-
level context to form a contextual object (resp. type). Domain-level contexts
are formed as usual, but may contain context variables to describe a yet
unknown prefix. Last, we include domain-level substitutions that allow us to
move between domain-level contexts. The compound substitution $\sigma,M$
extends the substitution $\sigma$ with domain $\widehat{\Psi}$ to a
substitution with domain $\widehat{\Psi},x$, where $M$ replaces $x$. Following
Nanevski et al. (2008); Pientka et al. (2019), we do not store the domain
(like $\widehat{\Psi}$) in the substitution, it can always be recovered before
applying the substitution. We also include _weakening substitution_ , written
as $\mathsf{wk}_{\widehat{\Psi}}$, to describe the weakening of the domain
$\Psi$ to $\Psi,\overrightarrow{x{:}A}$. Weakening substitutions are
necessary, as they allow us to express the weakening of a context variable
$\psi$. Identity is a special form of the $\mathsf{wk}_{\widehat{\Psi}}$
substitution, which follows immediately from the typing rule of
$\mathsf{wk}_{\widehat{\Psi}}$. Composition is admissible.

We summarise the typing rules for domain-level terms and types in Fig. 2. We
also include typing rules for domain-level contexts. Note that since we
restrict ourselves to a simply-typed domain-level, we simply check that $A$ is
a well-formed type. We remark that equality for domain-level terms and
substitution is modulo $\beta\eta$. In particular,
$\lfloor\lceil\widehat{\Phi}\vdash N\rceil\rfloor_{\sigma}$ reduces to
$[\sigma]N$.

$\begin{array}[]{c}\lx@intercol\vtop{\hbox to341.43306pt{
\framebox{$\Gamma;\Psi\vdash M:A$}~{}~{}Term $M$ has type $A$ in domain-level
context $\Psi$ and context $\Gamma$\newline }}\lx@intercol\\\
\Gamma;\Psi\vdash
x:A\lx@proof@logical@and\Gamma\vdash\Psi:\texttt{ctx}x{:}A\in\Psi\qquad\Gamma;\Psi\vdash\mathsf{lam}:(\texttt{tm}\to\texttt{tm})\to\texttt{tm}\Gamma\vdash\Psi:\texttt{ctx}\qquad\Gamma;\Psi\vdash\mathsf{app}:\texttt{tm}\to\texttt{tm}\to\texttt{tm}\Gamma\vdash\Psi:\texttt{ctx}\\\\[4.5pt]
\Gamma;\Psi\vdash M~{}N:B\lx@proof@logical@and\Gamma;\Psi\vdash M:A\to
B\Gamma;\Psi\vdash N:A\qquad\Gamma;\Psi\vdash\lambda x.M:A\to
B\Gamma;\Psi,x{:}A\vdash M:B\qquad\Gamma;\Psi\vdash\lfloor
t\rfloor_{\sigma}:A\lx@proof@logical@and\Gamma\vdash t:\lceil\Phi\vdash
A\rceil\text{ or }\Gamma\vdash
t:\lceil\Phi\vdash_{v}A\rceil\Gamma;\Psi\vdash\sigma:\Phi\\\\[9.00002pt]
\lx@intercol\vtop{\hbox to341.43306pt{
\framebox{$\Gamma;\Phi\vdash\sigma:\Psi$}~{}~{}Substitution $\sigma$ provides
a mapping from the (domain) context $\Psi$ to $\Phi$\newline
<EMAIL_ADDRESS>\Gamma;\Psi,\overrightarrow{x{:}A}\vdash\mathsf{wk}_{\widehat{\Psi}}:\Psi\Gamma\vdash\Psi,\overrightarrow{x{:}A}:\texttt{ctx}\quad\Gamma;\Phi\vdash\cdot:\cdot\Gamma\vdash\Phi:\texttt{ctx}\quad\Gamma;\Phi\vdash\sigma,M:\Psi,x{:}A\lx@proof@logical@and\Gamma;\Phi\vdash\sigma:\Psi\Gamma;\Phi\vdash
M:A\\\\[9.00002pt]
\lx@intercol\framebox{$\Gamma\vdash\Psi:\texttt{ctx}$}~{}~{}\mbox{Domain-level
context $\Psi$ is<EMAIL_ADDRESS>\Gamma\vdash\cdot:\texttt{ctx}\quad\Gamma\vdash
y:\texttt{ctx}\Gamma(y)=\mathsf{ctx}\quad\Gamma\vdash\Psi,x{:}A:\texttt{ctx}\Gamma\vdash\Psi:\texttt{ctx}\end{array}$
Figure 2. Typing Rules for Domain-level Terms, Substitutions, Contexts

In our grammar, we distinguish between the contextual type $\Psi\vdash A$ and
the more restricted contextual type $\Phi\vdash_{v}A$ which characterises only
variables of type $A$ from the domain-level context $\Phi$. We give here two
sample typing rules for $\Phi\vdash_{v}A$ which are the ones used most in
practice to illustrate the main idea. We embed contextual objects into
computations via the modality. Computation-level types include boxed
contextual types, $\lceil\Phi\vdash A\rceil$, and function types, written as
$(y:\breve{\tau}_{1})\Rightarrow\tau_{2}$. We overload the function space and
allow as domain of discourse both computation-level types and the schema
$\mathsf{ctx}$ of domain-level contexts, although only in the latter case $y$
can occur in $\tau_{2}$. We use $\mathsf{fn}\;y\Rightarrow t$ to introduce
functions of both kinds. We also overload function application $t\;s$ to
eliminate function types $(y:\tau_{1})\Rightarrow\tau_{2}$ and
$(y:\mathsf{ctx})\Rightarrow\tau_{2}$, although in the latter case $s$ stands
for a domain-level context. We separate domain-level contexts from contextual
objects, as we do not allow functions that return a domain-level context.

The recursor is written as
$\mathsf{rec}^{{\mathcal{I}}}~{}{\vec{\mathcal{B}}}~{}\Psi~{}t$. Here, $t$
describes a term of type $\lceil\Psi\vdash\texttt{tm}\rceil$ that we recurse
over and $\vec{\mathcal{B}}$ describes the different branches that we can take
depending on the value computed by $t$. As is common when we have
dependencies, we annotate the recursor with the typing invariant
${\mathcal{I}}$. Here, we consider only the recursor over domain-level terms
of type tm. Hence, we annotate it with
${\mathcal{I}}=(\psi:\mathsf{ctx})\Rightarrow(y:\lceil\psi\vdash\texttt{tm}\rceil)\Rightarrow\tau$.
To check that the recursor
$\mathsf{rec}^{{\mathcal{I}}}~{}{\mathcal{B}}~{}\Psi~{}t$ has type
$[\Psi/\psi]\tau$, we check that each of the three branches has the specified
type ${\mathcal{I}}$. In the base case, we may assume in addition to
$\psi:{\mathsf{ctx}}$ that we have a variable
$p:\lceil\psi\vdash_{v}\texttt{tm}\rceil$ and check that the body has the
appropriate type. If we encounter a contextual object built with the domain-
level constant $\mathsf{app}$, then we choose the branch $b_{\mathsf{app}}$.
We assume $\psi{:}\,\mathsf{ctx}$, $m{:}\,\lceil\psi\vdash\texttt{tm}\rceil$,
$n{:}\,\lceil\psi\vdash\texttt{tm}\rceil$, as well as $f_{n}$ and $f_{m}$
which stand for the recursive calls on $m$ and $n$ respectively. We then check
that the body $t_{\mathsf{app}}$ is well-typed. If we encounter a domain
object built with the domain-level constant $\mathsf{lam}$, then we choose the
branch $b_{\mathsf{lam}}$. We assume $\psi{:}\,\mathsf{ctx}$ and
$m{:}\,\lceil\psi,x{:}\texttt{tm}\vdash\texttt{tm}\rceil$ together with the
recursive call $f_{m}$ on $m$ in the extended LF context
$\psi,x{:}\texttt{tm}$. We then check that the body $t_{\mathsf{lam}}$ is
well-typed. The typing rules for computations are given in Fig. 3. We omit the
reduction rules here for brevity.

$\begin{array}[]{c}\lx@intercol\vtop{\hbox to341.43306pt{
\framebox{$\Gamma\vdash C:T$}~{}~{} Contextual object $C$ has contextual type
$T$\newline }}\lx@intercol\\\ \Gamma\vdash(\widehat{\Psi}\vdash M):(\Psi\vdash
A)\Gamma;\Psi\vdash M:A\qquad\Gamma\vdash(\widehat{\Psi}\vdash
x):(\Psi\vdash_{v}A)\lx@proof@logical@and\Gamma\vdash\Psi:\texttt{ctx}x{:}A\in\Psi\qquad\Gamma\vdash(\widehat{\Psi}\vdash\lfloor
x\rfloor_{\mathsf{wk}_{\widehat{\Psi}}}):(\Psi\vdash_{v}A)\lx@proof@logical@and
x{:}\lceil\Phi\vdash_{v}A\rceil\in\Gamma\Gamma;\Psi\vdash\mathsf{wk}_{\widehat{\Psi}}:\Phi\end{array}$

$\begin{array}[]{c}\lx@intercol\vtop{\hbox to341.43306pt{
\framebox{$\Gamma\vdash t:\tau$}~{}~{} Term~{}$t$ has computation
<EMAIL_ADDRESS>\Gamma\vdash
y:\breve{\tau}y:\breve{\tau}\in\Gamma\qquad\Gamma\vdash\lceil C\rceil:\lceil
T\rceil\Gamma\vdash C:T\qquad\Gamma\vdash
t~{}s:[s/y]\tau_{2}\lx@proof@logical@and\Gamma\vdash
t:(y:\breve{\tau}_{1})\Rightarrow\tau_{2}\Gamma\vdash
s:\breve{\tau}_{1}\qquad\Gamma\vdash\mathsf{fn}\;y\Rightarrow
t:(y:\breve{\tau}_{1})\Rightarrow\tau_{2}\lx@proof@logical@and\Gamma,y:\breve{\tau}_{1}\vdash
t:\tau_{2}\Gamma\vdash(y:\breve{\tau}_{1})\Rightarrow\tau_{2}:\
\text{type}\\\\[6.75pt] \lx@intercol\mbox{Recursor over domain-level
<EMAIL_ADDRESS>\Gamma\vdash\mathsf{rec}^{{\mathcal{I}}}(b_{v}\mid b_{\mathsf{app}}\mid
b_{\mathsf{lam}})~{}~{}\Psi~{}t:[{\Psi}/\psi]\tau\lx@proof@logical@and\Gamma\vdash
t:\lceil\Psi\vdash\texttt{tm}\rceil\Gamma\vdash{\mathcal{I}}:\
\text{type}\Gamma\vdash b_{v}:{\mathcal{I}}\Gamma\vdash
b_{\mathsf{app}}:{\mathcal{I}}\Gamma\vdash
b_{\mathsf{lam}}:{\mathcal{I}}\\\\[9.00002pt]
\raisebox{7.74997pt}{\mbox{Branch for Variable
($b_{v}$)}}\qquad\inferrule*{\Gamma,\psi:\mathsf{ctx},p:\lceil\psi\vdash_{v}\texttt{tm}\rceil\vdash
t_{v}:\tau}{\Gamma\vdash({\psi,p\mapsto
t_{v}}):{\mathcal{I}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}}\\\\[4.5pt]
\raisebox{7.74997pt}{\mbox{Branch for Application $\mathsf{app}$
($b_{\mathsf{app}}$)}}\qquad\Gamma\vdash(\psi,m,n,f_{n},f_{m}\mapsto
t_{\mathsf{app}}):{\mathcal{I}}\Gamma,\psi:\mathsf{ctx},m{:}\lceil\psi\vdash\texttt{tm}\rceil,n{:}\lceil\psi\vdash\texttt{tm}\rceil,f_{m}{:}\tau,f_{n}{:}\tau\vdash
t_{\mathsf{app}}:\tau\\\\[4.5pt] \raisebox{7.74997pt}{\mbox{Branch for
Function $\mathsf{lam}$
($b_{\mathsf{lam}}$)}}\qquad\Gamma\vdash\psi,m,f_{m}\mapsto
t_{\mathsf{lam}}:{\mathcal{I}}\Gamma,\phi:\mathsf{ctx},m{:}\lceil\phi,x{:}\texttt{tm}\vdash\texttt{tm}\rceil,f_{m}{:}[(\phi,x{:}\texttt{tm})/\psi]\tau\vdash
t_{\mathsf{lam}}:[\phi/\psi]\tau\end{array}$

Figure 3. Typing Rules for Contextual Objects and Computations

We now give an interpretation of simply-typed Cocon in a presheaf model with a
cartesian closed universe of representables. Let us first extend the internal
dependent type theory with the constant tm for modelling the domain-level type
constant tm and with the constants
$\texttt{app}\colon\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm}$
and
$\texttt{lam}\colon(\texttt{El}\,\texttt{tm}\to\texttt{El}\,\texttt{tm})\to\texttt{El}\,\texttt{tm}$
to model the corresponding domain-level constants $\mathsf{app}$ and
$\mathsf{lam}$.

Interpretation of domain-level types
$\displaystyle\llbracket\texttt{tm}\rrbracket$ $\displaystyle=$ tm
$\displaystyle\llbracket A\to B\rrbracket$ $\displaystyle=$
$\displaystyle\texttt{arrow}\ \llbracket A\rrbracket\ \llbracket B\rrbracket$
Interpretation of domain-level contexts
$\displaystyle\llbracket\Gamma\vdash\psi:\texttt{ctx}\rrbracket$
$\displaystyle=$ $\displaystyle\psi$
$\displaystyle\llbracket\Gamma\vdash\cdot:\texttt{ctx}\rrbracket$
$\displaystyle=$ unit where
$\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket=e$
$\displaystyle\llbracket\Gamma\vdash(\Psi,x{:}A):\texttt{ctx}\rrbracket$
$\displaystyle=$ $\displaystyle\texttt{times}\ e\ \llbracket A\rrbracket$
$\displaystyle\mbox{Interpretation of domain-level terms, where
}\llbracket\Gamma\vdash\Psi\texttt{ ctx}\rrbracket=e$ where
$\Psi=\Psi_{0},x{:}A,y_{k}{:}A_{k},\ldots,y_{1}{:}A_{1}$
$\displaystyle\llbracket\Gamma;\Psi\vdash x\colon A\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{snd}~{}(\texttt{fst}^{k}~{}u)$ where
$\llbracket\Gamma;\Psi,x{:}A\vdash M:B\rrbracket=e^{\prime}$
$\displaystyle\llbracket\Gamma;\Psi\vdash\lambda x.\,M:A\to B\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{arrow-i}\ (\leftthreetimes
x{:}\texttt{El}\,\llbracket A\rrbracket.e^{\prime}~{}(\texttt{pair}~{}u~{}x))$
where $\llbracket\Gamma;\Psi\vdash M:A\to B\rrbracket=e_{1}$
$\displaystyle\llbracket\Gamma;\Psi\vdash M\ N:B\rrbracket$ $\displaystyle=$
$\displaystyle\leftthreetimes u:\texttt{El}\,e.\texttt{arrow-e}\ (e_{1}~{}u)\
(e_{2}~{}u)$ where $\llbracket\Gamma\vdash t:\lceil\Phi\vdash
A\rceil\rrbracket=e_{1}$ $\displaystyle\llbracket\Gamma;\Psi\vdash\lfloor
t\rfloor_{\sigma}:A\rrbracket$ $\displaystyle=$
$\displaystyle\texttt{let}~{}\texttt{box}~{}x=e_{1}\ \texttt{in}\
\leftthreetimes u:\texttt{El}\,e.x(e_{2}\;u)$
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathsf{app}:\texttt{tm}\to\texttt{tm}\to\texttt{tm}\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{arrow-i}(\leftthreetimes
x{:}\texttt{El}\,\texttt{tm}.\,\texttt{arrow-i}\ (\leftthreetimes
y{:}\texttt{El}\,\texttt{tm}.\,\texttt{app}\ x\ y))$
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathsf{lam}:(\texttt{tm}\to\texttt{tm})\to\texttt{tm}\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{arrow-i}(\leftthreetimes
f{:}\texttt{El}\,(\texttt{arrow}~{}\texttt{tm}~{}\texttt{tm}).\,\texttt{lam}\
(\leftthreetimes x{:}\texttt{El}\,\texttt{tm}.\,\texttt{arrow-e}\ f\ x))$
$\displaystyle\mbox{Interpretation of domain-level substitutions, where
}\llbracket\Gamma\vdash\Psi\texttt{ ctx}\rrbracket=e$
$\displaystyle\llbracket\Gamma;\Psi\vdash\cdot:\cdot\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{terminal}$ where
$\llbracket\Gamma;\Psi\vdash\sigma:\Phi\rrbracket=e_{1}$ and
$\llbracket\Gamma;\Psi\vdash M:A\rrbracket=e_{2}$
$\displaystyle\llbracket\Gamma;\Psi\vdash(\sigma,M):\Phi,x{:}A\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes u:\texttt{El}\,e.\texttt{pair}\
(e_{1}u)\ (e_{2}u)$ where $n=|\overrightarrow{x{:}A}|$
$\displaystyle\llbracket\Gamma;\Psi,\overrightarrow{x{:}A}\vdash\mathsf{wk}_{\widehat{\Psi}}:\Psi\rrbracket$
$\displaystyle=$ $\displaystyle\leftthreetimes
u:\texttt{El}\,e.\texttt{fst}^{n}~{}u$ Figure 4. Interpretation of Domain-
level Types and Terms

We can now translate domain-level and computation-level types of Cocon into
the internal dependent type theory for $\widehat{\mathbb{D}}$. We do so by
interpreting the domain-level terms, types, substitutions, and contexts (see
Fig. 4). All translations are on well-typed terms and types. Domain-level
types are interpreted as the terms of type Obj in the internal dependent type
theory that represent them. Domain-level contexts are also interpreted as
terms of type Obj by $\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket$. For
example, a domain-level context $x{:}\texttt{tm},y{:}\texttt{tm}$ is
interpreted as
$\texttt{times}~{}(\texttt{times}~{}\texttt{unit}~{}\texttt{tm})~{}\texttt{tm}:\texttt{Obj}$.
A domain-level substitution with domain $\Psi$ and codomain $\Phi$ becomes a
function from $\texttt{El}\,e^{\prime}$ to $\texttt{El}\,e$, where
$e^{\prime}=\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket$ and
$e=\llbracket\Gamma\vdash\Phi:\texttt{ctx}\rrbracket$. Thus we use a semantic
function to interpret a simultaneous substitution as usual. As $e$ is some
product, for example
$\texttt{times}~{}(\texttt{times}~{}\texttt{unit}~{}\texttt{tm})~{}\texttt{tm}$,
the domain-level substitution is translated into a function returning an n-ary
tuple. A weakening substitution
$\Gamma;\Psi,x{:}\texttt{tm}\vdash\mathsf{wk}_{\Psi}:\Psi$ is interpreted as
$\texttt{fst}~{}u$ where
$u{:}\,\texttt{El}\,(\texttt{times}~{}e~{}\texttt{tm})$ and
$e=\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket$. More generally, when we
weaken a context $\Psi$ by $n$ declarations, i.e. $\overrightarrow{x{:}A}$, we
interpret $\mathsf{wk}_{\Psi}$ as $\texttt{fst}^{n}~{}u$. A well-typed domain-
level term, $\Gamma;\Psi\vdash M:A$, is mapped to a function from
$u{:}\texttt{El}\,\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket$ to
$\texttt{El}\,\llbracket A\rrbracket$.

Hence the translation of a well-typed domain-level term eventually introduces
via a $\leftthreetimes\ u$ that stands for the term-level interpretation of a
domain-level context $\Phi$. Most cases in the interpretation just pass $u$
along. The exceptional case is $\Gamma;\Phi\vdash\lambda x.M:A\to B$, because
the body $M$ is translated into a function from an extended domain-level
context $\Psi,x{:}A$. In this case, we need to pair $u$ with the variable $x$
obtained from the constructor of the domain-level function. When we translate
a variable $x$ where $\Phi=\Phi_{0},x{:}A,y_{k}{:}A_{k},\ldots,y_{1}{:}A_{1}$,
we return $\texttt{snd}~{}(\texttt{fst}^{k}~{}u)$. We translate
$\Gamma;\Phi\vdash\lfloor t\rfloor_{\sigma}:A$ directly using let box-
construct. Intuitively, a substitution of terms is morphism composition. The
interpretation of the domain-level substitution $\sigma$ has given one
morphism. The computation term $t$ should give the other morphism. Since it
has the contextual type $\lceil\Phi\vdash\texttt{tm}\rceil$ its translation
will be of type $\flat(\texttt{El}\,e\to\texttt{El}\,\texttt{tm})$ where
$e^{\prime}=\llbracket\Gamma\vdash\Phi:\texttt{ctx}\rrbracket$. We thus can
obtain a $\texttt{El}\,e\to\texttt{El}\,\texttt{tm}$ from let box, in which we
can compose $e_{2}$ to obtain the final morphism. The translation of domain-
level applications and domain-level constants $\mathsf{app}$ and
$\mathsf{lam}$ is straightforward.

The interpretation of a contextual type ${(\Phi\vdash A)}$ makes explicit the
fact that they correspond to functions
$\texttt{El}\,e\to\texttt{El}\,\llbracket A\rrbracket$ where
$e=\llbracket\Gamma\vdash\Phi:\texttt{ctx}\rrbracket$ (see Fig. 5).
Consequently, the corresponding contextual object $(\widehat{\Phi}\vdash M)$
is interpreted as a function which is already the case by just taking the
interpretation of domain-level terms. The case of ${(\Psi\vdash_{v}A)}$
requires the contextual object to be interpreted to the restricted function
space denoted by $\to_{v}$, which is the case by looking at the variable case
of the domain-level interpretation.

$\begin{array}[]{l@{~}c@{~}ll}\lx@intercol\mbox{Interpretation of contextual
objects<EMAIL_ADDRESS>\llbracket\Gamma\vdash(\widehat{\Phi}\vdash M):(\Phi\vdash
A)\rrbracket\hfil~{}&=\hfil~{}&\llbracket\Gamma;\Phi\vdash
M:A\rrbracket\\\\[2.25pt] \llbracket\Gamma\vdash(\widehat{\Phi}\vdash
M):(\Phi\vdash_{v}A)\rrbracket\hfil~{}&=\hfil~{}&\llbracket\Gamma;\Phi\vdash
M:A\rrbracket\\\\[4.5pt] \lx@intercol\mbox{Interpretation of contextual types
<EMAIL_ADDRESS>\llbracket\Gamma\vdash(\Phi\vdash
A)\rrbracket\hfil~{}&=\hfil~{}&(u{:}\texttt{El}\,e)\to\texttt{El}\,\llbracket
A\rrbracket&\mbox{where}~{}\llbracket\Gamma\vdash\Phi:\texttt{ctx}\rrbracket=e\\\\[2.25pt]
\llbracket\Gamma\vdash(\Phi\vdash_{v}A)\rrbracket\hfil~{}&=\hfil~{}&(u{:}\texttt{El}\,e)\to_{v}\texttt{El}\,\llbracket
A\rrbracket&\mbox{where}~{}\llbracket\Gamma\vdash\Phi:\texttt{ctx}\rrbracket=e\end{array}$
Figure 5. Interpretation of Contextual Objects and Types

Last, we give the interpretation of computation-level types, contexts and
terms (see Fig. 6). It is mostly straightforward. We simply map $\lceil
T\rceil$ in context $\Gamma$ to $\flat\llbracket\Gamma\vdash T\rrbracket$ and
$\lceil C\rceil$ is simply interpreted as a boxed term. Since we intend to
keep all variables on the computation level crisp, we interpret function types
to the crisp function space. As a consequence, the argument in a function
application must be closed. This is true because all computation-level terms
should only use crisp variables, and it is justified by the soundness theorem.
When translating a computation-level function, we use
$\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}$ for abstraction, so that we
create a crisp function. We then recursively interpret the function body.

$\begin{array}[]{l@{~}c@{~}ll}\lx@intercol\mbox{Interpretation of computation-
level types<EMAIL_ADDRESS>\llbracket\Gamma\vdash\lceil
T\rceil\rrbracket\hfil~{}&=\hfil~{}&\flat\llbracket\Gamma\vdash
T\rrbracket\\\\[2.25pt]
\llbracket\Gamma\vdash(x{:}\breve{\tau}_{1})\Rightarrow\tau_{2}\rrbracket\hfil~{}&=\hfil~{}&(x{::}\llbracket\Gamma\vdash\breve{\tau}_{1}\rrbracket)\to^{\flat}\llbracket\Gamma,x:\breve{\tau}_{1}\vdash\tau_{2}\rrbracket\\\\[2.25pt]
\llbracket\Gamma\vdash\texttt{ctx}\rrbracket\hfil~{}&=\hfil~{}&\texttt{Obj}\\\\[4.5pt]
\lx@intercol\mbox{Computation-level typing contexts
<EMAIL_ADDRESS>\llbracket\cdot\rrbracket\hfil~{}&=\hfil~{}&\cdot&\\\\[2.25pt]
\llbracket\Gamma,\,x{:}\,\breve{\tau}\rrbracket\hfil~{}&=\hfil~{}&\llbracket\Gamma\rrbracket,\,x::\llbracket\Gamma\vdash\breve{\tau}\rrbracket&\\\\[4.5pt]
\lx@intercol\mbox{Interpretation of computations ($\Gamma\vdash t:\tau$;
without<EMAIL_ADDRESS>\llbracket\Gamma\vdash\lceil
C\rceil:\lceil
T\rceil\rrbracket\hfil~{}&=\hfil~{}&\texttt{box}~{}e&\mbox{where}~{}\llbracket\Gamma\vdash
C:T\rrbracket=e\\\\[2.25pt] \llbracket\Gamma\vdash t_{1}\
t_{2}:\tau\rrbracket\hfil~{}&=\hfil~{}&e_{1}\
e_{2}&\mbox{where}~{}\llbracket\Gamma\vdash
t_{1}:(x{:}\breve{\tau}_{2})\Rightarrow\tau\rrbracket=e_{1}{}\\\
\hfil~{}&\hfil~{}&&\mbox{and}~{}\llbracket\Gamma\vdash
t_{2}:\breve{\tau_{2}}\rrbracket=e_{2}\\\\[2.25pt]
\llbracket\Gamma\vdash\mathsf{fn}\;x\Rightarrow
t:(x{:}\breve{\tau}_{1})\Rightarrow\tau_{2}\rrbracket\hfil~{}&=\hfil~{}&\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}x{::}\llbracket\Gamma\vdash\breve{\tau}_{1}\rrbracket.\,e&\mbox{where}~{}\llbracket\Gamma,x{:}\breve{\tau}_{1}\vdash
t:\tau_{2}\rrbracket=e\\\\[2.25pt] \llbracket\Gamma\vdash
x:\tau\rrbracket\hfil~{}&=\hfil~{}&x&\end{array}$ Figure 6. Interpretation of
Computation-level Types and Terms – without recursor

The interpretation of the recursor is straightforward now (see Fig. 7). In
Lemma 4.5, we expressed a primitive recursion scheme in our internal type
theory and defined a term rec together with its type. We now interpret every
branch of our recursor in the computation-level as a function of the required
type in our internal type theory. While this is somewhat tedious, it is
straightforward. When interpreting the branches, we again use the crisp
function space, which allows us to push the parameters to the crisp context
and simulate the behavior of Cocon. The branch body is then interpreted
recursively.

$\begin{array}[]{l@{~}c@{~}ll}\lx@intercol\mbox{Interpretation of recursor for
<EMAIL_ADDRESS>\lx@intercol\llbracket\Gamma\vdash\mathsf{rec}^{{\mathcal{I}}}(b_{v}\mid
b_{\mathsf{app}}\mid
b_{\mathsf{lam}})~{}~{}\Psi~{}t:[{\Psi}/\psi,~{}t/y]\tau\rrbracket=\texttt{rec}~{}e_{v}~{}e_{\texttt{app}}~{}e_{\texttt{lam}}~{}e_{c}~{}e\hfil\lx@intercol\\\
\lx@intercol\quad\mbox{where}~{}\llbracket\Gamma\vdash
b_{v}:{\mathcal{I}}\rrbracket=e_{v},\llbracket\Gamma\vdash
b_{\mathsf{app}}:{\mathcal{I}}\rrbracket=e_{\texttt{app}},\llbracket\Gamma\vdash
b_{\mathsf{lam}}:{\mathcal{I}}\rrbracket=e_{\texttt{lam}},\hfil\lx@intercol\\\
\lx@intercol\phantom{\quad\mbox{where}}~{}\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket=e_{c}~{}\mbox{and}~{}\llbracket\Gamma\vdash
<EMAIL_ADDRESS>\lx@intercol\mbox{Interpretation of Variable
<EMAIL_ADDRESS>\llbracket\Gamma\vdash({\psi,p\mapsto
t_{v}}):{\mathcal{I}}\rrbracket\hfil~{}&=\hfil~{}&\lx@intercol\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}\psi{::}\texttt{Obj}.\,\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}p{::}\flat(\texttt{El}\,\psi\to_{v}\texttt{El}\,\texttt{tm}).e\hfil\lx@intercol\\\
\lx@intercol\quad\mbox{where}~{}\llbracket\Gamma,\psi:\mathsf{ctx},p:\lceil\psi\vdash_{v}\texttt{tm}\rceil\vdash
<EMAIL_ADDRESS>\lx@intercol\mbox{Interpretation of Application
<EMAIL_ADDRESS>\llbracket\Gamma\vdash(\psi,m,n,f_{n},f_{m}\mapsto
t_{\mathsf{app}}):{\mathcal{I}}\rrbracket\hfil~{}&=\hfil~{}&\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}\psi{::}\texttt{Obj}.\,\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}m,n{::}\flat(\texttt{El}\,\psi\to\texttt{El}\,\texttt{tm}).\\\
\hfil~{}&\hfil~{}&\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}f_{m}{::}\llbracket\Gamma\vdash[\psi,m/\psi,y]\tau\rrbracket.\,\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}f_{n}{::}\llbracket\Gamma\vdash[\psi,n/\psi,y]\tau\rrbracket.e\\\
\lx@intercol\quad\mbox{where}~{}\llbracket\Gamma,\psi{:}\texttt{ctx},m{:}\lceil\psi\vdash\texttt{tm}\rceil,n{:}\lceil\psi\vdash\texttt{tm}\rceil,f_{m}:[m/y]\tau,f_{n}:[n/y]\tau\vdash
t_{\mathsf{app}}:[\lceil\psi\vdash\mathsf{app}~{}\lfloor m\rfloor~{}\lfloor
<EMAIL_ADDRESS>\lx@intercol\mbox{Interpretation of Lambda-Abstraction
<EMAIL_ADDRESS>\llbracket\Gamma\vdash(\psi,m,f_{m}\mapsto
t_{\mathsf{lam}}):{\mathcal{I}}\rrbracket\hfil~{}&=\hfil~{}&\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}\psi::\texttt{Obj}.\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}m::\flat(\texttt{El}\,(\texttt{times}~{}\psi~{}\texttt{tm})\to\texttt{El}\,\texttt{tm}).\leftthreetimes^{\\!\\!\scriptscriptstyle\flat}f_{m}{::}\tau_{m}.e\\\
\lx@intercol\quad\mbox{where}~{}\llbracket\Gamma\vdash[(\psi,x{:}\texttt{tm}),~{}m/\psi,y]\tau\rrbracket=\tau_{m},\hfil\lx@intercol\\\
\lx@intercol\phantom{\quad\mbox{where}}~{}\llbracket\Gamma,\psi{:}\texttt{ctx},m{:}\lceil\psi,x{:}\texttt{tm}\vdash\texttt{tm}\rceil,f_{m}:[(\psi,x:tm),m/\psi,y]\tau\vdash
t_{\mathsf{app}}:[\lceil\psi\vdash\mathsf{lam}~{}\lambda x.\lfloor
m\rfloor\rceil/y]\tau\rrbracket=e\hfil\lx@intercol\\\ \end{array}$ Figure 7.
Interpretation of Recursor

We can now show that all well-typed domain-level and computation-level objects
are translated into well-typed constructions in our internal type theory. As a
consequence, we can show that equality in Cocon implies the corresponding
equivalence in our internal type theoretic interpretation.

###### Lemma 5.1.

The interpretation maintains the following typing invariants:

  * •

If $\Gamma\vdash\Psi\colon\texttt{ctx}$ then
$\llbracket\Gamma\vdash\Psi\colon\texttt{ctx}\rrbracket\colon\texttt{Obj}$.

  * •

If $\Gamma;\,\Psi\vdash M\colon A$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma;\Psi\vdash
M\colon
A\rrbracket\colon(u:\texttt{El}\,\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket)\to\texttt{El}\,\llbracket
A\rrbracket$.

  * •

If $\Gamma;\,\Psi\vdash\sigma\colon\Psi$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma;\Psi\vdash\sigma\colon\Psi\rrbracket\colon(u{:}\,\texttt{El}\,\llbracket\Gamma\vdash\Psi:\texttt{ctx}\rrbracket)\to\texttt{El}\,\llbracket\Psi\rrbracket$.

  * •

If $\Gamma\vdash C\colon T$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma\vdash
C:T\rrbracket\colon\llbracket\Gamma\vdash T\rrbracket$.

  * •

If $\Gamma\vdash t\colon\tau$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma\vdash
t\colon\tau\rrbracket\colon\llbracket\Gamma\vdash\tau\rrbracket$.

The proof goes by induction on derivations. Next we show that equivalence in
Cocon is preserved by the interpretation.

###### Proposition 5.2 (Soundness).

The following are true.

  * •

If $\Gamma;\,\Psi\vdash M\equiv N\colon A$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma;\,\Psi\vdash
M:A\rrbracket=\llbracket\Gamma;\,\Psi\vdash
N:A\rrbracket\colon(u{:}\,\texttt{El}\,\llbracket\Psi\rrbracket)\to\texttt{El}\,\llbracket
A\rrbracket$.

  * •

If $\Gamma;\Psi\vdash\sigma\equiv\sigma^{\prime}\colon\Phi$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma;\Psi\vdash\sigma:\Phi\rrbracket=\llbracket\Gamma;\Psi\vdash\sigma^{\prime}:\Phi\rrbracket\colon(u{:}\,\texttt{El}\,\llbracket\Psi\rrbracket)\to\texttt{El}\,\llbracket\Phi\rrbracket$.

  * •

If $\Gamma\vdash t_{1}\equiv t_{2}\colon\breve{\tau}$ then
$\llbracket\Gamma\rrbracket\,\mid\,\cdot\vdash\llbracket\Gamma\vdash
t_{1}:\breve{\tau}\rrbracket=\llbracket\Gamma\vdash
t_{2}:\breve{\tau}\rrbracket\colon\llbracket\Gamma\vdash\breve{\tau}\rrbracket$.

The proof in the $\beta$ and $\eta$ equivalence cases of contextual types is
interesting. In the case of $\beta$ equivalence, we have * Γ ; Φ ⊢M : A
Γ; Ψ ⊢σ : Φ Γ; Ψ ⊢⌊⌈M⌉⌋_σ≡[σ]M : A The right hand side is easy; substitution
in terms is just composition of morphisms:

where $\llbracket\Gamma;\Phi\vdash M:A\rrbracket=e_{1}$ and
$\llbracket\Gamma;\Psi\vdash\sigma:\Phi\rrbracket=e_{2}$
$\displaystyle\llbracket\Gamma;\Psi\vdash[\sigma]M:A\rrbracket$
$\displaystyle=e_{1}\circ e_{2}$

On the left hand side, we have

where $\llbracket\Gamma\vdash\Psi\texttt{ ctx}\rrbracket=e$,
$\displaystyle\llbracket\Gamma;\Psi\vdash\lfloor\lceil
M\rceil\rfloor_{\sigma}:A\rrbracket$
$\displaystyle=\texttt{let}~{}\texttt{box}~{}x=\texttt{box}~{}e_{1}\
\texttt{in}\ \leftthreetimes u:\texttt{El}\,e.x(e_{2}\;u)$ due to the $\beta$
rule of $\flat$ $\displaystyle=\leftthreetimes u:\texttt{El}\,e.e_{1}(e_{2}\
u)$

Thus the $\beta$ equivalence of contextual types is sound semantically.

The following rule expresses the $\eta$ equivalence of contextual types: * Γ⊢t
: ⌈ Ψ ⊢A ⌉ Γ⊢t ≡⌈⌊t⌋_$\mathsf{wk}_{\widehat{\Psi}}$⌉ : ⌈ Ψ ⊢A ⌉

We reason as follows:

where $\llbracket\Gamma\vdash\Psi\texttt{ ctx}\rrbracket=e$ and
$\llbracket\Gamma\vdash t:\lceil\Psi\vdash A\rceil\rrbracket=e^{\prime}$
$\displaystyle\llbracket\Gamma\vdash\lceil\lfloor
t\rfloor_{\mathsf{wk}_{\widehat{\Psi}}}\rceil:\lceil\Psi\vdash
A\rceil\rrbracket$
$\displaystyle=\texttt{box}~{}\texttt{let}~{}\texttt{box}~{}x=e^{\prime}\
\texttt{in}\ \leftthreetimes u:\texttt{El}\,e.x\ u$ $\eta$ equivalence of
$\leftthreetimes$
$\displaystyle=\texttt{box}~{}\texttt{let}~{}\texttt{box}~{}x=\llbracket\Gamma\vdash
t:\lceil\Psi\vdash A\rceil\rrbracket\ \texttt{in}\ x$
$\displaystyle=\llbracket\Gamma\vdash t:\lceil\Psi\vdash A\rceil\rrbracket$

The last equation requires a second thought. Indeed, this equation does not
normally hold. In fact, $\texttt{box}~{}\texttt{let}~{}\texttt{box}~{}x=t\
\texttt{in}\ x=t$ is equivalent to requiring $\flat$ to be idempotent. In our
model, this turns out to be true, as we can see from

$\displaystyle\flat\flat F(\Psi)=\flat F(\top)=F(\top)=\flat F(\Psi)$

That is, $\flat$ is _definitionally_ idempotent, which allows us to conclude
the equation. The fact that we rely on the idempotency of the $\flat$ modality
implies that the model can only support a two-level modal system.

##  6\. Dependently Typed Case

In the previous sections, we outlined the interpretation of a simply typed
variant of Cocon to a presheaf model. In this section, we demonstrate how the
idea can be extended to the dependently typed case. In the dependently typed
case, both domain level and computation level have dependent function spaces.
This can be used to model intrinsically simply typed languages in the domain
level.

⬇

ty : type. trm : ty $\rightarrow~{}$ type.

o : ty. lam : $\Pi$ a : ty, $\Pi$ b : ty, (trm a $\rightarrow~{}$ trm b)
$\rightarrow~{}$ trm (arr a b).

arr : ty $\rightarrow~{}$ ty $\rightarrow~{}$ ty. app : $\Pi$ a : ty, $\Pi$ b
: ty, trm (arr a b) $\rightarrow~{}$ trm a $\rightarrow~{}$ trm b.

In trm, we use the type parameter to keep track of the object-level type of an
object-level term. We still use HOAS to encode the case of lambda abstraction.
As in the simply typed case, we have two distinct function spaces in
dependently typed Cocon as well: the weak space that is used in the domain
level and is used for HOAS, and the strong space that is used in the
computation level and supports induction.

###  6.1. A Simplified Cocon

To model a dependently typed variant of Cocon capable of encoding this object
language, we present the modification to the syntax of the simply typed Cocon
in Fig. 8. In the syntax for domain-level types, we add the types for the
domain language as well as turn the simple function space into a dependent
one. For the terms, we add the corresponding constructors of domain level
types, trm and ty. Compared to Pientka et al. (2019), this version of Cocon is
simplified by removing the full hierarchy of universes; as a consequence,
types and terms are separated.

${{{\begin{array}[]{p{4.8cm}@{~}l@{~}r@{~}l}Domain-level
types}}~{&A,B\hfil~{}&\;\mathrel{::=}~{}&\texttt{ty}\,\mid\,\texttt{trm}\;M\,\mid\,\Pi
x:A.B\\\ Domain-level terms}}~{&M,N\hfil~{}&\;\mathrel{::=}~{}&\lambda x.M\mid
M\,N\mid x\mid\lfloor t\rfloor_{\sigma}\mid c\\\ Domain-level
Constants}}~{&c\hfil~{}&\;\mathrel{::=}~{}&\mathtt{o}\,\mid\,\mathtt{arr}\,\mid\,\mathtt{lam}\,\mid\,\mathtt{app}\end{array}$
Figure 8. Syntax of dependent Cocon $\begin{array}[]{c}\lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\Gamma\vdash\Psi:\texttt{ctx}$}~{}~{}The domain-level
context $\Psi$ is well-formed\newline }}\lx@intercol\\\
\Gamma\vdash\cdot:\texttt{ctx}\qquad\Gamma\vdash\psi:\texttt{ctx}\Gamma(\psi)=\texttt{ctx}\qquad\Gamma\vdash\Phi,x:A:\texttt{ctx}\lx@proof@logical@and\Gamma\vdash\Phi:\texttt{ctx}\Gamma;\Psi\vdash
A\texttt{ type}\par\\\\[9.00002pt] \lx@intercol\vtop{\hbox to341.43306pt{From
now on, whenever $\Psi$ presents, $\Gamma\vdash\Psi:\texttt{ctx}$ is
assumed.\newline }}\lx@intercol\\\ \lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\Gamma;\Psi\vdash A\texttt{ type}$} ~{}~{} The
domain-level type $A$ is well-formed\newline }}\lx@intercol\\\
\inferrule*{}{\Gamma;\Psi\vdash\texttt{ty}\texttt{
type}}\qquad\inferrule*{\Gamma;\Psi\vdash
M:\texttt{ty}}{\Gamma;\Psi\vdash\texttt{trm}\;M\texttt{
type}}\qquad\inferrule*{\Gamma;\Psi\vdash A\texttt{ type}\\\
\Gamma;\Psi,x:A\vdash B\texttt{ type}}{\Gamma;\Psi\vdash\Pi x:A.B\texttt{
type}}\par\\\\[18.00003pt] \lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\Gamma;\Psi\vdash M:A$} ~{}~{} Term $M$ has type $A$
in domain-level context $\Psi$ and context $\Gamma$\newline }}\lx@intercol\\\
\inferrule*{x:A\in\Psi}{\Gamma;\Psi\vdash
x:A}\qquad\inferrule*{\Gamma;\Psi,x:A\vdash M:B}{\Gamma;\Psi\vdash\lambda
x.M:\Pi x:A.B}\qquad\inferrule*{\Gamma;\Psi\vdash M:\Pi x:A.B\\\
\Gamma;\Psi\vdash N:A}{\Gamma;\Psi\vdash M\;N:[N/x]B}\par\\\\[4.5pt]
\inferrule*{\Gamma\vdash t:\lceil\Phi\vdash A\rceil\text{ or }\Gamma\vdash
t:\lceil\Phi\vdash_{v}A\rceil\\\
\Gamma;\Psi\vdash\sigma:\Phi}{\Gamma;\Psi\vdash\lfloor
t\rfloor_{\sigma}:[\sigma]A}\par\qquad\par\inferrule*{\Gamma;\Psi\vdash M:A\\\
\Gamma;\Psi\vdash A\equiv B\texttt{ type}}{\Gamma;\Psi\vdash
M:B}\par\qquad\par\inferrule*{}{\Gamma;\Psi\vdash\mathtt{o}:\texttt{ty}}\par\\\\[4.5pt]
\inferrule*{\Gamma;\Psi\vdash a:\texttt{ty}\\\ \Gamma;\Psi\vdash
b:\texttt{ty}}{\Gamma;\Psi\vdash\mathtt{arr}\;a\;b:\texttt{ty}}\par\qquad\par\inferrule*{\Gamma;\Psi\vdash
a:\texttt{ty}\\\ \Gamma;\Psi\vdash b:\texttt{ty}\\\ \Gamma;\Psi\vdash
f:\texttt{trm}\;a\to\texttt{trm}\;b}{\Gamma;\Psi\vdash\mathtt{lam}\;a\;b\;f:\texttt{trm}\;(\mathtt{arr}\;a\;b)}\par\\\\[4.5pt]
\inferrule*{\Gamma;\Psi\vdash a:\texttt{ty}\\\ \Gamma;\Psi\vdash
b:\texttt{ty}\\\ \Gamma;\Psi\vdash m:\texttt{trm}\;(\mathtt{arr}\;a\;b)\\\
\Gamma;\Psi\vdash
n:\texttt{trm}\;a}{\Gamma;\Psi\vdash\mathtt{app}\;a\;b\;m\;n:\texttt{trm}\;b}\par\\\\[18.00003pt]
\lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\Gamma;\Psi\vdash\sigma:\Phi$} ~{}~{} Substitution
$\sigma$ provides a mapping from the (domain) context $\Phi$ to $\Psi$\newline
}}\lx@intercol\\\ \inferrule*{\Gamma\vdash\Psi\texttt{
ctx}}{\Gamma;\Psi\vdash\cdot:\cdot}\qquad\inferrule*{\Gamma;\Psi\vdash\sigma:\Phi\\\
\Gamma;\Psi\vdash
M:[\sigma]A}{\Gamma;\Psi\vdash\sigma,M:\Phi,x:A}\qquad\inferrule*{\Gamma\vdash\Psi,\overrightarrow{x:A}\texttt{
ctx}}{\Gamma;\Psi,\overrightarrow{x:A}\vdash\mathsf{wk}_{\widehat{\Psi}}:\Psi}\end{array}$
Figure 9. Domain-level judgments

The typing rules are shown in Fig. 9 and are changed more significantly. Since
domain-level terms can appear in types now, we need to add well-formedness
condition for domain-level contexts, $\Gamma\vdash\Psi\texttt{ ctx}$, and
types, $\Gamma;\Psi\vdash A\texttt{ type}$. In particular, $\texttt{trm}\;M$
is well-formed only if $M$ has type ty. In the typing rules, the application
rule and the unbox rule shows how dependent types are involved. In particular,
in the unbox case, the substitution $\sigma$ is applied to $A$ as the
resulting type. Without loss of generality, we require object-level
constructors to be fully applied, e.g. $\mathtt{arr}\ a$ is not a valid
domain-level term. It helps to simplify the semantic interpretation and allows
us to focus on the essential idea of the development.

$\begin{array}[]{c}\lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\vdash\Gamma$}~{}~{} $\Gamma$ is a well-formed
context\newline }}\lx@intercol\\\
\inferrule*{}{\vdash\cdot}\qquad\inferrule*{\vdash\Gamma\\\
\Gamma\vdash\breve{\tau}\texttt{
type}}{\vdash\Gamma,x:\breve{\tau}}\\\\[9.00002pt] \lx@intercol\vtop{\hbox
to341.43306pt{\framebox{$\Gamma\vdash\breve{\tau}\texttt{ type}$}~{}~{}
$\breve{\tau}$ is a well-formed type in context $\Gamma$\newline
}}\lx@intercol\\\ \inferrule*{}{\Gamma\vdash\texttt{ctx}\texttt{
type}}\qquad\inferrule*{\Gamma\vdash\breve{\tau}_{1}\texttt{ type}\\\
\Gamma,y:\breve{\tau}_{1}\vdash\tau_{2}\texttt{
type}}{\Gamma\vdash(y:\breve{\tau}_{1})\Rightarrow\tau_{2}\texttt{
type}}\qquad\inferrule*{\Gamma;\Psi\vdash A\texttt{
type}}{\Gamma\vdash\lceil\Psi\vdash A\rceil\texttt{
type}}\qquad\inferrule*{\Gamma;\Psi\vdash A\texttt{
type}}{\Gamma\vdash\lceil\Psi\vdash_{v}A\rceil\texttt{ type}}\\\\[9.00002pt]
\lx@intercol\vtop{\hbox to341.43306pt{\framebox{$\Gamma\vdash C:T$}~{}~{}
Contextual object $C$ has contextual type $T$\newline }}\lx@intercol\\\
\inferrule*{}{\Gamma\vdash(\widehat{\Psi}\vdash M):(\Psi\vdash
A)}\qquad\inferrule*{x:A\in\Psi}{\Gamma\vdash(\widehat{\Psi}\vdash
x):(\Psi\vdash_{v}A)}\qquad\inferrule*{x:\lceil\Phi\vdash_{v}A\rceil\in\Gamma\\\
\Gamma;\Psi\vdash\mathsf{wk}_{\widehat{\Psi}}:\Phi}{\Gamma\vdash(\widehat{\Psi}\vdash\lfloor
x\rfloor_{\mathsf{wk}_{\widehat{\Psi}}}):(\Psi\vdash_{v}A)}\par\\\\[9.00002pt]
\lx@intercol\vtop{\hbox to341.43306pt{\framebox{$\Gamma\vdash t:\breve{\tau}$}
~{}~{} Term $t$ has computation type $\breve{\tau}$\newline }}\lx@intercol\\\
\inferrule*{y:\breve{\tau}\in\Gamma}{\Gamma\vdash
y:\breve{\tau}}\qquad\inferrule*{\Gamma\vdash C:T}{\Gamma\vdash\lceil
C\rceil:\lceil T\rceil}\qquad\inferrule*{\Gamma,y:\breve{\tau_{1}}\vdash
t:\tau_{2}}{\Gamma\vdash\texttt{fn}\;y\Rightarrow
t:(y:\breve{\tau_{1}})\Rightarrow\tau_{2}}\\\\[9.00002pt]
\inferrule*{\Gamma\vdash t:(y:\breve{\tau_{1}})\Rightarrow\tau_{2}\\\
\Gamma\vdash s:\breve{\tau_{1}}}{\Gamma\vdash
t\;s:[s/y]\tau_{2}}\qquad\inferrule*{\Gamma\vdash t:\breve{\tau}_{1}\\\
\Gamma\vdash\breve{\tau}_{1}\equiv\breve{\tau}_{2}\texttt{ type}}{\Gamma\vdash
t:\breve{\tau}_{2}}\par\\\\[13.50002pt] \lx@intercol\vtop{\hbox
to341.43306pt{Recursor over $\texttt{ty}$:
$\mathcal{I}=(\psi:\texttt{ctx})\Rightarrow(y:\lceil\psi\vdash\texttt{ty}\rceil)\Rightarrow\tau$\newline
}}\lx@intercol\\\ \inferrule*{\Gamma\vdash
t:\lceil\Psi\vdash\texttt{ty}\rceil\\\ \Gamma\vdash
b_{\mathtt{o}}:\mathcal{I}\\\ \Gamma\vdash
b_{\mathtt{arr}}:\mathcal{I}}{\Gamma\vdash\texttt{rec}^{\mathcal{I}}\;(b_{\mathtt{o}}\,\mid\,b_{\mathtt{arr}})\;\Psi\;t:[\Psi,t/\psi,y]\tau}\par\\\\[9.00002pt]
\text{Branch for the $\mathtt{o}$
case}\quad\inferrule*{\Gamma,\psi:\texttt{ctx}\vdash
t_{\mathtt{o}}:[\lceil\psi\vdash\mathtt{o}\rceil/y]\tau}{\Gamma\vdash(\psi\mapsto
t_{\mathtt{o}}):\mathcal{I}}\\\\[9.00002pt] \text{Branch for the
$\mathtt{arr}$
case}\par\inferrule*{\Gamma,\psi:\texttt{ctx},m,n:\lceil\psi\vdash\texttt{ty}\rceil,f_{m}:[m/y]\tau,f_{n}:[n/y]\tau\vdash
t_{arr}:[\lceil\psi\vdash\mathtt{arr}\lfloor m\rfloor\lfloor
n\rfloor\rceil/y]\tau}{\Gamma\vdash(\psi,m,n,f_{m},f_{n}\mapsto
t_{\mathtt{arr}}):\mathcal{I}\par}\\\\[13.50002pt] \lx@intercol\vtop{\hbox
to341.43306pt{ Recursor over $\texttt{trm}$:
$\mathcal{I}=(\psi:\texttt{ctx})\Rightarrow(z:\lceil\vdash\texttt{ty}\rceil)\Rightarrow(y:\lceil\psi\vdash\texttt{trm}\;\lfloor
z\rfloor_{\cdot}\rceil)\Rightarrow\tau$\newline }}\lx@intercol\\\
\inferrule*{\Gamma\vdash t:\lceil\vdash\texttt{ty}\rceil\\\ \Gamma\vdash
t^{\prime}:\lceil\Psi\vdash\texttt{trm}\;\lfloor t\rfloor_{\cdot}\rceil\\\
\Gamma\vdash b_{v}:\mathcal{I}\\\ \Gamma\vdash b_{\mathtt{lam}}:\mathcal{I}\\\
\Gamma\vdash
b_{\mathtt{app}}:\mathcal{I}}{\Gamma\vdash\texttt{rec}^{\mathcal{I}}\;(b_{v}\,\mid\,b_{\mathtt{lam}}\,\mid\,b_{\mathtt{app}})\;\Psi\;t\;t^{\prime}:[\Psi,t,t^{\prime}/\psi,z,y]\tau}\par\\\\[9.00002pt]
\text{Branch for the variable
case}\quad\inferrule*{\Gamma,\psi:\texttt{ctx},a:\lceil\vdash\texttt{ty}\rceil,t:\lceil\psi\vdash_{v}\texttt{trm}\;\lfloor
a\rfloor_{\cdot}\rceil\vdash t_{v}:[a,t/z,y]\tau}{\Gamma\vdash(\psi,a,t\mapsto
t_{v}):\mathcal{I}\par}\\\\[9.00002pt] \text{Branch for the $\mathtt{lam}$
case}\par\inferrule*{\Gamma,\psi:\texttt{ctx},a,b:\lceil\vdash\texttt{ty}\rceil,m:\lceil\psi,x:\texttt{trm}\;\lfloor
a\rfloor_{\cdot}\vdash\texttt{trm}\;\lfloor b\rfloor_{\cdot}\rceil,\\\
f_{m}:[(\psi,\texttt{trm}\;\lfloor
a\rfloor_{\cdot}),b,m/\psi,x,y]\tau\vdash{t_{\mathtt{lam}}}:{[\lceil\vdash\mathtt{arr}\lfloor
a\rfloor\lfloor b\rfloor\rceil,\lceil\psi\vdash\mathtt{lam}\lfloor
a\rfloor_{\cdot}\lfloor b\rfloor_{\cdot}(\lambda x.\lfloor
m\rfloor)\rceil/z,y]\tau}}{\Gamma\vdash(\psi,a,b,m,f_{m}\mapsto
t_{\mathtt{lam}}):\mathcal{I}}\par\\\\[9.00002pt] \text{Branch for the
$\mathtt{app}$
case}\par\inferrule*{\Gamma,\psi:\texttt{ctx},a,b:\lceil\vdash\texttt{ty}\rceil,m:\lceil\psi\vdash\texttt{trm}{(\mathtt{arr}\lfloor
a\rfloor_{\cdot}\lfloor
b\rfloor_{\cdot})}\rceil,n:\lceil\psi\vdash\texttt{trm}{\lfloor
a\rfloor_{\cdot}}\rceil,\\\ f_{m}:[\lceil\vdash\mathtt{arr}\lfloor
a\rfloor\lfloor b\rfloor\rceil,m/z,y]\tau,f_{n}:[a,n/z,y]\tau\vdash
t_{\mathtt{app}}:{[b,\lceil\psi\vdash\mathtt{app}\lfloor
a\rfloor_{\cdot}\lfloor b\rfloor_{\cdot}\lfloor m\rfloor\lfloor
n\rfloor\rceil/z,y]\tau}}{\Gamma\vdash(\psi,a,b,m,n,f_{m},f_{n}\mapsto
t_{\mathtt{app}}):\mathcal{I}}\par\end{array}$ Figure 10. Judgments in the
computation level

The computation-level judgments are shown in Fig. 10. Similar to the domain
level, we also need well-formedness judgments for computation-level contexts
and types. Unlike Cocon defined in Pientka et al. (2019), we need a separate
judgment for well-formed types because we do not have universes here. The
computation-level language is also dependently typed, as shown in the
application rule. We also formulate the induction principle for trm and ty.
The case for ty is straightforward as it is a normal algebraic data type. For
trm, in addition to the cases of $\mathtt{lam}$ and $\mathtt{app}$, we need a
case for variables as in the simply typed settings.

###  6.2. Categories with Families

In the previous section, we showed that we can regard the domain-level
language as a cartesian closed category $\mathbb{D}$ and use the Yoneda
embedding to embed the domain level into the presheaf category
$\widehat{\mathbb{D}}$, which is regarded as the computation-level language.
Interestingly, this model can be extended to the case of dependently typed
domain languages. In this case, $\mathbb{D}$ needs to have enough structure to
model dependent types, and the model we consider here is categories with
families (CwFs) (Dybjer, 1995; Hofmann, 1997).

###### Definition 6.1.

A _category with families_ $\mathcal{C}$ consists of the following data:

  1. (1)

a terminal object $\top$,

  2. (2)

a functor $\textsf{Ty}:\mathcal{C}^{op}\to\mathpzc{Set}$, whose action on
morphisms we denote as $-\\{\sigma\\}:\mathsf{Ty}(\Phi)\to\mathsf{Ty}(\Psi)$
for $\sigma:\Psi\to\Phi$,

  3. (3)

for $\Phi\in\mathcal{C}$ and $A\in\mathsf{Ty}(\Phi)$, a set
$\mathsf{Tm}(\Phi,A)$, such that:

     * •

for $\sigma:\Psi\to\Phi$ and $t\in\mathsf{Tm}(\Phi,A)$,
$t\\{\sigma\\}\in\mathsf{Tm}(\Psi,A\\{\sigma\\})$, and

     * •

the equations $t\\{id_{\Phi}\\}=t$ and
$t\\{\sigma\\}\\{\delta\\}=t\\{\sigma\circ\delta\\}$ are valid.

  4. (4)

a context comprehension $-.-$ so that given $\Phi\in\mathcal{C}$ and
$A\in\mathsf{Ty}(\Phi)$, $\Phi.A\in\mathcal{C}$,

  5. (5)

for $\Phi\in\mathcal{C}$ and $A\in\mathsf{Ty}(\Phi)$, a projection morphism of
context comprehension $p(A):\Phi.A\to\Phi$,

  6. (6)

for $\Phi\in\mathcal{C}$ and $A\in\mathsf{Ty}(\Phi)$, a variable projection
$v_{A}\in\mathsf{Tm}(\Phi.A,A\\{p(A)\\})$, and

  7. (7)

for $\sigma:\Psi\to\Phi$, $A\in\mathsf{Ty}(\Phi)$, and
$t\in\mathsf{Tm}(\Psi,A\\{\sigma\\})$, a unique extension morphism
$\langle\sigma,t\rangle:\Psi\to\Phi.A$.

The following equations hold:

  1. (1)

$p(A)\circ\langle\sigma,t\rangle=\sigma$,

  2. (2)

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

  3. (3)

$\sigma=\langle p(A)\circ\sigma,v_{T}\\{\sigma\\}\rangle$ where
$\sigma:\Phi\to\Psi.A$.

We regard the objects in $\mathcal{C}$ as contexts and the morphisms as
substitutions of one context for another. Based on this understanding,
$\mathsf{Ty}(\Phi)$ denotes the set of semantic types in context $\Phi$. Given
a semantic type $A\in\mathsf{Ty}(\Phi)$, $A\\{\sigma\\}$ is thus applying the
substitution $\sigma$ to $A$ given $\sigma:\Psi\to\Phi$. Based on their
definitions, we can prove the following properties of type and term
substitutions. Given $A\in\mathsf{Ty}(\Phi)$, $\sigma:\Psi\to\Phi$,
$\delta:\Psi^{\prime}\to\Psi$, $t:\mathsf{Tm}(\Phi,A)$:

$\displaystyle A\\{id_{\Phi}\\}$ $\displaystyle=A$ $\displaystyle
A\\{\sigma\\}\\{\delta\\}$ $\displaystyle=A\\{\sigma\circ\delta\\}$

$\mathsf{Tm}(\Phi,A)$ denotes the set of semantic terms of type $A$ in context
$\Phi$. Given a term $t\in\mathsf{Tm}(\Phi,A)$ and a substitution
$\sigma:\Psi\to\Phi$, $t\\{\sigma\\}:\mathsf{Tm}(\Psi,A\\{\sigma\\})$ is the
result of applying $\sigma$ to $t$. Note that the type of this term is
$A\\{\sigma\\}$, so CwFs are capable of handling dependent types.

Sometimes, given a substitution $\sigma:\Psi\to\Phi$ and
$A\in\mathsf{Ty}(\Phi)$, we would like to obtain another substitution
$q(\sigma,A):\Psi.A\\{\sigma\\}\to\Phi.A$. This substitution is needed below
when we define substitution for $\Pi$ types. We can define

$\displaystyle q(\sigma,A):=\langle\sigma\circ
p(A\\{\sigma\\}),v_{A\\{\sigma\\}}\rangle$

By applying the property of $p(A\\{\sigma\\})$, we can see that the following
diagram is a pullback:

${\Psi.A\\{\sigma\\}}$${\Phi.A}$${\Psi}$${\Phi}$$\scriptstyle{q(\sigma,A)}$$\scriptstyle{p(A\\{\sigma\\})}$$\scriptstyle{p(A)}$$\scriptstyle{\sigma}$

We shall work with telescopes of types. A _telescope_ of types in context
$\Phi$ is a sequence of types $A_{1},A_{2},\dots,A_{n}$ such that
$A_{1}\in\mathsf{Ty}(\Phi)$, $A_{2}\in\mathsf{Ty}(\Phi.A_{1})$, …,
$A_{n}\in\mathsf{Ty}(\Phi.A_{1}.\dots A_{n-1})$. We write $\vec{A}$ to range
over telescopes and extend context comprehension, substitution and projection
to telescopes in the canonical way. That is, we write $\Phi.\vec{A}$ for
$\Phi.A_{1}.\dots.A_{n}$ and $p(\vec{A})$ for $p(A_{1})\circ\dots\circ
p(A_{n})$.

Up until this point, we have obtained a generic categorical structure for
dependent type theory. In order to model the dependent function space, we need
a semantic type former.

###### Definition 6.2.

(Hofmann, 1997) Semantic $\Pi$ types in a CwF $\mathcal{C}$ have the following
data:

  1. (1)

A semantic type $\Pi(A,B)\in\mathsf{Ty}(\Phi)$ for each
$A\in\mathsf{Ty}(\Phi)$ and $B\in\mathsf{Ty}(\Phi.A)$,

  2. (2)

a semantic term $\Lambda_{A,B}(M)\in\mathsf{Tm}(\Phi,\Pi(A,B))$ for each
$M\in\mathsf{Tm}(\Phi.A,B)$, and

  3. (3)

a semantic term $\mathsf{App}_{A,B}(M,N)\in\mathsf{Tm}(\Phi,B\\{\langle
id_{\Phi},N\rangle\\})$ for each $M\in\mathsf{Tm}(\Phi,\Pi(A,B))$ and
$N\in\mathsf{Tm}(\Phi,A)$.

so that the following axioms are satisfied:

  1. (1)

$\Pi(A,B)\\{\sigma\\}=\Pi(A\\{\sigma\\},B\\{q(\sigma,A)\\})\in\mathsf{Ty}(\Psi)$
for $\sigma:\Psi\to\Phi$,

  2. (2)

$\Lambda_{A,B}(M)\\{\sigma\\}=\Lambda_{A\\{\sigma\\},B\\{q(\sigma,A)\\}}(M\\{q(\sigma,A)\\})\in\mathsf{Tm}(\Psi,\Pi(A,B)\\{\sigma\\})$
for $M\in\mathsf{Tm}(\Phi.A,B)$ and $\sigma:\Psi\to\Phi$,

  3. (3)

$\mathsf{App}_{A,B}(M,N)\\{\sigma\\}=\mathsf{App}_{A\\{\sigma\\},B\\{q(\sigma,A)\\}}(M\\{\sigma\\},N\\{\sigma\\})\in\mathsf{Tm}(\Psi,B\\{\langle
id_{\Phi},N\rangle\\}\\{\sigma\\})=\mathsf{Tm}(\Psi,B\\{\langle\sigma,N\\{\sigma\\}\rangle\\})$
for $M\in\mathsf{Tm}(\Phi,\Pi(A,B))$, $N\in\mathsf{Tm}(\Phi,A)$ and
$\sigma:\Psi\to\Phi$,

  4. (4)

$\mathsf{App}_{A,B}(\Lambda_{A,B}(M),N)=M\\{\langle
id_{\Phi},N\rangle\\}\in\mathsf{Tm}(\Phi,B\\{\langle id_{\Phi},N\rangle\\})$
for each $M\in\mathsf{Tm}(\Phi.A,B)$ and $N\in\mathsf{Tm}(\Phi,A)$, and

  5. (5)

$\Lambda_{A,B}(\mathsf{App}_{A,B}(M\\{p(A)\\},v_{A}))=M\in\mathsf{Tm}(\Phi,\Pi(A,B))$.

We often omit the subscripts of $\Lambda$ and $\mathsf{App}$ in favor of
conciseness when they can be unambiguously inferred. For example, the fourth
axiom can be more concisely expressed as
$\mathsf{App}(\Lambda(M),N)=M\\{\langle id_{\Phi},N\rangle\\}$.

One characteristic of this framework is that the consistency of equations
involves reasoning about equality between sets. Consider the third equation
above. We can transform the left hand side as follows:

$\displaystyle\mathsf{App}(M,N)\\{\sigma\\}$
$\displaystyle\in\mathsf{Tm}(\Phi,B\\{\langle
id_{\Psi},N\rangle\\}\\{\sigma\\})$
$\displaystyle=\mathsf{Tm}(\Phi,B\\{\langle id_{\Psi},N\rangle\circ\sigma\\})$
property of extension morphism
$\displaystyle=\mathsf{Tm}(\Phi,B\\{\langle\sigma,N\\{\sigma\\}\rangle\\})$

The right hand side has:

$\displaystyle\mathsf{App}(M\\{\sigma\\},N\\{\sigma\\})$
$\displaystyle\in\mathsf{Tm}(\Phi,B\\{q(\sigma,A)\\}\\{\langle
id_{\Phi},N\\{\sigma\\}\rangle\\})$
$\displaystyle=\mathsf{Tm}(\Phi,B\\{q(\sigma,A)\circ\langle
id_{\Phi},N\\{\sigma\\}\rangle\\})$
$\displaystyle=\mathsf{Tm}(\Phi,B\\{\langle\sigma\circ
p(A\\{\sigma\\}),v_{A\\{\sigma\\}}\rangle\circ\langle
id_{\Phi},N\\{\sigma\\}\rangle\\})$
$\displaystyle=\mathsf{Tm}(\Phi,B\\{\langle\sigma,N\\{\sigma\\}\rangle\\})$

As both terms belong to the same set, the equation is well-defined.

Combining the definition of a CwF with $\Pi$ types, we are able to capture the
nature of dependent types with dependent function spaces in both the domain
level and the computation level. We can also axiomatize other types like ty
and trm and their constructors. However, we need more to interpret Cocon:

  1. (1)

CwFs do not provide a direct connection between the domain and the computation
level;

  2. (2)

the domain-level terms exhibit different substitution behavior from the
computation terms.

To overcome these issues, we can extend the model presented in Section 2 by
requiring the domain category to possess structure of a CwF. We will expand
our discussion in the next section.

###  6.3. Presheaves over a Small Category with Families

Having introduced an appropriate notion of model for dependent type theories,
we can now generalise the construction from Section 4 to the case of dependent
domain languages.

As in the simply-typed case, we begin with a term model $\mathbb{D}$ of the
domain-level type theory. The main difference is that in the dependent case,
this category has the structure of a CwF instead of being just cartesian
closed. In order to interpret the computation types of Cocon, we work in the
presheaf category $\widehat{\mathbb{D}}$. This category has enough structure
to interpret Cocon computations and also embeds $\mathbb{D}$ fully and
faithfully via the Yoneda embedding.

#### A Universe for a small CwF

For working with the internal type theory of $\widehat{\mathbb{D}}$, it is
again convenient to capture the embedding of $\mathbb{D}$ into
$\widehat{\mathbb{D}}$ in terms of a Tarski-style universe. It is given by the
following term and type constants in the internal type theory of
$\widehat{\mathbb{D}}$. The types $\mathsf{Ctx}$ and $\texttt{El}\,\Phi$
generalize Obj and $\texttt{El}\,a$ from Section 4 to the dependent case:

⋅ ⊢Ctx type

Φ: Ctx ⊢El (Φ) type

Φ: Ctx ⊢Ty(Φ) type

Φ: Ctx, A : Ty(Φ) ⊢Tm(Φ, A) type

⋅ ⊢⊤ : Ctx

Φ: Ctx, A : Ty(Φ) ⊢Φ.A : Ctx

Φ: Ctx ⊢! : El (Φ) →El (⊤)

Φ: Ctx, A : Ty(Φ) ⊢p : El (Φ.A) →El (Φ)

Φ: Ctx, A : Ty(Φ) ⊢v : Tm(Φ.A, A{p})

Φ: Ctx, Ψ: Ctx, A : Ty(Ψ), σ: El (Φ) →El (Ψ) ⊢A{σ} : Ty(Φ)

Φ,Ψ: Ctx, A : Ty(Ψ), M : Tm(Ψ, A), σ: El (Φ) →El (Ψ) ⊢M{σ} : Tm(Φ, A{σ})

Ψ, Φ: Ctx, σ: El (Ψ) →El (Φ), A : Ty(Φ), M : Tm(Ψ, A{σ})
⊢$\langle\sigma,M\rangle$ : El (Ψ) →El (Φ.A)

Let us outline the interpretation of these constants in $\widehat{\mathbb{D}}$
next. Recall from Section 3 that contexts are objects of
$\widehat{\mathbb{D}}$, types in context $\Gamma$ are presheaves
$\widehat{\mathsf{Ty}}(\Gamma)={{\scriptstyle\int}\Gamma}^{\mathrm{op}}\to\mathpzc{Set}$,
and terms are sections of the projections maps $p\colon\Gamma.A\to\Gamma$ in
$\widehat{\mathbb{D}}$. We detail the required structure used in the
interpretation.

The interpretation of the types $\mathsf{Ctx}$ and $\texttt{El}\,(\Phi)$ is as
follows:

$\displaystyle\mathsf{Ctx}$ $\displaystyle:\widehat{\mathsf{Ty}}(\top)$
$\displaystyle\mathsf{Ctx}(\Psi,*)$
$\displaystyle=\\{\vec{A}\mid\text{$\vec{A}$ is a telescope of types in
context~{}$\Psi$}\\}$
$\displaystyle\mathsf{Ctx}(\sigma:(\Psi^{\prime},*)\to(\Psi,*))$
$\displaystyle=\vec{A}\mapsto\vec{A}\\{\sigma\\}$ El
$\displaystyle:\widehat{\mathsf{Ty}}(\top.\mathsf{Ctx})$
$\displaystyle\texttt{El}\,(\Psi,(*,\vec{A}))$
$\displaystyle=\\{\sigma\in\mathbb{D}(\Psi,\Psi.\vec{A})\mid
p(\vec{A})\circ\sigma=\mathsf{id}_{\Psi}\\}$
$\displaystyle\texttt{El}\,(\sigma:(\Psi^{\prime},(*,\vec{A}\\{\sigma\\})\to(\Psi,(*,\vec{A})))$
$\displaystyle=f\in\mathbb{D}(\Psi,\Psi.\vec{A})\mapsto f\\{\sigma\\}$

The types of the form $\mathsf{Ty}(\Phi)$ in the internal type theory are
interpreted as follows:

Ty $\displaystyle:\widehat{\mathsf{Ty}}(\top.\mathsf{Ctx})$
$\displaystyle\mathtt{Ty}(\Psi,(*,\vec{A}))$
$\displaystyle=\mathsf{Ty}(\Psi.\vec{A})$
$\displaystyle\mathtt{Ty}(\sigma:(\Psi^{\prime},(*,\vec{A}\\{\sigma\\})\to(\Psi,(*,\vec{A})))$
$\displaystyle=B\in\mathsf{Ty}(\Psi.\vec{A})\mapsto B\\{q(\sigma,\vec{A})\\}$

Here Ty on the right hand side is given by the CwF structure of the domain
category $\mathbb{D}$. That is, Ty is defined in terms of Ty in the domain
category, so all types of the domain level can be referred to as terms in the
presheaf category.

The types of the form $\mathtt{Tm}(\Phi,A)$ are interpreted as follows.

Tm $\displaystyle:\widehat{\mathsf{Ty}}(\top.\mathsf{Ctx}.\texttt{Ty})$
$\displaystyle\texttt{Tm}(\Psi,(*,\vec{A},B))$
$\displaystyle=\mathsf{Tm}(\Psi.\vec{A},B)$ $\displaystyle\texttt{Tm}(\sigma)$
$\displaystyle=M\mapsto M\\{q(\sigma,\vec{A})\\}$

Similar to Ty, Tm is also defined by terms $\mathsf{Tm}$ in the domain
category $\mathbb{D}$.

For spelling out the interpretation of the remaining terms, we need to give a
manageable presentation of the semantic interpretation of function types of
the form $\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})$. In the simply
typed case, the Yoneda lemma shows an isomorphism between
$\mathbb{D}(\Phi,\Phi^{\prime})$ and
$\widehat{\mathbb{D}}(\mathrm{y}(\Phi),\mathrm{y}(\Phi^{\prime}))$. In the
dependently typed case, this isomorphism remains: the function space
$\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})$ is isomorphic to
$\mathbb{D}(\Phi,\Phi^{\prime})$, as proved by the following lemma:

###### Lemma 6.3.

The interpretation of

$\Phi{:}\,\mathsf{Ctx},\Phi^{\prime}{:}\,\mathsf{Ctx}\vdash\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})\texttt{
type}$

in the internal type theory of $\widehat{\mathbb{D}}$ is isomorphic to the
following presheaf Hom:

Hom
$\displaystyle\colon\widehat{\mathsf{Ty}}(\top.\mathsf{Ctx}.\mathsf{Ctx}\\{p\\})$
$\displaystyle\textsf{Hom}(\Psi,(*,\vec{A},\vec{B}))$
$\displaystyle=\\{\sigma\in\mathbb{D}(\Psi.\vec{A},\Psi.\vec{B})\mid
p(\vec{B})\circ\sigma=p(\vec{A})\\}$

###### Proof.

For one direction, as given in Section 3, the type
$\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})$ in the syntax is
interpreted to a function $f$ which takes $\sigma\colon\Phi\to\Psi$ and
$M:\Phi\to\Phi.\vec{A}\\{\sigma\\}$ and outputs
$\Phi\to\Phi.\vec{B}\\{\sigma\\}$ that is natural in $\Phi$. Then we obtain
$f(p_{\vec{A}}:\Psi.\vec{A}\to\Psi,v:\Psi.\vec{A}\to\Psi.\vec{A}.\vec{A}\\{p_{\vec{A}}\\}):\Psi.\vec{A}\to\Psi.\vec{A}.\vec{B}\\{p_{\vec{A}}\\}$,
such that $p_{\vec{A}}\circ f(p_{\vec{A}},v)=\mathsf{id}_{\Psi.\vec{A}}$. We
obtain $\Psi.\vec{A}\to\Psi.\vec{B}$ by composing $q(p_{\vec{A}},\vec{B})$
with $f(p_{\vec{A}},v)$.

The other direction is given $\sigma:\Psi.\vec{A}\to\Psi.\vec{B}$,
$\delta:\Phi\to\Psi$ and $\sigma^{\prime}:\Phi\to\Phi.\vec{A}\\{\delta\\}$ and
outputs $\Phi\to\Phi.\vec{B}\\{\delta\\}$.

${\Psi.\vec{A}}$${\Psi.\vec{B}}$${\Phi}$${\Phi.\vec{A}\\{\delta\\}}$${\Phi.\vec{B}\\{\delta\\}}$$\scriptstyle{\sigma}$$\scriptstyle{\sigma^{\prime}}$$\scriptstyle{q(\delta,\vec{A})}$$\scriptstyle{q(\delta,\vec{B})}$

Thus the morphism $\Phi\to\Phi.\vec{B}\\{\delta\\}$ is obtained by composing
$\sigma^{\prime}$ with the unique morphism that makes the above square a
pullback. ∎

In the following, we shall apply the isomorphism from the lemma implicitly and
treat the interpretation of
$\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})$ to be the same as Hom.

With this convention, we are able to give an explicit interpretation for the
judgments that we give at the beginning of this section. Recall, for example,
the term for type substitution:

$\displaystyle\Phi:\mathsf{Ctx},\,\Psi:\mathsf{Ctx},\,A:\mathtt{Ty}(\Psi),\,\sigma:\texttt{El}\,(\Phi)\to\texttt{El}\,(\Psi)\vdash
A\\{\sigma\\}:\mathtt{Ty}(\Phi)$

This term $A\\{\sigma\\}$ is interpreted as the following natural
transformation:

$\displaystyle A\\{\sigma\\}_{\Theta}$
$\displaystyle:=(*,\vec{A},\vec{B},C:\mathtt{Ty}(\Theta.\vec{B}),\sigma:\Theta.\vec{A}\to\Theta.\vec{B})\mapsto(*,\vec{A},\vec{B},C,\sigma,C\\{\sigma\\})$

Recall that terms of $\widehat{\mathbb{D}}$ are interpreted as sections of
context projections, so $A\\{\sigma\\}$ is a natural transformation from the
interpretation of the context
$\Gamma:=\Phi:\mathsf{Ctx},\,\Psi:\mathsf{Ctx},\,A:\mathtt{Ty}(\Psi),\,\sigma:\texttt{El}\,(\Phi)\to\texttt{El}\,(\Psi)$
to the interpretation of the context $\Gamma,\,B:\mathtt{Ty}(\Phi)$. $\vec{A}$
and $\vec{B}$ interpret $\Phi$ and $\Psi$ respectively because $\mathsf{Ctx}$
is interpreted as a set of telescopes of $\Theta$.

We omit the interpretation of the remaining terms and the verification of the
equations and next turn to the case where $\mathbb{D}$ is a CwF with dependent
product.

#### Domain-level $\Pi$ types

Domain-level $\Pi$ types can be formulated by the following constants: Φ: Ctx,
A : Ty(Φ), B : Ty(Φ.A) ⊢Π(A, B) : Ty(Φ)

Φ: Ctx, M : Tm(Φ.A, B) ⊢Λ(M) : Tm(Φ, Π(A, B))

Φ: Ctx, M : Tm(Φ, Π(A, B)), N : Tm(Φ, A) ⊢App(M, N) : Tm(Φ, B{$\langle
1_{\Phi},N\rangle$}) $\Pi$ types defined here reside in the presheaf category
and model $\Pi$ types in the domain category $\mathbb{D}$. They can be defined
in terms of $\Pi$ types in $\mathbb{D}$ as the types defined above:

$\displaystyle\Pi_{\Psi}:=(*,\vec{A},C:\mathsf{Ty}(\Psi.\vec{A}),D:\mathsf{Ty}(\Psi.\vec{A}.C))\mapsto(*,\vec{A},C:\mathsf{Ty}(\Psi.\vec{A}),D:\mathsf{Ty}(\Psi.\vec{A}.C),\Pi(C,D))$

where $\Pi(C,D)$ is given by the $\Pi$ types in $\mathbb{D}$.

#### Object-level Language

Finally we can define a model for the object-level language defined in the
beginning of Section 6. In this object language, trm is indexed by ty. We
encode the object language as follows: ⋅ ⊢ty : Ty(⊤)

⋅ ⊢ trm : Ty(⊤.ty)

Φ:Ctx ⊢ty’ := ty{!} : Ty(Φ) For convenience, we introduce the abbreviation
$\textsf{ty}^{\prime}$ for $\textsf{ty}\\{!\\}$. We model ty and trm in their
minimal contexts in order to avoid formulating their coherence conditions
w.r.t. substitutions. In the front-end language, we use the applied form
$\texttt{trm}\;a$ to denote a type of terms with type $a$. In the model given
as here, we must apply a substitution instead: Φ: Ctx, a : Tm(Φ, ty’) ⊢ trm
{$\langle!,a\rangle$} : Ty(Φ) That is, in the front-end syntax, we write
$\texttt{trm}~{}a$, which is interpreted as
$\textsf{trm}\\{\langle!,a\rangle\\}$ in the model. We introduce an
abbreviation for later:

$\displaystyle\textsf{trm}[a]:=\textsf{trm}\\{\langle!,a\rangle\\}$

Finally, the constructors of the object language are formulated as follows: Φ:
Ctx ⊢o : Tm(Φ, ty’)

Φ: Ctx ⊢arr : Tm(Φ, ty’) →Tm(Φ, ty’) →Tm(Φ, ty’)

Φ: Ctx ⊢lam : (a, b : Tm(Φ, ty’)) →Tm(Φ. trm[a] , trm[b{p}] ) →Tm(Φ,
trm[arr(a, b)] )

Φ: Ctx ⊢app : (a, b : Tm(Φ, ty’)) →Tm(Φ, trm[arr(a, b)] ) →Tm(Φ, trm[a] )
→Tm(Φ, trm[b] )

#### Category-theoretic perspective

A number of properties of the universe El can be obtained by category-
theoretic considerations. We have explained El as a syntactic representation
of the Yoneda embedding. It has been shown (Capriotti, 2016) that the Yoneda
embedding is a morphism of CwFs, which means that it is a functor preserving
the CwF structure. Using the notation of (Capriotti, 2016, Definition 2.1.4)
this means that there are isomorphisms such as
$\mathrm{y}(\Phi.A)\cong\mathrm{y}(\Phi).\mathrm{y}^{\mathrm{Ty}}(A)$ for the
preservation of context comprehension. The terms and types for the universe El
in the internal type theory that we have defined at the beginning of this
section are a syntactic presentation of this structure.

With this category-theoretic view, it is possible to use existing results on
morphisms of CwFs to obtain information about the universe El . For example,
(Clairambault and Dybjer, 2014, Proposition 4.8) can be used to show that the
Yoneda embedding preserves $\Pi$-types up to isomorphism, because the Yoneda
embedding preserves local cartesian closed structure (Pitts, 1987, Lemma 4.5).
This gives us isomorphisms such as between
$\texttt{El}\,(\Phi)\to\texttt{El}\,(\Phi^{\prime})$ and
$\texttt{El}\,(\Phi\to\Phi^{\prime})$. For instance the direct proof of Lemma
6.3 above can be understood as an instance of this isomorphism.

###  6.4. Interpreting the Domain Level

Given the semantic model, we can detail the interpretation of the dependently
typed Cocon defined in Section 6.1 into this model. The interpretation is a
natural generalization of the simply typed version. First we will consider the
interpretation of the domain-level types and terms, as shown in Fig. 11. One
complication we encountered here is that various judgments are interdependent.
For example, the type well-formedness judgment $\Gamma;\Psi\vdash A\texttt{
type}$ and the term well-formedness judgment $\Gamma;\Psi\vdash M:A$ depend on
each other. As previously discussed, a general fact of the interpretation is
that $\texttt{trm}\;M$ in the syntactic level is interpreted to
$\textsf{trm}[\llbracket M\rrbracket]$.

Interpretation of domain-level types
$\displaystyle\llbracket\Gamma;\Psi\vdash\Pi x:A.B\texttt{ type}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\Pi(\llbracket\Gamma;\Psi\vdash A\texttt{
type}\rrbracket,\llbracket\Gamma;\Psi,x:A\vdash B\texttt{ type}\rrbracket)$
$\displaystyle\llbracket\Gamma;\Psi\vdash\texttt{ty}\texttt{ type}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\textsf{ty}^{\prime}$
$\displaystyle\llbracket\Gamma;\Psi\vdash\texttt{trm}\;M\texttt{
type}\rrbracket$ $\displaystyle\;=\;$
$\displaystyle\textsf{trm}[\llbracket\Gamma;\Psi\vdash
M:\texttt{ty}\rrbracket]$ Interpretation of domain-level contexts
$\displaystyle\llbracket\Gamma\vdash\cdot\texttt{ ctx}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\top$
$\displaystyle\llbracket\Gamma\vdash\Psi,x:A\texttt{ ctx}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\llbracket\Gamma\vdash\Psi\texttt{
ctx}\rrbracket.\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket$
$\displaystyle\llbracket\Gamma\vdash\psi\texttt{ ctx}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\psi$ Interpretation of domain-level
substitutions where $\Psi^{\prime}=\llbracket\Gamma\vdash\Psi\texttt{
ctx}\rrbracket$
$\displaystyle\llbracket\Gamma;\Psi\vdash\cdot:\cdot\rrbracket$
$\displaystyle\;=\;$
$\displaystyle!:\texttt{El}\,(\Psi^{\prime})\to\texttt{El}\,(\top)$ where
$A^{\prime}=\llbracket\Gamma;\Phi\vdash A\texttt{ type}\rrbracket$
$\displaystyle\llbracket\Gamma;\Psi\vdash\sigma,M:\Phi,x:A\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\langle
e_{1},e_{2}\rangle:\texttt{El}\,(\Psi^{\prime})\to\texttt{El}\,(\Phi^{\prime}.A^{\prime})$
where $k=|\overrightarrow{x{:}A}|$
$\displaystyle\llbracket\Gamma;\Psi,\overrightarrow{x:A}\vdash
wk_{\widehat{\Psi}}:\Psi\rrbracket$ $\displaystyle\;=\;$ $\displaystyle
p^{k}:\texttt{El}\,(\llbracket\Gamma\vdash\Psi,\overrightarrow{x:A}\texttt{
ctx}\rrbracket)\to\texttt{El}\,(\Psi^{\prime})$ Interpretation of domain-level
terms where $\Psi^{\prime}=\llbracket\Gamma\vdash\Psi\texttt{ ctx}\rrbracket$
where $\Psi=\Psi_{0},x:A,\overrightarrow{y_{i}:B_{i}}$
$\displaystyle\llbracket\Gamma;\Psi\vdash x:A\rrbracket$ $\displaystyle\;=\;$
$\displaystyle
v\\{p^{k}\\}:\mathsf{Tm}(\Psi^{\prime},A^{\prime}\\{p^{k+1}\\})$ where
$A^{\prime}=\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket$ and
$B^{\prime}=\llbracket\Gamma;\Psi,x:A\vdash B\texttt{ type}\rrbracket$,
$\displaystyle\llbracket\Gamma;\Psi\vdash\lambda x.M:\Pi x:A.B\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\Lambda(e):\mathsf{Tm}(\Psi^{\prime},\Pi(A^{\prime},B^{\prime}))$
where $A^{\prime}=\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket$ and
$B^{\prime}=\llbracket\Gamma;\Psi,x:A\vdash B\texttt{ type}\rrbracket$,
$\displaystyle\llbracket\Gamma;\Psi\vdash M\;N:[N/x]B\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathsf{App}(e_{1},e_{2}):\mathsf{Tm}(\Psi^{\prime},B^{\prime}\\{e_{2}\\})$
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathtt{o}:\texttt{ty}\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathsf{o}:\mathsf{Tm}(\Psi^{\prime},\textsf{ty}^{\prime})$
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathtt{arr}\;a\;b:\texttt{ty}\rrbracket$
$\displaystyle\;=\;$ $\displaystyle\mathtt{arr}({\llbracket\Gamma;\Psi\vdash
a:\texttt{ty}\rrbracket},{\llbracket\Gamma;\Psi\vdash
b:\texttt{ty}\rrbracket}):\mathsf{Tm}(\Psi^{\prime},\textsf{ty}^{\prime})$
where $a^{\prime}=\llbracket\Gamma;\Psi\vdash
a:\texttt{ty}\rrbracket:\mathsf{Tm}(\Psi^{\prime},\textsf{ty}^{\prime})$,
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathsf{lam}\;a\;b\;m:\texttt{trm}\;(\mathsf{arr}\;a\;b)\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathtt{lam}(a^{\prime},b^{\prime},\mathsf{App}(e^{\prime}\\{p\\},v)):\mathsf{Tm}(\Psi^{\prime},\textsf{trm}[arr(a^{\prime},b^{\prime})])$
where $a^{\prime}=\llbracket\Gamma;\Psi\vdash a:\texttt{ty}\rrbracket$ and
$b^{\prime}=\llbracket\Gamma;\Psi\vdash b:\texttt{ty}\rrbracket$,
$\displaystyle\llbracket\Gamma;\Psi\vdash\mathsf{app}\;a\;b\;m\;n:\texttt{trm}\;b\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathtt{app}(a^{\prime},b^{\prime},e_{1},e_{2}):\mathsf{Tm}(\Psi^{\prime},\textsf{trm}[b^{\prime}])$
$\displaystyle\llbracket\Gamma;\Psi\vdash\lfloor
t\rfloor_{\sigma}:[\sigma/\widehat{\Phi}]A\rrbracket$ $\displaystyle\;=\;$
$\displaystyle\texttt{let}~{}\texttt{box}~{}u=e_{1}\ \texttt{in}\
u\\{e_{2}\\}:\mathsf{Tm}(\Psi^{\prime},A^{\prime}\\{e_{2}\\})$ Figure 11.
Interpretation of the domain-level level

In the interpretation, we proceed by interpreting domain-level types,
$\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket$. We interpret ty and
trm to their semantic correspondences. Dependent function types $\Pi$ is
interpreted to semantic $\Pi$ types as defined in the previous subsection. The
interpretation of domain-level contexts $\llbracket\Gamma\vdash\Psi\texttt{
ctx}\rrbracket$ is defined recursively by appending interpreted types to the
end of the semantic context. The empty context $\cdot$ is interpreted to the
terminal object $\top$ and a context variable $\psi$ is interpreted to an
interpreted crisp variable in the interpretation of $\Gamma$, which we will
give later in the interpretation of the computation level.

Domain-level substitutions are interpreted to substitution morphisms by
$\llbracket\Gamma;\Psi\vdash\sigma:\Phi\rrbracket$. The interpretation in this
case is very similar to the simply typed case. We use $!$ for the case of an
empty substitution, $\langle e_{1},e_{2}\rangle$ for an extended substitution,
and iterated first projections $p^{k}$ for weakening substitutions.

Last we interpret domain-level terms using $\llbracket\Gamma;\Psi\vdash
t:A\rrbracket$. In the variable case, given well-typedness, we know that the
domain-level context $\Psi$ must have the form
$\Psi_{0},x:A,\overrightarrow{y_{i}:B_{i}}$. We first use
$v:\mathtt{Tm}(\Psi_{0}.A^{\prime},A^{\prime}\\{p\\})$ to extract $x$ from
$\Psi_{0},x:A$. Then we apply weakening $p^{k}$ to it where $k$ is the length
of the part of context after $x$, which gives us $v\\{p^{k}\\}$. The
abstraction and the application cases are straightforward; they are
interpreted to their semantic terms immediately. Next we interpret the
constructors on the object level. $\mathtt{o}$ and $\mathtt{arr}$ are
interpreted directly to their semantic correspondences.

The $\mathtt{lam}$ case is more interesting, because we need to determine how
HOAS encoding in the domain language corresponds in the semantics. According
to the rule for $\mathsf{lam}$ in the previous subsection, HOAS corresponds to
a semantic term in the set
$\mathtt{Tm}(\Phi^{\prime}.\textsf{trm}[a^{\prime}],\textsf{trm}[b^{\prime}\\{p\\}])$.
Meanwhile, if we directly interpret $m$ as in the rule, we obtain a term
$e^{\prime}$ in the set
$\mathtt{Tm}(\Psi^{\prime},\Pi(\textsf{trm}[a^{\prime}],\textsf{trm}[b^{\prime}\\{p\\}]))$.
Therefore, we need to transform $e^{\prime}$ properly by supplying
$\mathsf{App}(e^{\prime}\\{p\\},v)$. We can examine that this transformation
does achieve the goal:

$\displaystyle\mathsf{App}(e^{\prime}\\{p\\},v)$
$\displaystyle:\mathtt{Tm}(\Psi^{\prime}.\textsf{trm}[a^{\prime}],\textsf{trm}[b^{\prime}\\{p\\}]\\{p\\}\\{\langle
id_{\Psi^{\prime}.\textsf{trm}[a^{\prime}]},v\rangle\\})$
$\displaystyle=\mathtt{Tm}(\Psi^{\prime}.\textsf{trm}[a^{\prime}],\textsf{trm}[b^{\prime}\\{p\\}]\\{p\circ\langle
id_{\Psi^{\prime}.\textsf{trm}[a^{\prime}]},v\rangle\\})$
$\displaystyle=\mathtt{Tm}(\Psi^{\prime}.\textsf{trm}[a^{\prime}],\textsf{trm}[b^{\prime}\\{p\\}])$

The $\mathtt{app}$ case is straightforward. In the unbox case, we first
interpret $t$, from which we obtain a boxed semantic term. We use let box to
extract from it $u$ in $\mathtt{Tm}(\Phi^{\prime},A^{\prime})$. By applying
the interpreted substitution $e_{2}$ to $u$, we obtain a term in the expected
set $\mathtt{Tm}(\Psi^{\prime},A^{\prime}\\{e_{2}\\})$.

###  6.5. Interpreting the Computation Level

Intepretation of computation types $\displaystyle\llbracket\Gamma\vdash\lceil
T\rceil\texttt{ type}\rrbracket$ $\displaystyle\;=\;$
$\displaystyle\flat\llbracket\Gamma\vdash T\rrbracket$
$\displaystyle\llbracket\Gamma\vdash(x:\check{\tau_{1}})\Rightarrow\tau_{2}\texttt{
type}\rrbracket$ $\displaystyle\;=\;$
$\displaystyle(x::\llbracket{\Gamma\vdash\check{\tau}_{1}\texttt{
type}}\rrbracket)\to^{\flat}{\llbracket\Gamma,x:\breve{\tau}_{1}\vdash\tau_{2}\texttt{
type}\rrbracket}$ $\displaystyle\llbracket\Gamma\vdash\texttt{ctx}\texttt{
type}\rrbracket$ $\displaystyle\;=\;$ $\displaystyle\mathsf{Ctx}$
Interpretation of computation contexts
$\displaystyle\llbracket\cdot\rrbracket$ $\displaystyle\;=\;$
$\displaystyle\cdot$ $\displaystyle\llbracket\Gamma,x:\check{\tau}\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\llbracket\Gamma\rrbracket,x::\llbracket\Gamma\vdash\breve{\tau}\texttt{
type}\rrbracket$ Interpretation of contextual objects
$\displaystyle\llbracket\Gamma\vdash(\widehat{\Psi}\vdash M):(\Psi\vdash
A)\rrbracket$ $\displaystyle\;=\;$ $\displaystyle\llbracket\Gamma;\Psi\vdash
M:A\rrbracket$ $\displaystyle\llbracket\Gamma\vdash(\widehat{\Psi}\vdash
M):(\Psi\vdash_{v}A)\rrbracket$ $\displaystyle\;=\;$
$\displaystyle\llbracket\Gamma;\Psi\vdash M:A\rrbracket$ Interpretation of
contextual types $\displaystyle\llbracket\Gamma\vdash(\Psi\vdash A)\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathsf{Tm}(\llbracket\Gamma\vdash\Psi\texttt{
ctx}\rrbracket,\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket)$
$\mathsf{Tm}_{v}$ is $\mathsf{Tm}$ but equivalent to $v\\{p^{k}\\}$
$\displaystyle\llbracket\Gamma\vdash(\Psi\vdash_{v}A)\rrbracket$
$\displaystyle\;=\;$
$\displaystyle\mathsf{Tm}_{v}(\llbracket\Gamma\vdash\Psi\texttt{
ctx}\rrbracket,\llbracket\Gamma;\Psi\vdash A\texttt{ type}\rrbracket)$