Type-Theoretic Signatures for Algebraic Theories and Inductive Types

András Kovács

Submitted in fulfillment of the requirements for the degree of Doctor of
Philosophy

Eötvös Loránd University
Doctoral School of Informatics
March 2022
DOI: 10.15476/ELTE.2022.070

## Acknowledgements

I would like to thank my supervisor Ambrus Kaposi for his support and the
remarkably low-stress experience throughout my studies, and also for the
research collaboration which provided ample content for this thesis. Many
thanks to Tamás Kozsik for being a likewise supportive supervisor in my first
year of studies, and to Zoltán Horváth for doing a great job providing
financial and administrative support, and I also want to thank the secretaries
at department and at the faculty.

I would like to thank my opponents Fredrik Forsberg and Christian Sattler for
their careful reading and comments on my thesis.

I would like to thank attendees of the Budapest type theory seminar for the
many discussions over the years, in particular Balázs Kőműves, Péter
Diviánszky, Gábor Lehel, Gergő Érdi and my fellow PhD students Rafaël Bocquet
and István Donkó.

I would like to thank everyone in the research community who educated and
inspired me through various discussions and interactions. I would like to
express special thanks to my coauthors Thorsten Altenkirch, Nicolai Kraus and
Ambroise Lafont.

Finally, I would like to thank my parents for their love and support.

###### Contents

  1. 1 Introduction
    1. 1.1 Overview
    2. 1.2 How to Read This Thesis
    3. 1.3 Formalization
    4. 1.4 Notation and Conventions
  2. 2 Simple Signatures
    1. 2.1 Theory of Signatures
    2. 2.2 Semantics
      1. 2.2.1 Algebras
      2. 2.2.2 Morphisms
      3. 2.2.3 Displayed Algebras
      4. 2.2.4 Sections
    3. 2.3 Term Algebras
      1. 2.3.1 Recursor Construction
      2. 2.3.2 Eliminator Construction
    4. 2.4 Comparison to Endofunctors as Signatures
  3. 3 Semantics in Two-Level Type Theory
    1. 3.1 Motivation
    2. 3.2 Models of Type Theories
      1. 3.2.1 The Algebraic View
      2. 3.2.2 Categories With Families
      3. 3.2.3 Type formers
    3. 3.3 Two-Level Type Theory
      1. 3.3.1 Models
      2. 3.3.2 Internal Syntax and Notation
      3. 3.3.3 Alternative Presentation for 2LTT
    4. 3.4 Presheaf Semantics of 2LTT
      1. 3.4.1 Presheaf Model of the Outer Layer
      2. 3.4.2 Modeling the Inner Layer
      3. 3.4.3 Functions With Inner Domains
    5. 3.5 Simple Signatures in 2LTT
      1. 3.5.1 Theory of Signatures
      2. 3.5.2 Algebras
      3. 3.5.3 Morphisms
      4. 3.5.4 Displayed Algebras
      5. 3.5.5 Sections
      6. 3.5.6 Term Algebras
      7. 3.5.7 Recursor Construction
      8. 3.5.8 Eliminator Construction
      9. 3.5.9 Strict Elimination
  4. 4 Finitary QII Signatures
    1. 4.1 Theory of Signatures
    2. 4.2 Semantics
      1. 4.2.1 Overview
      2. 4.2.2 Separate vs. Bundled Models
      3. 4.2.3 Finite Limit Cwfs
      4. 4.2.4 The Cwf of Finite Limit Cwfs
      5. 4.2.5 Type Formers
      6. 4.2.6 Recovering AMDS Interpretations
      7. 4.2.7 Left Adjoints of Substitutions
    3. 4.3 Discussion of Semantics
      1. 4.3.1 Flcwfs For Free
      2. 4.3.2 Variations of the Semantics
      3. 4.3.3 Substitutions
      4. 4.3.4 Using Signatures in Implementations
    4. 4.4 Term Algebras
      1. 4.4.1 Universes & Metatheory
      2. 4.4.2 Signatures & Semantics
      3. 4.4.3 Term Algebra Construction
      4. 4.4.4 Recursor Construction
      5. 4.4.5 Eliminator Construction
    5. 4.5 Levitation and Bootstrapping for Closed Signatures
      1. 4.5.1 Models & Signatures
    6. 4.6 Reductions to Basic Type Formers
      1. 4.6.1 Finitary QIIT Constructions
      2. 4.6.2 Reduction of Finitary Inductive-Inductive Types
      3. 4.6.3 Reduction of Closed QIITs
    7. 4.7 Related Work
  5. 5 Infinitary QII Signatures
    1. 5.1 Theory of Signatures
    2. 5.2 Semantics
      1. 5.2.1 Overview
      2. 5.2.2 Model of the Theory of Signatures
    3. 5.3 Left Adjoints of Substitutions
    4. 5.4 Signature-Based Semantics of Signatures
    5. 5.5 Discussion of Semantics
    6. 5.6 Term Algebras
      1. 5.6.1 Term Algebra Construction
      2. 5.6.2 Eliminator Construction
    7. 5.7 Levitation and Bootstrapping
    8. 5.8 Related Work
  6. 6 Higher Inductive-Inductive Signatures
    1. 6.1 Strict Signatures
      1. 6.1.1 Semantics
    2. 6.2 Weak Signatures
      1. 6.2.1 Semantics
    3. 6.3 Discussion & Related Work
      1. 6.3.1 Evaluation
      2. 6.3.2 Related Work
  7. A AMDS interpretation of FQII signatures
  8. B AMDS interpretation of strict HII signatures

## CHAPTER 1 Introduction

This thesis develops the usage of certain type theories as specification
languages for algebraic theories and inductive types.

_Type theories_ have emerged as popular metatheoretic settings for mechanized
mathematics. One reason is that the field of type theory is generally aware of
the issue of overheads in representation, and it is a common endeavor to
search for concise “synthetic” ways to talk about different areas of
mathematics. In type theory, it is a virtue to be able to directly say what we
mean, and in a way such that simple-minded computers are able to verify it.

_Algebraic theories_ are certain mathematical structures which are especially
well-behaved, and which are ubiquitous in mathematics, such as groups or
categories. In type theories, _inductive types_ are certain freely generated
(initial) models of algebraic theories. Inductive types are a core feature in
implementations of type theories, widely used in mathematical formalization,
but also as the primary way to define the data structures which are used in
programming.

This thesis observes that if we are to specify more complicated algebraic
theories, dependent type theories provide the natural tool to manage
complexities. The expressive power of type theory which makes it suitable as a
foundation for mechanized mathematics, also proves useful for the more
specialized task of specifying algebraic signatures.

There is a trade-off between the complexity of a mathematical language and the
ease of usage of the language. Minimal languages are convenient to reason
about and develop metatheory for, but they often require an excessive amount
of boilerplate to work in. However, it is a worthwhile effort to try to move
towards the Pareto frontier of this trade-off. We believe that the current
thesis makes progress in this respect.

Our signatures are useful in broader mathematical contexts, but we are also
concerned with potential implementation in proof assistants. Although it is
unlikely that our signatures can be deployed in practice exactly as they are,
they should be still helpful as formal bases of practical implementations.

###  1.1 Overview

In Chapter 2, we present a minimal example of a type theory of signatures.
This allows specifying single-sorted signatures without equations. The purpose
of the chapter is didactic. We develop just enough semantics to get notions of
initiality and induction for algebras. We also present a _term algebra
construction_ : this shows that the initial algebra for each signature can be
constructed from the syntax of signatures itself.

In Chapter 3 we describe a metatheoretic setting which is often used in the
thesis. This is _two-level type theory_ [ACKS19]. It allows us to develop
general semantics for signatures, while still working inside a convenient type
theory. As a demonstration, we generalize the semantics from Chapter 2 so that
it is given internally to arbitrary categories-with-families. As a special
case, signatures can be interpreted in arbitrary categories with finite
products.

In Chapter 4 we describe finitary quotient inductive-inductive signatures.
These are close to generalized algebraic theories [Car86] in expressive power.
In particular, most type theories themselves can be specified with finitary
quotient inductive-inductive signatures. We significantly expand the semantics
of signatures, now for each signature we provide a category of algebras with
certain extra structure, which is equivalent to having finite limits. This
allows us to prove for each signature the equivalence of initiality and
induction. Also, owing to two-level type theory, signatures can be interpreted
internally to any category with finite limits. Additionally

  * •

We present a term algebra construction.

  * •

We show that morphisms of signatures are interpreted as right adjoint functors
in the semantics.

  * •

We present how self-description of signatures can be exploited to minimize
metatheoretic assumptions.

  * •

For certain fragments of the theory of signatures, we describe ways to
construct initial algebras from simpler type formers.

In Chapter 5, we describe infinitary quotient inductive-inductive signatures.
These allow specification of infinitely branching trees (as initial algebras).
We adapt the semantics from the previous chapter. We also revisit term models,
left adjoints of signature morphisms and self-description of signatures. Self-
description in particular is significantly strengthened, since the full
theories of signatures in Chapters 4-5 can be now described using infinitary
quotient inductive-inductive signatures. We also describe how to build
semantics of signatures internally to the theory of signatures itself. For
example, this means that for each signature, algebra morphisms are also
specified with a signature. The full semantics can be internalized in the
theory of signatures in this manner; this is useful for building new
signatures in a generic way.

In Chapter 6, we describe higher inductive-inductive signatures. These differ
from the previous signatures mostly in their intended semantics, whose context
is now homotopy type theory [Uni13], and which allows specified equalities to
be proof-relevant. The higher-dimensional generalization of types and
equalities makes semantics more complicated, so we only present enough
semantics to specify notions of initiality and induction for each signature.
Additionally, we consider two different notions of algebra morphisms: one
preserves structure strictly (up to definitional equality), while the other
preserves structure up to paths.

###  1.2 How to Read This Thesis

We list several general references which could be helpful for readers.

  * •

It is useful to have some user experience with a type-theory-based proof
assistant or programming language, such as Agda, Coq, Lean or Idris. In the
author’s view, mechanized formalization is the most effective way to build
intuition about working in type theories.

  * •

We often use categories-with-families [CCD19, Hof97, Dyb95] throughout the
thesis.

  * •

We use a modest amount of category theory, for which [Awo10] should be a
sufficient reference.

  * •

For Chapter 6, the Homotopy Type Theory book [Uni13] provides context and
motivation.

This thesis is mostly written in a linear fashion, as later chapters often
revisit or generalize earlier concepts. There are some breaks from linearity
though, so we summarize dependencies between chapters as follows:

  * •

Chapter 3 depends on Chapter 2.

  * •

All chapters after Chapter 3 depend on it.

  * •

Chapter 5 depends on Chapter 4 as it revisits most constructions from there.

  * •

Chapter 6 only depends on Chapter 3.

###  1.3 Formalization

Chapter 2 is fully formalized in Agda, and the semantics of weak signatures in
Chapter 6 is mostly formalized, with some omissions and shortcuts. The
formalization can be found in [Kov22b].

###  1.4 Notation and Conventions

Throughout this thesis, we always work in some sort of type theory, although
the exact flavor of the type theory will vary. We summarize here the notations
and conventions that will stay consistent. Our style of notation is a mostly a
mix of the homotopy type theory book [Uni13] and the syntax of the proof
assistant Agda.

#####  $\Sigma$-types

We write a dependent pair type as $(a:A)\times B$, where $B$ may refer to $a$.
Pairing is $(t,\,u)$, and projections are $\mathsf{proj}_{1}$ and
$\mathsf{proj}_{2}$. Iterated $\Sigma$-types can written as
$(a:A)\times(b:B)\times C$, for example. We often silently re-associate left-
nested $\Sigma$-types to the right, e.g. write $(a:A)\times(b:B)\times C$
instead of $(\mathit{ab}:(a:A)\times B)\times C$.

Field projection notation: we reuse binder names in $\Sigma$-types as field
projections. For example, if we have $t:(\mathsf{foo}:A)\times B$, then
$\mathsf{foo}_{t}$ projects the first component from $t$. To make this a bit
more convenient, we also allow to name the last components, for example if
$t:(\mathsf{foo}:A)\times(\mathsf{bar}:B)$, then we have $\mathsf{foo}_{t}:A$,
and $\mathsf{bar}_{t}:B[\mathsf{foo}\mapsto\mathsf{foo}_{t}]$. This notation
is useful when we handle components of more complicated algebraic structures.

##### Unit type

Whenever the unit type is available, we name it $\top$, and its inhabitant
$\mathsf{tt}$.

#####  $\Pi$-types

Dependent function types are written as $(a:A)\to B$, where $B$ may depend on
the $a$ variable. It is possible to group multiple binders with the same type,
as in $(x\,y:A)\to B$. For non-dependent function types, we write plainly
$A\to B$. Functions are defined as $\lambda\,x.\,t$. We may group multiple
binders, as in $\lambda\,x\,y\,z.\,t$, and optionally add type annotation to
binders, as in $\lambda\,(x:A).\,t$.

We also use Agda-like implicit arguments: a function type $\\{a:A\\}\to B$
signals that we usually omit the argument in function applications. For
example, if $\mathsf{id}:\\{A:\mathsf{Set}\\}\to A\to A$, we write
$\mathsf{id}\,\mathsf{true}:\mathsf{Bool}$. We can still make these arguments
explicit, by using bracketed application, as in
$\mathsf{id}\,\\{\mathsf{Bool}\\}\,\mathsf{true}$. Similarly, we may use
bracketed $\lambda$, as in $\lambda\,\\{A:\mathsf{Set}\\}\,(x:A).\,x$, to bind
implicit arguments.

Sometimes we also write pattern matching abstraction, as in
$\lambda\,(x,\,y).\,t$ for a function with a $\Sigma$ domain.

We may use implicit quantification as well: argument binders and types may be
entirely omitted when it is clear where they are quantified. This resembles
the implicit generalization in the Haskell or Idris programming languages. For
example, the $A$ and $B$ types are implicitly quantified below:

$\displaystyle\mathsf{map}:(A\to B)\to\mathsf{List}\,A\to\mathsf{List}\,B$
$\displaystyle\mathsf{map}:\equiv...$

##### Identity types

We use $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\\!\equiv\\!\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!=\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ to denote identity
types. We always use $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\equiv\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ as a “strict”
equality which satisfies uniqueness of identity proofs. Reflexivity of
identity is always written as $\mathsf{refl}$. We use $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\\!=\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$
as intensional identity in Chapter 2. In later chapters, $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\\!=\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$
denotes the identity type in the inner layer of a two-level type theory, and
$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\\!\equiv\\!\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}$ denotes the outer identity type.

##### Definitions

We give definitions using $:\equiv$, for example as in

$\displaystyle\mathsf{id}:\\{A:\mathsf{Set}\\}\to A\to A$
$\displaystyle\mathsf{id}\,a:\equiv a$

Note that we write the function argument on the left of $:\equiv$, instead of
writing a $\lambda$ on the right. We may switch between the two styles. The
type signature can be omitted in a definition. We may also use pattern
matching, like in $\mathsf{foo}\,(x,\,y):\equiv...$.

## CHAPTER 2 Simple Signatures

In this chapter, we take a look at a very simple notion of algebraic
signature. The motivation for doing so is to present the basic ideas of this
thesis in the easiest possible setting, with explicit definitions. The later
chapters are greatly generalized and expanded compared to the current one, and
are not feasible (and probably not that useful) to present in full formal
detail. We also include a complete Agda formalization of the contents of this
chapter, in around 250 lines.

The mantra throughout this dissertation is the following: algebraic theories
are specified by typing contexts in certain _theories of signatures_. For each
class of algebraic theories, there is a corresponding theory of signatures,
which is viewed as a proper type theory and comes equipped with a model
theory. _Semantics_ of signatures is given by interpreting them in certain
models of the theory of signatures. Semantics should at least provide a notion
of induction principle for each signature; in this chapter we provide a bit
more than that, and we will do substantially more in Chapters 4 and 5.

##### Metatheory

We work in an intensional type theory which supports $\Pi$, $\Sigma$, $\top$,
intensional identity $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!=\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$, inductive families,
and two universes $\mathsf{Set}$ and $\mathsf{Set}_{1}$ closed under the
mentioned type formers, with $\mathsf{Set}:\mathsf{Set}_{1}$. Since the
contents of this chapter are formalized in Agda, and our notation is
reminiscent of Agda too, we can think of the metatheory as a subset of Agda.

###  2.1 Theory of Signatures

Generally, more expressive theories of signatures can describe larger classes
of theories. As we are aiming for minimalism right now, the current theory of
signatures is as follows:

######  Definition 1.

The theory of signatures, or ToS for short, is a simple type theory equipped
with the following features:

  * •

An empty base type $\iota$.

  * •

A _first-order function type_ $\iota\\!\to\\!\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}$; this is a function whose domain is fixed to be
$\iota$. Moreover, first-order functions only have neutral terms: there is
application, but no $\lambda$-abstraction.

We can specify the full syntax using the following Agda-like inductive
definitions.

$\displaystyle\mathsf{Ty}$ $\displaystyle:\mathsf{Set}$
$\displaystyle\mathsf{Var}$
$\displaystyle:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{Set}$ $\displaystyle\iota$
$\displaystyle:\mathsf{Ty}$ $\displaystyle\mathsf{vz}$
$\displaystyle:\mathsf{Var}\,(\Gamma\triangleright A)\,A$
$\displaystyle\iota\\!\to\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$
$\displaystyle:\mathsf{Ty}\to\mathsf{Ty}$ $\displaystyle\mathsf{vs}$
$\displaystyle:\mathsf{Var}\,\Gamma\,A\to\mathsf{Var}\,(\Gamma\triangleright
B)\,A$ $\displaystyle\mathsf{Con}$ $\displaystyle:\mathsf{Set}$
$\displaystyle\mathsf{Tm}$
$\displaystyle:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{Set}$
$\displaystyle\scaleobj{.75}\bullet$ $\displaystyle:\mathsf{Con}$
$\displaystyle\mathsf{var}$
$\displaystyle:\mathsf{Var}\,\Gamma\,A\to\mathsf{Tm}\,\Gamma\,A$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\triangleright\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$
$\displaystyle:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{Con}\hskip 20.00003pt$
$\displaystyle\mathsf{app}$ $\displaystyle:\mathsf{Tm}\,\Gamma\,(\iota\to
A)\to\mathsf{Tm}\,\Gamma\,\iota\to\mathsf{Tm}\,\Gamma\,A$

Here, $\mathsf{Con}$ contexts are lists of types, and $\mathsf{Var}$ specifies
well-typed De Bruijn indices, where $\mathsf{vz}$ represents the zero index,
and $\mathsf{vs}$ takes the successor of an index.

######  Notation 1.

We use capital Greek letters starting from $\Gamma$ to refer to contexts, $A$,
$B$, $C$ to refer to types, and $t$, $u$, $v$ to refer to terms. In examples,
we may use a nameful notation instead of De Bruijn indices. For example, we
may write
$x:\mathsf{Tm}\,(\scaleobj{.75}\bullet\triangleright(x:\iota)\triangleright(y:\iota))\,\iota$
instead of
$\mathsf{var}\,(\mathsf{vs}\,\mathsf{vz}):\mathsf{Tm}\,(\scaleobj{.75}\bullet\triangleright\iota\triangleright\iota)\,\iota$.
Additionally, we may write $t\,u$ instead of $\mathsf{app}\,t\,u$ for $t$ and
$u$ terms.

######  Definition 2.

Parallel substitutions map variables to terms.

$\displaystyle\mathsf{Sub}:\mathsf{Con}\to\mathsf{Con}\to\mathsf{Set}$
$\displaystyle\mathsf{Sub}\,\Gamma\,\Delta\equiv\\{A:\mathsf{Ty}\\}\to\mathsf{Var}\,\Delta\,A\to\mathsf{Tm}\,\Gamma\,A$

We use $\sigma$ and $\delta$ to refer to substitutions. We also recursively
define the action of substitution on terms:

$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}]:\mathsf{Tm}\,\Delta\,A\to\mathsf{Sub}\,\Gamma\,\Delta\to\mathsf{Tm}\,\Gamma\,A$
$\displaystyle(\mathsf{var}\,x)$ $\displaystyle[\sigma]:\equiv\sigma\,x$
$\displaystyle(\mathsf{app}\,t\,u)$
$\displaystyle[\sigma]:\equiv\mathsf{app}\,(t[\sigma])\,(u[\sigma])$

The identity substitution $\mathsf{id}$ is defined simply as $\mathsf{var}$.
It is easy to see that $t[\mathsf{id}]=t$ for all $t$. Substitution
composition is as follows.

$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\circ\\!\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}:\mathsf{Sub}\,\Delta\,\Xi\to\mathsf{Sub}\,\Gamma\,\Delta\to\mathsf{Sub}\,\Gamma\,\Xi$
$\displaystyle(\sigma\circ\delta)\,x:\equiv(\sigma\,x)[\delta]$

######  Example 1.

We may write signatures for natural numbers and binary trees respectively as
follows.

$\displaystyle\mathsf{NatSig}$
$\displaystyle:\equiv\scaleobj{.75}\bullet\triangleright(\mathit{zero}:\iota)\triangleright(\mathit{suc}:\iota\to\iota)$
$\displaystyle\mathsf{TreeSig}$
$\displaystyle:\equiv\scaleobj{.75}\bullet\triangleright(\mathit{leaf}:\iota)\triangleright(\mathit{node}:\iota\to\iota\to\iota)$

In short, the current ToS allows signatures which are

  * •

_Single-sorted_ : this means that we have a single type constructor,
corresponding to $\iota$.

  * •

_Closed_ : signatures cannot refer to any externally existing type. For
example, we cannot write a signature for lists of natural numbers in a direct
fashion, since there is no way to refer to the type of natural numbers.

  * •

_Finitary_ : inductive types corresponding to signatures are always finitely
branching trees.

_Remark._ We omit $\lambda$-expressions from the ToS for the sake of
simplicity: this causes terms to be always in normal form (neutral, to be
precise), and thus we can skip talking about conversion rules. Later, starting
from Chapter 4 we include proper $\beta\eta$-rules in theories of signatures.

###  2.2 Semantics

For each signature, we need to know what it means for a type theory to support
the corresponding inductive type. For this, we need at least a notion of
_algebras_ , which can be viewed as a bundle of all type and value
constructors, and what it means for an algebra to support an _induction
principle_. Additionally, we may want to know what it means to support a
_recursion principle_ , which can be viewed as a non-dependent variant of
induction. In the following, we define these notions by induction on ToS
syntax.

_Remark._ We use “algebra” and “model” synonymously throughout this thesis.

####  2.2.1 Algebras

First, we calculate types of algebras. This is simply a standard
interpretation into the $\mathsf{Set}$ universe. We define the following
operations by induction; the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$
name is overloaded for $\mathsf{Con}$, $\mathsf{Ty}$ and $\mathsf{Tm}$.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}:\mathsf{Ty}\to\mathsf{Set}\to\mathsf{Set}$
$\displaystyle\iota^{A}\,$ $\displaystyle X:\equiv X$ $\displaystyle(\iota\to
A)^{A}\,$ $\displaystyle X:\equiv X\to A^{A}\,X$ $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}^{A}:\mathsf{Con}\to\mathsf{Set}\to\mathsf{Set}$
$\Gamma^{A}\,X:\equiv\\{A:\mathsf{Ty}\\}\to\mathsf{Var}\,\Gamma\,A\to
A^{A}\,X$ $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}:\mathsf{Tm}\,\Gamma\,A\to\\{X:\mathsf{Set}\\}\to\Gamma^{A}\,X\to
A^{A}\,X$ $\displaystyle(\mathsf{var}\,x)^{A}\,$
$\displaystyle\gamma:\equiv\gamma\,x$
$\displaystyle(\mathsf{app}\,t\,u)^{A}\,$ $\displaystyle\gamma:\equiv
t^{A}\,\gamma\,(u^{A}\,\gamma)$ $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}:\mathsf{Sub}\,\Gamma\,\Delta\to\\{X:\mathsf{Set}\\}\to\Gamma^{A}\,X\to\Delta^{A}\,X$
$\sigma^{A}\,\gamma\,x:\equiv(\sigma\,x)^{A}\,\gamma$

Here, types and contexts depend on some $X:\mathsf{Set}$, which serves as the
interpretation of $\iota$. We define $\Gamma^{A}$ as a product: for each
variable in the context, we get a semantic type. This trick, along with the
definition of $\mathsf{Sub}$, makes formalization a bit more compact. Terms
and substitutions are interpreted as natural maps. Substitutions are
interpreted by pointwise interpreting the contained terms.

######  Notation 2.

We may write values of $\Gamma^{A}$ using notation for $\Sigma$-types. For
example, we may write $(\mathit{zero}:X)\times(\mathit{suc}:X\to X)$ for the
result of computing $\mathsf{NatSig}^{A}\,X$.

######  Definition 3.

We define algebras as follows.

$\displaystyle\mathsf{Alg}:\mathsf{Con}\to\mathsf{Set}_{1}$
$\displaystyle\mathsf{Alg}\,\Gamma:\equiv(X:\mathsf{Set})\times\Gamma^{A}\,X$

######  Example 2.

$\mathsf{Alg}\,\mathsf{NatSig}$ is computed to
$(X:\mathsf{Set})\times(\mathit{zero}:X)\times(\mathit{suc}:X\to X)$.

####  2.2.2 Morphisms

Now, we compute notions of morphisms of algebras. In this case, morphisms are
functions between underlying sets which preserve all specified structure. The
interpretation for calculating morphisms is a _logical relation
interpretation_ [HRR14] over the $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}$ interpretation. The key part is the interpretation of types:

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{M}:(A:\mathsf{Ty})\\{X_{0}\,X_{1}:\mathsf{Set}\\}(X^{M}:X_{0}\to
X_{1})\to A^{A}\,X_{0}\to A^{A}\,X_{1}\to\mathsf{Set}$
$\displaystyle\iota^{M}\,$ $\displaystyle
X^{M}\,\alpha_{0}\,\,\alpha_{1}:\equiv X^{M}\,\alpha_{0}=\alpha_{1}$
$\displaystyle(\iota\to A)^{M}\,$ $\displaystyle
X^{M}\,\alpha_{0}\,\,\alpha_{1}:\equiv(x:X_{0})\to
A^{M}\,X^{M}\,(\alpha_{0}\,x)\,(\alpha_{1}\,(X^{M}\,x))$

We again assume an interpretation for the base type $\iota$, as $X_{0}$,
$X_{1}$ and $X^{M}:X_{0}\to X_{1}$. $X^{M}$ is function between underlying
sets of algebras, and $A^{M}$ computes what it means that $X^{M}$ preserves an
operation with type $A$. At the base type, preservation is simply equality. At
the first-order function type, preservation is a quantified statement over
$X_{0}$. We define morphisms for $\mathsf{Con}$ pointwise:

$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{M}:(\Gamma:\mathsf{Con})\\{X_{0}\,X_{1}:\mathsf{Set}\\}\to(X_{0}\to
X_{1})\to\Gamma^{A}\,X_{0}\to\Gamma^{A}\,X_{1}\to\mathsf{Set}$
$\displaystyle\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}:\equiv\\{A:\mathsf{Ty}\\}(x:\mathsf{Var}\,\Gamma\,A)\to
A^{M}\,X^{M}\,(\gamma_{0}\,x)\,(\gamma_{1}\,x)$

For terms and substitutions, we get preservation statements, which are
sometimes called _fundamental lemmas_ in discussions of logical relations
[HRR14].

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{M}:(t:\mathsf{Tm}\,\Gamma\,A)\to\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}\to
A^{M}\,X^{M}\,(t^{A}\,\gamma_{0})\,(t^{A}\,\gamma_{1})$
$\displaystyle(\mathsf{var}\,x)^{M}$
$\displaystyle\gamma^{M}:\equiv\gamma^{M}\,x$
$\displaystyle(\mathsf{app}\,t\,u)^{M}$ $\displaystyle\gamma^{M}:\equiv
t^{M}\,\gamma^{M}\,(u^{A}\,\gamma_{0})$ $\displaystyle\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}^{M}:(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\to\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}\to\Delta^{M}\,X^{M}\,(\sigma^{A}\,\gamma_{0})\,(\sigma^{A}\,\gamma_{1})$
$\displaystyle\sigma^{M}\,\gamma^{M}\,x:\equiv(\sigma\,x)^{M}\,\gamma^{M}$

The definition of $(\mathsf{app}\,t\,u)^{M}$ is well-typed by the induction
hypothesis $u^{M}\,\gamma^{M}:X^{M}\,(u^{A}\,\gamma_{0})=u^{A}\,\gamma_{1}$.

######  Definition 4.

To get notions of algebra morphisms, we again pack up $\Gamma^{M}$ with the
interpretation of $\iota$.

$\displaystyle\mathsf{Mor}:\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Alg}\,\Gamma\to\mathsf{Alg}\,\Gamma\to\mathsf{Set}$
$\displaystyle\mathsf{Mor}\,\\{\Gamma\\}\,(X_{0},\,\gamma_{0})\,(X_{1},\,\gamma_{1}):\equiv(X^{M}:X_{0}\to
X_{1})\times\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}$

######  Example 3.

We have the following computation:

$\mathsf{Mor}\,\\{\mathsf{NatSig}\\}\,(X_{0},\,\mathit{zero_{0}},\,\mathit{suc_{0}})\,(X_{1},\,\mathit{zero_{1}},\,\mathit{suc_{1}}):\equiv$
$\displaystyle(X^{M}:X_{0}\to X_{1})$ $\displaystyle\times\,$
$\displaystyle(X^{M}\,\mathit{zero_{0}}=\mathit{zero_{1}})$
$\displaystyle\times\,$ $\displaystyle((x:X_{0})\to
X^{M}\,(\mathit{suc_{0}}\,x)=\mathit{suc_{1}}\,(X^{M}\,x))$

######  Definition 5.

We state initiality as a predicate on algebras:

$\displaystyle\mathsf{Initial}:\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Alg}\,\Gamma\to\mathsf{Set}$
$\displaystyle\mathsf{Initial}\,\\{\Gamma\\}\,\gamma:\equiv(\gamma^{\prime}:\mathsf{Alg}\,\Gamma)\to\mathsf{isContr}\,(\mathsf{Mor}\,\gamma\,\gamma^{\prime})$

Here $\mathsf{isContr}$ refers to unique existence [Uni13, Section 3.11]. If
we drop $\mathsf{isContr}$ from the definition, we get the notion of weak
initiality, which corresponds to the recursion principle for $\Gamma$.
Although we call this predicate $\mathsf{Initial}$, in this chapter we do not
yet show that algebras form a category. We will show this in a more general
setting in Chapter 4.

###### Morphisms vs. logical relations.

The $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{M}$ interpretation can be
viewed as a special case of logical relations over the $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}^{A}$ model: every morphism is a _functional_
logical relation, where the chosen relation between the underlying sets
happens to be a function. Consider now a more general relational
interpretation for types:

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{R}:(A:\mathsf{Ty})\\{X_{0}\,X_{1}:\mathsf{Set}\\}(X^{R}:X_{0}\to
X_{1}\to\mathsf{Set})\to A^{A}\,X_{0}\to A^{A}\,X_{1}\to\mathsf{Set}$
$\displaystyle\iota^{R}\,$ $\displaystyle
X^{R}\,\alpha_{0}\,\,\alpha_{1}:\equiv X^{R}\,\alpha_{0}\,\alpha_{1}$
$\displaystyle(\iota\to A)^{R}\,$ $\displaystyle
X^{R}\,\alpha_{0}\,\,\alpha_{1}:\equiv(x_{0}:X_{0})(x_{1}:X_{1})\to
X^{R}\,x_{0}\,x_{1}\to A^{R}\,X^{R}\,(\alpha_{0}\,x_{0})\,(\alpha_{1}\,x_{1})$

Here, functions are related if they map related inputs to related outputs. If
we know that $X^{M}\,\alpha_{0}\,\alpha_{1}\equiv(f\,\alpha_{0}=\alpha_{1})$
for some function $f$, we get

$(x_{0}:X_{0})(x_{1}:X_{1})\to f\,x_{0}=x_{1}\to
A^{R}\,X^{R}\,(\alpha_{0}\,x_{0})\,(\alpha_{1}\,x_{1})$

Now, we can simply substitute along the input equality proof in the above
type, to get the previous definition for $(\iota\to A)^{M}$:

$(x_{0}:X_{0})\to A^{R}\,X^{R}\,(\alpha_{0}\,x_{0})\,(\alpha_{1}\,(f\,x_{0}))$

This substitution along the equation is called “singleton contraction” in the
jargon of homotopy type theory [Uni13]. The ability to perform contraction
here is at the heart of the _strict positivity restriction_ for inductive
signatures. Strict positivity in our setting corresponds to only having first-
order function types in signatures. If we allowed function domains to be
arbitrary types, in the definition of $(A\to B)^{M}$ we would only have a
black-box $A^{M}\,X^{M}:A^{A}\,X_{0}\to A^{A}\,X_{1}\to\mathsf{Set}$ relation,
which is not known to be given as an equality.

In Chapter 4 we expand on this. As a preliminary summary: although higher-
order functions have relational interpretation, such relations do not
generally compose. What we eventually aim to have is a category of algebras
and algebra morphisms, where morphisms do compose. We need a _directed_ model
of the theory of signatures, where every signature becomes a category of
algebras. The way to achieve this is to prohibit higher-order functions,
thereby avoiding the polarity issues that prevent a directed interpretation
for general function types.

####  2.2.3 Displayed Algebras

At this point we do not yet have specification for induction principles. We
use the term _displayed algebra_ to refer to “dependent” algebras, where every
displayed algebra component lies over corresponding components in the base
algebra. For the purpose of specifying induction, displayed algebras can be
viewed as bundles of induction motives and methods.

Displayed algebras over some $\gamma:\mathsf{Alg}\,\Gamma$ are equivalent to
slices over $\gamma$ in the category of $\Gamma$-algebras; we will show this
in Chapter 4. A slice $f:\Gamma^{M}\,\gamma^{\prime}\,\gamma$ maps elements of
$\gamma^{\prime}$’s underlying set to elements in the base algebra. Why do we
need displayed algebras, then? The main reason is that if we are to eventually
implement inductive types in a programming language or proof assistant, we
need to compute induction principles exactly, not merely up to isomorphisms.

For more illustration of using displayed algebras in a type-theoretic setting,
see [AL19]. We adapt the term “displayed algebra” from ibid. as a
generalization of displayed categories (and functors, natural transformations)
to other algebraic structures.

The displayed algebra interpretation is a _logical predicate_ interpretation,
defined as follows.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{D}:(A:\mathsf{Ty})\\{X\\}\to(X\to\mathsf{Set})\to
A^{A}\,X\to\mathsf{Set}$ $\displaystyle\iota^{D}\,$ $\displaystyle
X^{D}\,\alpha:\equiv X^{D}\,\alpha$ $\displaystyle(\iota\to A)^{D}\,$
$\displaystyle X^{D}\,\alpha:\equiv(x:X)(x^{D}:X^{D}\,x)\to
A^{D}\,X^{D}\,(\alpha\,x)$ $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{D}:(\Gamma:\mathsf{Con})\\{X\\}\to(X\to\mathsf{Set})\to\Gamma^{A}\,X\to\mathsf{Set}$
$\Gamma^{D}\,X^{D}\,\gamma:\equiv\\{A:\mathsf{Ty}\\}(x:\mathsf{Var}\,\Gamma\,A)\to
A^{D}\,X^{D}\,(\gamma\,x)$ $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{D}:(t:\mathsf{Tm}\,\Gamma\,A)\to\Gamma^{D}\,X^{D}\,\gamma\to
A^{D}\,X^{D}\,(t^{A}\,\gamma)$ $\displaystyle(\mathsf{var}\,x)^{D}\,$
$\displaystyle\gamma^{D}:\equiv\gamma^{D}\,x$
$\displaystyle(\mathsf{app}\,t\,u)^{D}\,$ $\displaystyle\gamma^{D}:\equiv
t^{D}\,\gamma^{D}\,(u^{A}\,\gamma)\,(u^{D}\,\gamma^{D})$ $\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}^{D}:(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\to\Gamma^{D}\,X^{D}\,\gamma\to\Delta^{D}\,X^{D}\,(\sigma^{A}\,\gamma)$
$\sigma^{D}\,\gamma^{D}\,x:\equiv(\sigma\,x)^{D}\,\gamma^{D}$

Analogously to before, everything depends on a predicate interpretation
$X^{D}:X\to\mathsf{Set}$ for $\iota$. For types, a predicate holds for a
function if the function preserves predicates. The interpretation of terms is
again a fundamental lemma, and we again have pointwise definitions for
contexts and substitutions.

######  Definition 6 (displayed algebras).

$\displaystyle\mathsf{DispAlg}:\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Alg}\,\Gamma\to\mathsf{Set}_{1}$
$\displaystyle\mathsf{DispAlg}\,\\{\Gamma\\}\,(X,\,\gamma):\equiv(X^{D}:X\to\mathsf{Set})\times\Gamma^{D}\,X^{D}\,\gamma$

######  Example 4.

We have the following computation.

$\mathsf{DispAlg}\,\\{\mathsf{NatSig}\\}\,(X,\,\mathit{zero},\,\mathit{suc})\equiv$
$\displaystyle(X^{D}$ $\displaystyle:X\to\mathsf{Set})$
$\displaystyle\times\,$ $\displaystyle(\mathit{zero^{D}}$
$\displaystyle:X^{D}\,\mathit{zero})$ $\displaystyle\times\,$
$\displaystyle(\mathit{suc^{D}}$ $\displaystyle:(n:X)\to X^{D}\,n\to
X^{D}\,(\mathit{suc}\,n))$

####  2.2.4 Sections

Sections of displayed algebras are “dependent” analogues of algebra morphisms,
where the codomain is displayed over the domain.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{S}:(A:\mathsf{Ty})\\{X\,X^{D}\\}(X^{S}:(x:X)\to
X^{D}\,x)\to(\alpha:A^{A}\,X)\to A^{D}\,X^{D}\,\alpha\to\mathsf{Set}$
$\displaystyle\iota^{S}\,$ $\displaystyle X^{S}\,\alpha\,\,\alpha^{D}:\equiv
X^{S}\,\alpha=\alpha^{D}$ $\displaystyle(\iota\to A)^{S}\,$ $\displaystyle
X^{S}\,\alpha\,\,\alpha^{D}:\equiv(x:X)\to
A^{S}\,X^{S}\,(\alpha\,x)\,(\alpha^{D}\,(X^{S}\,x))$
$\mathsf{Con}^{S}:(\Gamma:\mathsf{Con})\\{X\,X^{D}\\}(X^{S}:(x:X)\to
X^{D}\,x)\to(\gamma:\Gamma^{A}\,X)\to\Gamma^{D}\,X^{D}\,\gamma\to\mathsf{Set}$
$\Gamma^{S}\,X^{S}\,\gamma_{0}\,\gamma_{1}:\equiv\\{A:\mathsf{Ty}\\}(x:\mathsf{Var}\,\Gamma\,A)\to
A^{S}\,X^{S}\,(\gamma_{0}\,x)\,(\gamma_{1}\,x)$ $\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}^{S}:(t:\mathsf{Tm}\,\Gamma\,A)\to\Gamma^{S}\,X^{S}\,\gamma\,\gamma^{D}\to
A^{S}\,X^{S}\,(t^{A}\,\gamma)\,(t^{D}\,\gamma^{D})$
$\displaystyle(\mathsf{var}\,x)^{S}$
$\displaystyle\gamma^{S}:\equiv\gamma^{S}\,x$
$\displaystyle(\mathsf{app}\,t\,u)^{S}$ $\displaystyle\gamma^{S}:\equiv
t^{S}\,\gamma^{S}\,(u^{A}\,\gamma)$ $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{S}:(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\to\Gamma^{S}\,X^{S}\,\gamma\,\gamma^{D}\to\Delta^{S}\,X^{S}\,(\sigma^{A}\,\gamma)\,(\sigma^{A}\,\gamma^{D})$
$\sigma^{S}\,\gamma^{S}\,x=(\sigma\,x)^{S}\,\gamma^{S}$

######  Definition 7 (Displayed algebra sections (“sections” in short)).

$\displaystyle\mathsf{Section}:\\{\Gamma:\mathsf{Con}\\}\to(\gamma:\mathsf{Alg}\,\Gamma)\to\mathsf{DispAlg}\,\gamma\to\mathsf{Set}$
$\displaystyle\mathsf{Section}\,(X,\,\gamma)\,(X^{D}\,\gamma^{D}):\equiv(X^{S}:(x:X)\to
X^{D}\,x)\times\Gamma^{S}\,X^{S}\,\gamma\,\gamma^{D}$

######  Example 5.

We have the following computation.

$\mathsf{Section}\,\\{\mathsf{NatSig}\\}\,(X,\,\mathit{zero},\,\mathit{suc})\,(X^{D},\,\mathit{zero^{D}},\,\mathit{suc^{D}})\equiv$
$\displaystyle(X^{S}$ $\displaystyle:(x:X)\to X^{D}\,x)$
$\displaystyle\times\,$ $\displaystyle(\mathit{zero^{S}}$
$\displaystyle:X^{S}\,\mathit{zero}=\mathit{zero^{D}})$
$\displaystyle\times\,$ $\displaystyle(\mathit{suc^{S}}$
$\displaystyle:(n:X)\to
X^{S}\,(\mathit{suc\,n})=\mathit{suc^{D}}\,n\,(X^{S}\,n))$

######  Definition 8 (Induction).

We define a predicate which holds if an algebra supports induction.

$\displaystyle\mathsf{Inductive}:\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Alg}\,\Gamma\to\mathsf{Set}_{1}$
$\displaystyle\mathsf{Inductive}\,\\{\Gamma\\}\,\gamma:\equiv(\gamma^{D}:\mathsf{DispAlg}\,\gamma)\to\mathsf{Section}\,\gamma\,\gamma^{D}$

We can observe that
$\mathsf{Inductive}\,\\{\mathsf{NatSig}\\}\,(X,\,\mathsf{zero},\,\mathsf{suc})$
computes to the usual induction principle for natural numbers, but with
$\beta$-rules given as propositional equalities. The input $\mathsf{DispAlg}$
is a bundle of the induction motive and the methods, and the output
$\mathsf{Section}$ contains the $X^{S}$ eliminator function together with its
$\beta$-rules.

###  2.3 Term Algebras

In this section we show that if a type theory supports the inductive types
comprising the theory of signatures, it also supports every inductive type
which is described by the signatures.

Note that we specified $\mathsf{Tm}$ and $\mathsf{Sub}$, but did not need
either of them when specifying signatures, or when computing induction
principles. That signatures do not depend on terms is a property specific to
simple signatures; this will not be the case in Chapter 4 when we move to more
general signatures. However, terms and substitutions are already required in
the construction of term algebras.

The idea is that terms in contexts comprise initial algebras. For example,
$\mathsf{Tm}\,\mathsf{NatSig}\,\iota$ is the set of natural numbers (up to
isomorphism). Informally, this is because the only way to construct terms is
by applying the $\mathsf{suc}$ variable (given by $\mathsf{var}\,\mathsf{vz}$)
finitely many times to the $\mathsf{zero}$ variable (given by
$\mathsf{var}\,(\mathsf{vs}\,\mathsf{vz})$).

######  Definition 9 (Term algebras).

Fix an $\Omega:\mathsf{Con}$. We abbreviate $\mathsf{Tm}\,\Omega\,\iota$ as
$\mathsf{T}$; this will serve as the carrier set of the term algebra. We
additionally define the following.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{T}:(A:\mathsf{Ty})\to\mathsf{Tm}\,\Omega\,A\to A^{A}\,\mathsf{T}$
$\displaystyle\iota^{T}\,$ $\displaystyle t:\equiv t$ $\displaystyle(\iota\to
A)^{T}\,$ $\displaystyle t:\equiv\lambda\,u.\,A^{T}\,(\mathsf{app}\,t\,u)$
$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{T}:(\Gamma:\mathsf{Con})\to\mathsf{Sub}\,\Omega\,\Gamma\to\Gamma^{A}\,\mathsf{T}$
$\Gamma^{T}\,\nu\,\\{A\\}\,x:\equiv A^{T}\,(\nu\,x)$ $\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}^{T}:(t:\mathsf{Tm}\,\Gamma\,A)(\nu:\mathsf{Sub}\,\Omega\,\Gamma)\to
A^{T}\,(t[\nu])=t^{A}\,(\Gamma^{T}\,\nu)$
$\displaystyle(\mathsf{var}\,x)^{T}\,$ $\displaystyle\nu\text{ holds by
}\mathsf{refl}$ $\displaystyle(\mathsf{app}\,t\,u)^{T}\,$
$\displaystyle\nu\text{ holds by }t^{T}\,\nu\text{ and }u^{T}\,\nu$
$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{T}:(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)(\nu:\mathsf{Sub}\,\Omega\,\Gamma)\\{A\\}(x:\mathsf{Var}\,\Delta\,A)$
$\to\Delta^{T}\,(\sigma\circ\nu)\,x=\sigma^{A}\,(\Gamma^{T}\,\nu)\,x$
$\sigma^{T}\,\nu\,x:\equiv(\sigma\,x)^{T}\,\nu$

Now we can define the term algebra for $\Omega$ itself:

$\displaystyle\mathsf{TmAlg}_{\Omega}:\mathsf{Alg}\,\Omega$
$\displaystyle\mathsf{TmAlg}_{\Omega}:\equiv\Omega^{T}\,\Omega\,\mathsf{id}$

In the interpretation for contexts, it is important that $\Omega$ is fixed,
and we do induction on all $\Gamma$ contexts such that there is a
$\mathsf{Sub}\,\Omega\,\Gamma$. It would not work to try to compute term
algebras by direct induction on contexts because we need to refer to the same
$\mathsf{T}$ set in the interpretation of every type in a signature.

The interpretation of types embeds terms as $A$-algebras. At the base type
$\iota$, this embedding is simply the identity function, since
$\iota^{A}\,\mathsf{T}\equiv\mathsf{T}\equiv\mathsf{Tm}\,\Omega\,\iota$. At
function types we recursively proceed under a semantic $\lambda$. The
interpretation of contexts is pointwise.

The interpretations of terms and substitutions are coherence properties, which
relate the term algebra construction to term evaluation in the
$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$ model. For terms, if we pick
$\nu\equiv\mathsf{id}$, we get $A^{T}\,t=t^{A}\,\mathsf{TmAlg}_{\Omega}$. The
left side embeds $t$ in the term model via $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}^{T}$, while the right hand side evaluates $t$ in
the term model.

One way to view the term algebra construction, is that we are working in a
_slice model_ over the fixed $\Omega$, and every
$\nu:\mathsf{Sub}\,\Omega\,\Gamma$ can be viewed as an internal
$\Gamma$-algebra in this model. The term algebra construction demonstrates
that every such internal algebra yields an external element of $\Gamma^{A}$.

####  2.3.1 Recursor Construction

We show that $\mathsf{TmAlg}_{\Omega}$ supports a recursion principle, i.e. it
is weakly initial.

######  Definition 10 (Recursor construction).

We assume $(X,\,\omega):\mathsf{Alg}\,\Omega$; recall that $X:\mathsf{Set}$
and $\omega:\Omega^{A}\,X$. We define $\mathsf{R}:\mathsf{T}\to X$ as
$\mathsf{R}\,t:\equiv t^{A}\,\omega$. We additionally define the following.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{R}:(A:\mathsf{Ty})(t:\mathsf{Tm}\,\Omega\,A)\to
A^{M}\,\mathsf{R}\,(A^{T}\,t)\,(t^{A}\,\omega)$ $\displaystyle\iota^{R}\,$
$\displaystyle t:\equiv(\mathsf{refl}:t^{A}\,\omega=t^{A}\,\omega)$
$\displaystyle(\iota\to A)^{R}\,$ $\displaystyle
t:\equiv\lambda\,u.\,A^{R}\,(\mathsf{app}\,t\,u)$ $\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}^{R}:(\Gamma:\mathsf{Con})(\nu:\mathsf{Sub}\,\Omega\,\Gamma)\to\Gamma^{M}\,\mathsf{R}\,(\Gamma^{T}\,\nu)\,(\nu^{A}\,\omega)$
$\Gamma^{R}\,\nu\,x:\equiv A^{R}\,(\nu\,x)$

We define the recursor for $\Omega$ as

$\displaystyle\mathsf{Rec}_{\Omega}:(\mathit{alg}:\mathsf{Alg}\,\Omega)\to\mathsf{Mor}\,\mathsf{TmAlg}_{\Omega}\,\mathit{alg}$
$\displaystyle\mathsf{Rec}_{\Omega}\,(X,\,\omega):\equiv(\mathsf{R},\,\Omega^{R}\,\Omega\,\mathsf{id})$

In short, the way we get recursion is by evaluating terms in arbitrary
$(X,\,\omega)$ algebras using $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}$. The $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{R}$ operation
for types and contexts confirms that $\mathsf{R}$ preserves structure
appropriately, so that $\mathsf{R}$ indeed yields algebra morphisms.

We skip interpreting terms and substitutions by $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}^{R}$. It is necessary to do so with more general
signatures, but not in the current chapter.

####  2.3.2 Eliminator Construction

We take the idea of the previous section a bit further. We have seen that
recursion for term algebras is given by evaluation in the “standard”
$\mathsf{Set}$ model. Now, we show that induction for term algebras is
obtained from the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{D}$
interpretation into the logical predicate model over the $\mathsf{Set}$ model.

######  Definition 11 (Eliminator construction).

We assume $(X^{D},\,\omega^{D}):\mathsf{DispAlg}\,\mathsf{TmAlg}_{\Omega}$.
Recall that $X^{D}:\mathsf{T}\to\mathsf{Set}$ and
$\omega^{D}:\Omega^{D}\,X^{D}\,(\Omega^{T}\,\Omega\,\mathsf{id})$. Like
before, we first interpret the underlying set:

$\displaystyle\mathsf{E}:(t:\mathsf{T})\to X^{D}\,t$
$\displaystyle\mathsf{E}\,t:\equiv t^{D}\,\omega^{D}$

However, this definition is not immediately well-typed, since
$t^{D}\,\omega^{D}$ has type
$X^{D}\,(t^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id}))$, so we have to show that
$t^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id})=t$. This equation says that nothing
happens if we evaluate a term with type $\iota$ in the term model. We get it
from the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{T}$ interpretation of
terms:
$t^{T}\,\mathsf{id}:t[\mathsf{id}]=t^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id})$,
and we also know that $t[\mathsf{id}]=t$. We interpret types and contexts as
well:

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{E}:(A:\mathsf{Ty})(t:\mathsf{Tm}\,\Omega\,A)\to
A^{S}\,\mathsf{E}\,(t^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id}))\,(t^{D}\,\omega^{D})$
$\displaystyle\iota^{E}\,$ $\displaystyle
t:(t^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id}))^{D}\,\omega^{D}=t^{D}\,\omega^{D}$
$\displaystyle(\iota\to A)^{E}\,$ $\displaystyle
t:\equiv\lambda\,u.\,A^{E}\,(\mathsf{app}\,t\,u)$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{E}:(\Gamma:\mathsf{Con})(\nu:\mathsf{Sub}\,\Omega\,\Gamma)\to\Gamma^{S}\,\mathsf{E}\,(\nu^{A}\,(\Omega^{T}\,\Omega\,\mathsf{id}))\,(\nu^{D}\,\omega^{D})$
$\displaystyle\Gamma^{E}\,\nu\,x:\equiv A^{E}\,(\nu\,x)$

In $\iota^{E}$ we use the same equation as in the definition of $\mathsf{E}$.
In $(\iota\to A)^{E}$ the definition is well-typed because of the same
equation, but instantiated for the abstracted $u$ term this time. All of this
amounts to some additional path induction and transport fiddling in the
(intensional) Agda formalization. We get induction for $\Omega$ as below.

$\displaystyle\mathsf{Ind}_{\Omega}:(\mathit{alg}:\mathsf{DispAlg}\,\mathsf{TmAlg}_{\Omega})\to\mathsf{Section}\,\mathsf{TmAlg}_{\Omega}\,\mathit{alg}$
$\displaystyle\mathsf{Ind}_{\Omega}\,(X^{D},\,\omega^{D}):\equiv(E,\,\Omega^{E}\,\Omega\,\mathsf{id})$

###  2.4 Comparison to Endofunctors as Signatures

A well-known alternative definition of algebraic signatures is to view certain
cocontinuous endofunctors as such. For example, single-sorted signatures can
be defined to be endofunctors which preserve colimits of some ordinal-indexed
chains. For instance, if we have a $\kappa$-cocontinuous
$F:\mathbb{C}\to\mathbb{C}$, then algebras are given as
$(X:|\mathbb{C}|)\times(\mathbb{C}(F\,X,\,X))$, called _F-algebras_ ,
morphisms as commuting squares, and Adámek’s theorem [AK79] establishes the
existence of initial algebras.

An advantage of this approach is that we can describe different classes of
signatures by choosing different $\mathbb{C}$ categories:

  * •

If $\mathbb{C}$ is $\mathbf{Set}$, we get simple inductive theories.

  * •

If $\mathbb{C}$ is $\mathbf{Set}^{I}$ for some set $I$, we get indexed
inductive signatures.

  * •

If $\mathbb{C}$ is $\mathbf{Set}/I$, we get inductive-recursive signatures.

Another advantage is that signatures are fairly semantic in nature: they make
sense even if we have no syntactic presentation at hand. That said, often we
do need syntactic signatures, for use in proof assistants, or just to have a
convenient notation for a class of cocontinuous functors.

An elegant way of carving out a large class of such functors is to consider
polynomials as signatures. For example, when working in Set, a signature is an
element of $(S:\mathsf{Set})\times(P:S\to\mathsf{Set})$, and $(S,\,P)$ is
interpreted as a functor as $X\mapsto(s:S)\times(P\,s\to X)$. The initial
algebra is the W-type specified by $S$ shapes and $P$ positions. This yields
infinitary inductive types as well.

However, it is not known how to get _inductive-inductive_ signatures by
picking the right $\mathbb{C}$ category and a functor. In an inductive-
inductive signature, there may be multiple sorts, which can be indexed over
previously declared sorts. For example, in the signature for categories we
have $\mathsf{Obj}:\mathsf{Set}$ and
$\mathsf{Mor}:\mathsf{Obj}\to\mathsf{Obj}\to\mathsf{Set}$, indexed twice over
$\mathsf{Obj}$. Some extensions are required to the idea of $F$-algebras:

  * •

For inductive-inductive definitions with two sorts, Forsberg gives a
specification with two functors, and a considerably more complex notion of
algebras, involving dialgebras [NF13].111However, the dialgebra specification
only covers restricted signatures, where $B:A\to\mathsf{Set}$ constructor
types may refer to $A:\mathsf{Set}$ constructors, but no other dependency is
allowed. There is a more general and yet more complicated notion of signature
in [NF13], which is not anymore represented with functors.

  * •

For an arbitrary number of sorts, Altenkirch et al. [ACD+18] use a “list” of
functors, specified mutually with categories of algebras: each functor has as
domain the semantic category of all previous sorts.

The functors-as-signatures approach gets significantly less convenient as we
consider more general specifications. The approach of this thesis is to skip
the middle ground between syntactic signatures and semantic categories of
algebras: we treat syntactic signatures as a key component, and give direct
semantic interpretation for them. Although we lose the semantic nature of
signatures, our approach scales extremely well, all the way up to infinitary
quotient-inductive-inductive types in Chapter 5, and to some extent to higher
inductive-inductive types as well in Chapter 6.

If we look back at $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}:\mathsf{Con}\to\mathsf{Set}\to\mathsf{Set}$, we may note that
$\Gamma^{A}$ yields a functor, in fact the same functor (up to isomorphism)
that we would get from an endofunctor presentation. However, this is a
coincidence in the single-sorted case. We can view
$(X:|\mathbb{C}|)\times(\mathbb{C}(F\,X,\,X))$ as specifying the category of
algebras as the total category of a displayed category (by viewing the
$\Sigma$-type here as taking total categories; a $\Sigma$ in $\mathbf{Cat}$).
In our approach, we aim to get the displayed categories directly, without
talking about functors.

## CHAPTER 3 Semantics in Two-Level Type Theory

In this chapter we describe how two-level type theory is used as a
metatheoretic setting in the rest of this thesis. First, we provide motivation
and overview. Second, we describe models of type theories in general, and
models of two-level type theories as extensions. Third, we describe presheaf
models of two-level type theories. Finally, we generalize the semantics and
the term algebra construction from Chapter 2 in two-level type theory, as a
way to illustrate the applications.

###  3.1 Motivation

We note two shortcomings of the semantics presented in the previous chapter.

First, the semantics that we provided was not as general as it could be. We
used the internal $\mathsf{Set}$ universe to specify algebras, but algebras
make sense in many different categories. A crude way to generalize semantics
is to simply say that our formalization, which was carried out in the syntax
(i.e. initial model) of some intensional type theory, can be interpreted in
any model of the type theory. But this is wasteful: for simple inductive
signatures, it is enough to assume a category with finite products as semantic
setting. We do not need all the extra baggage that comes with a model of a
type theory.

Second, we were not able to reason about definitional equalities, only
propositional ones. We have a formalization of signatures and semantics in
intensional Agda, where the two notions differ111As opposed to in extensional
type theory, where they are the same., but only propositional equality is
subject to internal reasoning. For instance, we would like to show that term
algebras support recursion with strict $\beta$-rules, and for this we need to
reason about strict equality.

######  Notation 3.

We use $\scaleobj{.75}\bullet$ for the terminal object in a $\mathbb{C}$
category, with $\epsilon:\mathbb{C}(A,\,\scaleobj{.75}\bullet)$ for the unique
morphism. For products, we use $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\otimes\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ with
$(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\\!,\\!\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}):\mathbb{C}(A,\,B)\to\mathbb{C}(A,\,C)\to\mathbb{C}(A,\,B\otimes C)$
and $\mathsf{p}$ and $\mathsf{q}$ for first and second projections
respectively.

######  Example 6.

Assuming a category $\mathbb{C}$ with finite products, we specify natural
number algebras and binary tree algebras as follows. Below,
$\mathsf{Alg}_{\mathsf{NatSig}}$ and $\mathsf{Alg}_{\mathsf{TreeSig}}$ are
both sets in some metatheory, and the $\times$ in the definitions refer to the
metatheoretic $\Sigma$.

$\displaystyle\mathsf{Alg}_{\mathsf{NatSig}}$
$\displaystyle:\equiv(X:|\mathbb{C}|)\times\mathbb{C}(\scaleobj{.75}\bullet,\,X)\times\mathbb{C}(X,\,X)$
$\displaystyle\mathsf{Alg}_{\mathsf{TreeSig}}$
$\displaystyle:\equiv(X:|\mathbb{C}|)\times\mathbb{C}(\scaleobj{.75}\bullet,\,X)\times\mathbb{C}(X\otimes
X,\,X)$

How should we adjust $\mathsf{Alg}$ from the previous chapter to compute
algebras in $\mathbb{C}$, and $\mathsf{Mor}$ to compute their morphisms? While
it is possible to do this in a direct fashion, working directly with objects
and morphisms of $\mathbb{C}$ is rather unwieldy. $\mathbb{C}$ is missing many
convenience features of type theories.

  * •

There are no variables or binders. We are forced to work in a point-free style
or chase diagrams; both become difficult to handle above a certain level of
complexity.

  * •

There are no functions, universes or inductive types.

  * •

Substitution (with weakening as a special case) has to be handled explicitly
and manually. Substitutions are certain morphisms, while “terms” are also
morphisms, and we have to use composition to substitute terms. In contrast, if
we are working internally in a type theory, terms and substitutions are
distinct, and we only have to explicitly deal with terms, and substitutions
are automated and implicit.

The above overlaps with motivations for working in _internal languages_ [nc21]
of structured categories: they aid calculation and compact formalization by
hiding bureaucratic structural details.

A finite product category $\mathbb{C}$ does not have much of an internal
language, it is too bare-bones. But we can work instead in the internal
language of $\hat{\mathbb{C}}$, the category of presheaves over $\mathbb{C}$.
This allows faithful reasoning about $\mathbb{C}$, while also including all
convenience features of extensional type theory.

_Two-level type theories_ [ACKS19], or 2LTT in short, are type theories such
that they have “standard” interpretations in presheaf categories. A 2LTT has
an inner layer, where types and terms arise by embedding $\mathbb{C}$ in
$\hat{\mathbb{C}}$, and an outer layer, where constructions are inherited from
$\hat{\mathbb{C}}$. The exact details of the syntax may vary depending on what
structures $\mathbb{C}$ supports, and which type formers we assume in the
outer layer. Although it is possible to add assumptions to a 2LTT which
preclude standard presheaf semantics [ACKS19, Section 2.4.], we stick to basic
2LTT in this thesis. By using 2LTT, we are able to use a type-theoretic syntax
which differs only modestly from the style of definitions that we have seen so
far.

From a programming perspective, basic 2LTT provides a convenient syntax for
writing metaprograms. This can be viewed as _two-stage compilation_ : if we
have a 2LTT program with an inner type, we can run it, and it returns another
program, which lives purely in the inner theory.

###  3.2 Models of Type Theories

Before explaining 2LTT-specific features, we review models of type theories in
general. Variants of 2LTT will be obtained by adding extra features on the top
of more conventional type theories.

It is also worth to take a more general look at models at this point, because
the notions presented in this subsection (categories with families, type
formers) will be reused several times in this thesis, when specifying theories
of signatures.

####  3.2.1 The Algebraic View

We take an algebraic view of models and syntaxes of type theories throughout
this thesis. Models of type theories are algebraic structures: they are
categories with certain extra structure. The syntax of a type theory is
understood to be its initial model. In initial models, the underlying category
is the category of typing contexts and parallel substitutions, while the extra
structure corresponds to type and term formers, and equations quotient the
syntax by definitional equality.

Type theories can be described with quotient inductive-inductive (QII)
signatures, and their initial models are quotient inductive-inductive types
(QIITs). Hence, 2LTT is also a QII theory. We will first talk about QIITs in
Chapter 4. Until then, we shall make do with an informal understanding of
categorical semantics for type theories, without using anything in particular
from the metatheory of QIITs. There is some circularity here, that we talk
about QIITs in this thesis, but we employ QIITs when talking about them.
However, this is only an annoyance in exposition and not a fundamental issue:
Sections 4.5 and 5.7 describe how to eliminate circularity by a form of
bootstrapping.

The algebraic view lets us dispense with all kinds of “raw” syntactic objects.
We only ever talk about well-typed and well-formed objects, moreover, every
construction must respect definitional equalities. For terms in the algebraic
syntax, definitional equality coincides with metatheoretic equality. This
mirrors equality of morphisms in 1-category theory, where we usually reuse
metatheoretic equality in the same way.

In the following we specify notions of models for type theories. We split this
in two parts: categories with families and type formers.

####  3.2.2 Categories With Families

######  Definition 12.

A category with families (cwf) [Dyb95] is a way to specify the basic
structural rules for contexts, substitutions, types and terms. It yields a
dependently typed explicit substitution calculus. A cwf consists of the
following.

  * •

A category with a terminal object. We denote the set of objects as
$\mathsf{Con}:\mathsf{Set}$ and use capital Greek letters starting from
$\Gamma$ to refer to objects. The set of morphisms is
$\mathsf{Sub}:\mathsf{Con}\to\mathsf{Con}\to\mathsf{Set}$, and we use
$\sigma$, $\delta$ and so on to refer to morphisms. We write $\mathsf{id}$ for
the identity morphism and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\circ\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ for composition. The
terminal object is $\scaleobj{.75}\bullet$ with unique morphism
$\epsilon:\mathsf{Sub}\,\Gamma\,\scaleobj{.75}\bullet$. In initial models
(that is, syntaxes) of type theories, objects correspond to typing contexts,
morphisms to parallel substitutions and the terminal object to the empty
context; this informs the naming scheme.

  * •

A _family structure_ , containing $\mathsf{Ty}:\mathsf{Con}\to\mathsf{Set}$
and $\mathsf{Tm}:(\Gamma:\mathsf{Con})\to\mathsf{Ty}\,\Gamma\to\mathsf{Set}$.
We use $A$, $B$, $C$ to refer to types and $t$, $u$, $v$ to refer to terms.
$\mathsf{Ty}$ is a presheaf over the category of contexts and $\mathsf{Tm}$ is
a displayed presheaf over $\mathsf{Ty}$. This means that types and terms can
be substituted:

$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}]:\mathsf{Ty}\,\Delta\to\mathsf{Sub}\,\Gamma\,\Delta\to\mathsf{Ty}\,\Gamma$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}]:\mathsf{Tm}\,\Delta\,A\to(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\to\mathsf{Tm}\,\Gamma\,(A[\sigma])$

Substitution is functorial: we have $A[\mathsf{id}]\equiv A$ and
$A[\sigma\circ\delta]\equiv A[\sigma][\delta]$, and likewise for terms.

A family structure is additionally equipped with _context comprehension_ which
consists of a context extension operation $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}:(\Gamma:\mathsf{Con})\to\mathsf{Ty}\,\Gamma\to\mathsf{Con}$ together
with a natural isomorphism $\mathsf{Sub}\,\Gamma\,(\Delta\triangleright
A)\simeq((\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\times\mathsf{Tm}\,\Gamma\,(A[\sigma]))$.

The following notions are derivable from the comprehension structure:

  * •

By going right-to-left along the isomorphism, we recover _substitution
extension_ $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip
1.0pt\text{--}\hskip
1.0pt}:(\sigma:\mathsf{Sub}\,\Gamma\,\Delta)\to\mathsf{Tm}\,\Gamma\,(A[\sigma])\to\mathsf{Sub}\,\Gamma\,(\Delta\triangleright
A)$. This means that starting from $\epsilon$ or the identity substitution
$\mathsf{id}$, we can iterate $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ to build substitutions as
lists of terms.

  * •

By going left-to-right, and starting from
$\mathsf{id}:\mathsf{Sub}\,(\Gamma\triangleright A)\,(\Gamma\triangleright
A)$, we recover the _weakening substitution_
$\mathsf{p}:\mathsf{Sub}\,(\Gamma\triangleright A)\,\Gamma$ and the _zero
variable_ $\mathsf{q}:\mathsf{Tm}\,(\Gamma\triangleright A)\,(A[\mathsf{p}])$.

  * •

By weakening $\mathsf{q}$, we recover a notion of variables as De Bruijn
indices. In general, the $n$-th De Bruijn index is defined as
$\mathsf{q}[\mathsf{p}^{n}]$, where $\mathsf{p}^{n}$ denotes $n$-fold
composition.

Comprehension can be characterized either by taking $\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$,
$\mathsf{p}$ and $\mathsf{q}$ as primitive, or the natural isomorphism. The
two are equivalent, and we may switch between them, depending on which is more
convenient.

There are other ways for presenting the basic categorical structure of models,
which are nonetheless equivalent to cwfs, including natural models [Awo18] and
categories with attributes [Car78]. We use the cwf presentation for its
immediately algebraic character and closeness to conventional explicit
substitution syntax.

######  Notation 4.

As De Bruijn indices are hard to read, we will mostly use nameful notation for
binders. For example, assuming
$\mathsf{Nat}:\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Ty}\,\Gamma$ and
$\mathsf{Id}:\\{\Gamma:\mathsf{Con}\\}(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Tm}\,\Gamma\,A\to\mathsf{Tm}\,\Gamma\,A\to\mathsf{Ty}\,\Gamma$,
we may write
$\scaleobj{.75}\bullet\,\triangleright\,n:\mathsf{Nat}\,\triangleright\,p:\mathsf{Id}\,\mathsf{Nat}\,n\,n$
for a typing context, instead of using numbered variables or cwf combinators
as in
$\scaleobj{.75}\bullet\triangleright\mathsf{Nat}\triangleright\mathsf{Id}\,\mathsf{Nat}\,\mathsf{q}\,\mathsf{q}$.

######  Notation 5.

In the following, we will denote family structures by
($\mathsf{Ty}$,$\mathsf{Tm}$) pairs and overload context extension
$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}$ for different families.

######  Definition 13.

The following derivable operations are commonly used.

  * •

_Single substitution_ can be derived from parallel substitution as follows.
Assume $t:\mathsf{Tm}\,(\Gamma\triangleright A)\,B$, and
$u:\mathsf{Tm}\,\Gamma\,A$. $t$ is a term which may depend on the last
variable in the context, which has $A$ type. We can substitute that variable
with the $u$ term as
$t[\mathsf{id},\,u]:\mathsf{Tm}\,\Gamma\,(\mathsf{A}[\mathsf{id},\,u])$. Note
that term substitution causes the type to be substituted as well.
$(\mathsf{id},\,u):\mathsf{Sub}\,\Gamma\,(\Gamma\triangleright A)$ is well-
typed because $u:\mathsf{Tm}\,\Gamma\,A$ hence also
$u:\mathsf{Tm}\,\Gamma\,(A[\mathsf{id}])$.

  * •

We can _lift substitutions_ over binders as follows. Assuming
$\sigma:\mathsf{Sub}\,\Gamma\,\Delta$ and $A:\mathsf{Ty}\,\Delta$, we
construct a lifting of $\sigma$ which maps an additional $A$-variable to
itself:
$(\sigma\circ\mathsf{p},\,\mathsf{q}):\mathsf{Sub}\,(\Gamma\triangleright
A[\sigma])\,(\Delta\triangleright A)$. Let us see why this is well-typed. We
have $\mathsf{p}:\mathsf{Sub}\,(\Gamma\triangleright A[\sigma])\,\Gamma$ and
$\sigma:\mathsf{Sub}\,\Gamma\,\Delta$, so
$\sigma\circ\mathsf{p}:\mathsf{Sub}\,(\Gamma\triangleright
A[\sigma])\,\Delta$. Also, $\mathsf{q}:\mathsf{Tm}\,(\Gamma\triangleright
A[\sigma])\,(A[\sigma][\mathsf{p}])$, hence
$\mathsf{q}:\mathsf{Tm}\,(\Gamma\triangleright
A[\sigma])\,(A[\sigma\circ\mathsf{p}])$, thus
$(\sigma\circ\mathsf{p},\,\mathsf{q})$ typechecks.

######  Notation 6.

As a nameful notation for substitutions, we may write $t[x\mapsto u]$, for a
single substitution, or $t[x\mapsto u_{1},y\mapsto u_{2}]$ and so on.

In nameful notation we leave all weakening implicit, including substitution
lifting. Formally, if we have $t:\mathsf{Tm}\,\Gamma\,A$, we can only mention
$t$ in $\Gamma$. If we need to mention it in $\Gamma\triangleright B$, we need
to use $t[\mathsf{p}]$ instead. In the nameful notation,
$t:\mathsf{Tm}\,(\Gamma\triangleright x:B)\,A$ may be used.222Moreover, when
working in the internal syntax of a theory, we just write Agda-like type-
theoretic notation, without noting contexts and substitutions in any way.

####  3.2.3 Type formers

A family structure in a cwf may be closed under certain type formers, such as
functions, $\Sigma$-types, universes or inductive types. We give some examples
here for their specification. First, we look at common negative type formers;
these are the type formers which can be specified using isomorphisms. Then, we
consider positive type formers, and finally universes.

##### Negative types

######  Definition 14.

A $(\mathsf{Ty},\,\mathsf{Tm})$ family supports $\Pi$-types if it supports the
following.

$\displaystyle\Pi$
$\displaystyle:(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Ty}\,(\Gamma\triangleright
A)\to\mathsf{Ty}\,\Gamma$ $\displaystyle\Pi[]$
$\displaystyle:(\Pi\,A\,B)[\sigma]\equiv\Pi\,(A[\sigma])\,(B[\sigma\circ\mathsf{p},\,\mathsf{q}])$
$\displaystyle\mathsf{app}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\Pi\,A\,B)\to\mathsf{Tm}\,(\Gamma\triangleright
A)\,B$ $\displaystyle\mathsf{lam}$
$\displaystyle:\mathsf{Tm}\,(\Gamma\triangleright
A)\,B\to\mathsf{Tm}\,\Gamma\,(\Pi\,A\,B)$ $\displaystyle\Pi\beta$
$\displaystyle:\mathsf{app}\,(\mathsf{lam}\,t)\equiv t$ $\displaystyle\Pi\eta$
$\displaystyle:\mathsf{lam}\,(\mathsf{app}\,t)\equiv t$
$\displaystyle\mathsf{lam}[]$
$\displaystyle:(\mathsf{lam}\,t)[\sigma]\equiv\mathsf{lam}\,(t[\sigma\circ\mathsf{p},\,\mathsf{q}])$

Here, $\Pi$ is the type formation rule. $\mathsf{\Pi[]}$ is the type
substitution rule, expressing that substituting $\Pi$ proceeds structurally on
constituent types. Note $B[\sigma\circ\mathsf{p},\,\mathsf{q}]$, where we lift
$\sigma$ over the additional binder.

The rest of the rules specify a natural isomorphism
$\mathsf{Tm}\,\Gamma\,(\Pi\,A\,B)\simeq\mathsf{Tm}\,(\Gamma\triangleright
A)\,B$. We only need a substitution rule (i.e. a naturality rule) for one
direction of the isomorphism, since the naturality of the other map is
derivable.

This way of specifying $\Pi$-types is very convenient if we have explicit
substitutions. The usual “pointful” specification is equivalent to this. For
example, we have the following derivation of pointful application:

$\displaystyle\mathsf{app}^{\prime}:\mathsf{Tm}\,\Gamma\,(\Pi\,A\,B)\to(u:\mathsf{Tm}\,\Gamma\,A)\to\mathsf{Tm}\,\Gamma\,(B[\mathsf{id},\,u])$
$\displaystyle\mathsf{app}^{\prime}\,t\,u:\equiv(\mathsf{app}\,t)[\mathsf{id},\,u]$

_Remark on naturality._ The above specification for $\Pi$ can be written more
compactly if we assume that everything is natural with respect to
substitution.

$\displaystyle\Pi$
$\displaystyle:(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Ty}\,(\Gamma\triangleright
A)\to\mathsf{Ty}\,\Gamma$ $\displaystyle(\mathsf{app},\,\mathsf{lam})$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\Pi\,A\,B)\simeq\mathsf{Tm}\,(\Gamma\triangleright
A)\,B$

This is a reasonable assumption; in the rest of the thesis we only ever define
structures on cwfs which are natural in this way.

######  Notation 7.

From now on, when specifying type formers in family structures, we assume that
everything is natural, and thus omit substitution equations.

There are ways to make this idea more precise, and take it a step further by
working in languages where only natural constructions are possible. The term
_higher-order abstract syntax_ (HOAS) is sometimes used for this style. It
lets us also omit contexts, so we would only need to write

$\displaystyle\Pi$
$\displaystyle:(A:\mathsf{Ty})\to(\mathsf{Tm}\,A\to\mathsf{Ty})\to\mathsf{Ty}$
$\displaystyle(\mathsf{app},\,\mathsf{lam})$
$\displaystyle:\mathsf{Tm}\,(\Pi\,A\,B)\simeq((a:\mathsf{Tm}\,A)\to\mathsf{Tm}\,(B\,a))$

Recently several promising works emerged in this area [Uem19, SA21, BKS21].
Although this technology is likely to be the preferred future direction in the
metatheory of type theories, this thesis does not make use of it. The field is
rather fresh, with several different approaches and limited amount of
pedagogical exposition, and the new techniques would also raise the level of
abstraction in this thesis, contributing to making it less accessible. It is
also not obvious how exactly HOAS-style could be employed to aid formalization
here, and it would require significant additional research. Often, a setup
with multiple modalities (“multimodal” [GKNB20]) is required [BKS21] because
we work with presheaves over different cwfs. It seems that a synthetic notion
of dependent modes would be also required to formalize constructions in this
thesis, since we often work with displayed presheaves over displayed cwfs.
This is however not yet developed in the literature.

######  Definition 15.

A family structure supports constant families if we have the following.

$\displaystyle\mathsf{K}$
$\displaystyle:\mathsf{Con}\to\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Ty}\,\Gamma$
$\displaystyle(\mathsf{app}_{\mathsf{K}},\,\mathsf{lam}_{\mathsf{K}})$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\mathsf{K}\,\Delta)\simeq\mathsf{Sub}\,\Gamma\,\Delta$

Constant families express that every context can be viewed as a non-dependent
type in any context. Having constant families is equivalent to the _democracy_
property for a cwf [CD14, NF13]. Constant families are convenient when
building models because they let us model non-dependent types as semantic
contexts, which are often simpler structures than semantic types. From a
programming perspective, constant families specify closed record types, where
$\mathsf{K}\,\Delta$ has $\Delta$-many fields.

If we have equalities of sets for the specification, i.e.
$\mathsf{Tm}\,\Gamma\,(\mathsf{K}\,\Delta)\equiv\mathsf{Sub}\,\Gamma\,\Delta$,
we have strict constant families.

######  Definition 16.

A family structure supports $\Sigma$-types if we have

$\displaystyle\Sigma$
$\displaystyle:(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Ty}\,(\Gamma\triangleright
A)\to\mathsf{Ty}\,\Gamma$ $\displaystyle(\mathsf{proj},\,(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}))$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\Sigma\,A\,B)\simeq((t:\mathsf{Tm}\,\Gamma\,A)\times\mathsf{Tm}\,\Gamma\,(B[\mathsf{id},\,t]))$

We may write $\mathsf{proj}_{1}$ and $\mathsf{proj}_{2}$ for composing the
metatheoretic first and second projections with $\mathsf{proj}$.

######  Definition 17.

A family structure supports the unit type if we have
$\top:\mathsf{Ty}\,\Gamma$ such that $\mathsf{Tm}\,\Gamma\,\top\simeq\top$,
where the $\top$ on the right is the metatheoretic unit type, and we overload
$\top$ for the internal unit type. From this, we get the internal
$\mathsf{tt}:\mathsf{Tm}\,\Gamma\,\top$, which is definitionally unique.

######  Definition 18.

A family structure supports extensional identity types if there is
$\mathsf{Id}:\mathsf{Tm}\,\Gamma\,A\to\mathsf{Tm}\,\Gamma\,A\to\mathsf{Ty}\,\Gamma$
such that
$(\mathsf{reflect},\,\mathsf{refl}):\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)\simeq(t\equiv
u)$.

It is also possible to give a positive definition for identity types, in which
case we get intensional identity. Extensional identity corresponds to a
categorical equalizer of terms (a limit), while the Martin-Löf-style
intensional identity is a positive (inductive) type.

This choice between negative and positive specification generally exists for
type formers with a single term construction rule. For example, $\Sigma$ can
be defined as a positive type, with an elimination rule that behaves like
pattern matching. Positive $\Sigma$ is equivalent to negative $\Sigma$,
although it only supports propositional $\eta$-rules. In contrast, positive
identity is usually _not_ equivalent to negative identity.

$\mathsf{refl}:t\equiv u\to\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)$ expresses
reflexivity of identity: definitionally equal terms are provably equal.
$\mathsf{reflect}$, which goes the other way around, is called _equality
reflection_ : provably equal terms are identified in the metatheory.

Uniqueness of identity proofs (UIP) is often ascribed to the extensional
identity type (see e.g. [Hof95]). UIP means that
$\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)$ has at most a single inhabitant up
to $\mathsf{Id}$. However, UIP is not something which is inherent in the
negative specification, instead it is inherited from the metatheory. If
$\mathsf{Tm}$ forms a homotopy set in the metatheory, then internal equality
proofs inherit uniqueness through the defining isomorphism.

##### Positive types

We do not dwell much on positive types here, as elsewhere in this thesis we
talk a lot about specifying such types anyway. We provide here some background
and a small example.

The motivation is to specify initial internal algebras in a cwf. However,
specifying the uniqueness of recursors using definitional equality is
problematic, if we are to have decidable and efficient conversion checking for
a type theory. Consider the specification of $\mathsf{Bool}$ together with its
recursor.

$\displaystyle\mathsf{Bool}$ $\displaystyle:\mathsf{Ty}\,\Gamma$
$\displaystyle\mathsf{true}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,\mathsf{Bool}$
$\displaystyle\mathsf{false}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,\mathsf{Bool}$
$\displaystyle\mathsf{BoolRec}$
$\displaystyle:(B:\mathsf{Ty}\,\Gamma)\to\mathsf{Tm}\,\Gamma\,B\to\mathsf{Tm}\,\Gamma\,B\to\mathsf{Tm}\,\Gamma\,\mathsf{Bool}\to\mathsf{Tm}\,\Gamma\,B$
$\displaystyle\mathsf{true}\beta$
$\displaystyle:\mathsf{BoolRec}\,B\,t\,f\,\mathsf{true}\equiv t$
$\displaystyle\mathsf{false}\beta$
$\displaystyle:\mathsf{BoolRec}\,B\,t\,f\,\mathsf{false}\equiv f$

$\mathsf{BoolRec}$ together with the $\beta$-rules specifies an internal
$\mathsf{Bool}$-algebra morphism. A possible way to specify definitional
uniqueness is as follows. Assuming $B:\mathsf{Ty}\,\Gamma$,
$t:\mathsf{Tm}\,\Gamma\,B$, $f:\mathsf{Tm}\,\Gamma\,B$ and
$m:\mathsf{Tm}\,(\Gamma\triangleright b:\mathsf{Bool})\,B$, such that
$m[b\mapsto\mathsf{true}]\equiv t$ and $m[b\mapsto\mathsf{false}]\equiv f$, it
follows that $\mathsf{BoolRec}\,B\,t\,f\,b:\mathsf{Tm}\,(\Gamma\triangleright
b:\mathsf{Bool})\,B$ is equal to $m$.

Unfortunately, deciding conversion with this rule entails deciding pointwise
equality of arbitrary $\mathsf{Bool}$ functions, which can be done in
exponential time in the number of $\mathsf{Bool}$ arguments. More generally,
Scherer presented a decision algorithm for conversion checking with strong
finite sums and products in simple type theory [Sch17], which also takes
exponential time. If we move to natural numbers with definitionally unique
recursion, conversion checking becomes undecidable. To illustrate this,
consider checking conversion between any closed term
$t:\mathsf{Nat}\to\mathsf{Nat}$ and the identity function. To cover the
$\eta$-rule, we would have to decide $t\,\mathsf{zero}\equiv\mathsf{zero}$ and
$(n:\mathsf{Tm}\,\scaleobj{.75}\bullet\,\mathsf{Nat})\to
t\,(\mathsf{suc}\,n)\equiv\mathsf{suc}\,(t\,n)$. Assuming canonicity, this is
equivalent to deciding $(n:\mathbb{N})\to
t\,(\mathsf{suc}^{n}\,\mathsf{zero})\equiv(\mathsf{suc}^{n}\,\mathsf{zero})$,
where $\mathsf{suc}^{n}\,\mathsf{zero}$ denotes a canonical numeral.

The standard solution is to have dependent elimination principles instead:
this allows inductive reasoning, canonicity and effectively decidable
definitional equality at the same time. For $\mathsf{Bool}$, we would have

$\displaystyle\mathsf{BoolInd}$
$\displaystyle:(B:\mathsf{Ty}\,(\Gamma\triangleright
b:\mathsf{Bool}))\to\mathsf{Tm}\,\Gamma\,(B[b\mapsto\mathsf{true}])$
$\displaystyle\to\mathsf{Tm}\,\Gamma\,(B[b\mapsto\mathsf{false}])\to(t:\mathsf{Tm}\,\Gamma\,\mathsf{Bool})\to\mathsf{Tm}\,\Gamma\,(B[b\mapsto
t])$

together with $\mathsf{BoolInd}\,B\,t\,f\,\mathsf{true}\equiv t$ and
$\mathsf{BoolInd}\,B\,t\,f\,\mathsf{false}\equiv f$.

Of course, if we assume extensional identity types, we have undecidable
conversion anyway, and definitionally unique recursion is equivalent to
induction. But decidable conversion is a pivotal part of type theory, which
makes it possible to relegate a deluge of boilerplate to computers, so
decidable conversion should be kept in mind.

##### Universes

Universes are types which classify types. There are several different flavors
of universes.

######  Definition 19.

A Tarski-style universe consists of the following data:

$\displaystyle\mathsf{U}:\mathsf{Ty}\,\Gamma\hskip
20.00003pt\mathsf{El}:\mathsf{Tm}\,\Gamma\,\mathsf{U}\to\mathsf{Ty}\,\Gamma$

This is a weak classifier, since not all elements of $\mathsf{Ty}\,\Gamma$ are
necessarily represented as terms of the universe. Like families, Tarski
universes can be closed under type formers. For instance, if $\mathsf{U}$ has
$\mathsf{Nat}$, we have the following:

$\displaystyle\mathsf{Nat}:\mathsf{Tm}\,\Gamma\,\mathsf{U}\hskip
10.00002pt\mathsf{zero}:\mathsf{Tm}\,\Gamma\,(\mathsf{El}\,\mathsf{Nat})\hskip
10.00002pt\mathsf{suc}:\mathsf{Tm}\,\Gamma\,(\mathsf{El}\,\mathsf{Nat})\to\mathsf{Tm}\,\Gamma\,(\mathsf{El}\,\mathsf{Nat})$
$\displaystyle\mathsf{NatElim}$
$\displaystyle:\,\,\,(P:\mathsf{Ty}\,(\Gamma\triangleright
n:\mathsf{El}\,\mathsf{Nat}))$
$\displaystyle\to\mathsf{Tm}\,\Gamma\,(P[n\mapsto\mathsf{zero}])$
$\displaystyle\to\mathsf{Tm}\,(\Gamma\triangleright
n:\mathsf{El}\,\mathsf{Nat}\triangleright\mathit{np}:P[n\mapsto
n])\,(P[n\mapsto\mathsf{suc}\,n])$
$\displaystyle\to(n:\mathsf{Tm}\,\Gamma\,(\mathsf{El}\,\mathsf{Nat}))\to\mathsf{Tm}\,\Gamma\,(P[n\mapsto
n])$

If all type formers in $\mathsf{U}$ follow this scheme, $\mathsf{U}$ may be
called a weakly Tarski universe. If we assume that every type former in
$\mathsf{U}$ is also duplicated in $(\mathsf{Ty},\,\mathsf{Tm})$, moreover
$\mathsf{El}$ preserves all type formers, so that e.g.
$\mathsf{El}\,\mathsf{Nat}$ is definitionally equal to the natural number type
in $\mathsf{Ty}$, then $\mathsf{U}$ is strongly Tarski.

It is often more convenient to have stronger classifiers as universes, so that
_all_ types in a given family structure are represented.

######  Definition 20.

Ignoring size issues for now, Coquand universes [Coq18] are specified as
follows:

$\mathsf{U}:\mathsf{Ty}\,\Gamma\hskip
10.00002pt(\mathsf{El},\,\mathsf{c}):\mathsf{Tm}\,\Gamma\,\mathsf{U}\simeq\mathsf{Ty}\,\Gamma$

$\mathsf{c}$ maps every type in $\mathsf{Ty}$ to a code in $\mathsf{U}$. Now
we can ignore $\mathsf{El}$ when specifying type formers, as $\mathsf{c}$ can
be always used to get a code in $\mathsf{U}$ for a type.

Unfortunately, the exact specification above yields an inconsistent “type-in-
type” system because $\mathsf{U}$ itself has a code in $\mathsf{U}$. The
standard solution is to have multiple family structures
$(\mathsf{Ty}_{i},\,\mathsf{Tm}_{i})$, indexed by universe levels, and have
$\mathsf{U}_{i}:\mathsf{Ty}_{i+1}\,\Gamma$ and
$\mathsf{Tm}_{i+1}\,\Gamma\,\mathsf{U}_{i}\simeq\mathsf{Ty}_{i}\,\Gamma$. For
a general specification of consistent universe hierarchies, see [Kov22a]. We
omit universe indices in the following, and implicitly assume “just enough”
universes for particular purposes.

######  Definition 21.

Russell universes are Coquand universes additionally satisfying
$\mathsf{Tm}\,\Gamma\,\mathsf{U}\equiv\mathsf{Ty}\,\Gamma$ as an equality of
sets, and also $\mathsf{El}\,t\equiv t$. This justifies omitting $\mathsf{El}$
and $\mathsf{c}$ from informal notation, implicitly casting between
$\mathsf{Tm}\,\Gamma\,\mathsf{U}$ and $\mathsf{Ty}\,\Gamma$.

Russell-style universes are commonly supported in set-theoretic models. They
are also often inherited from meta-type-theories which themselves have
Russell-universes. Major implementations of type theories (Coq, Lean, Agda,
Idris) are all such.

###  3.3 Two-Level Type Theory

####  3.3.1 Models

We describe models of 2LTT in the following. This is not the only possible way
to present 2LTT; our approach differs from [ACKS19] in some ways. We will
summarize the differences at the end of this section.

######  Definition 22.

A model of a two-level type theory is a model of type theory such that

  * •

It supports a Tarski-style universe $\mathsf{Ty}_{0}:\mathsf{Ty}\,\Gamma$ with
decoding
$\mathsf{Tm}_{0}:\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0}\to\mathsf{Ty}\,\Gamma$.

  * •

$\mathsf{Ty}_{0}$ may be closed under arbitrary type formers, however, it is
only possible to eliminate from $\mathsf{Ty}_{0}$ type formers to types in
$\mathsf{Ty}_{0}$.

Types in $\mathsf{Ty}_{0}$ are called _inner_ types, while other types are
_outer_. Alternatively, we may talk about _object-level_ and _meta-level_
types.

For example, if we have inner functions, we have the following:

$\displaystyle\Pi_{0}$
$\displaystyle:(A:\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0})\to\mathsf{Tm}\,(\Gamma\triangleright\mathsf{Tm}_{0}\,A)\to\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0}$
$\displaystyle(\mathsf{app}_{0},\,\mathsf{lam}_{0})$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,(\Pi_{0}\,A\,B))\simeq\mathsf{Tm}\,(\Gamma\triangleright\mathsf{Tm}_{0}\,A)\,(\mathsf{Tm}_{0}\,B)$

If we have inner Booleans, we have the following (with $\beta$-rules omitted):

$\displaystyle\mathsf{Bool}_{0}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0}$
$\displaystyle\mathsf{true}_{0}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,\mathsf{Bool}_{0})$
$\displaystyle\mathsf{false}_{0}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,\mathsf{Bool}_{0})$
$\displaystyle\mathsf{BoolInd_{0}}$
$\displaystyle:(B:\mathsf{Tm}\,(\Gamma\triangleright
b:\mathsf{Tm}_{0}\,\mathsf{Bool}_{0})\,\mathsf{Ty}_{0})$
$\displaystyle\to\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,(B[b\mapsto\mathsf{true}_{0}]))$
$\displaystyle\to\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,(B[b\mapsto\mathsf{false}_{0}]))$
$\displaystyle\to(t:\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}))\to\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,(B[b\mapsto
t]))$

Intuitively, we can view outer types and terms as metatheoretical, while
$\mathsf{Ty}_{0}$ represents the set of types in the object theory, and
$\mathsf{Tm}_{0}$ witnesses that any object type can be mapped to a
metatheoretical set of object terms. The restriction on elimination is
crucial. If we have a Boolean term in the object language, we can use the
object-level elimination principle to construct new object terms. But it makes
no sense to eliminate into the metatheory. In fact, an object-level Boolean
term is not necessarily $\mathsf{true}$ or $\mathsf{false}$, it can also be
just a variable or neutral term in some context, or it can be an arbitrary
non-canonical value in a given model.

We review some properties of 2LTT. An important point is the action of
$\mathsf{Tm}_{0}$ on type formers. In general, $\mathsf{Tm}_{0}$ preserves the
negative type formers but not others.

For example, we have the isomorphism
$\mathsf{Tm}_{0}\,(\Pi_{0}\,A\,B)\simeq\Pi_{1}\,(\mathsf{Tm}_{0}\,A)\,(\mathsf{Tm}_{0}\,B)$,
where $\Pi_{1}$ denotes outer functions. We move left-to-right by mapping $t$
to $\mathsf{lam}_{1}\,(\mathsf{app}_{1}\,t)$, and the other way by mapping $t$
to $\mathsf{lam}_{0}\,(\mathsf{app}_{0}\,t)$. The preservation of $\Sigma$,
$\top$, $\mathsf{K}$ and extensional identity is analogous.

In contrast, we can map from outer positive types to inner ones, but not the
other way around. From $b:\mathsf{Tm}\,\Gamma\,\mathsf{Bool}_{1}$, we can use
the outer $\mathsf{Bool}_{1}$ recursor to return in
$\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}$. In the other direction, only constant
functions are definable since the $\mathsf{Bool}_{0}$ recursor only targets
types in $\mathsf{Ty}_{0}$.

It may be the case that there are universes in the inner layer. For example,
disregarding size issues (or just accepting an inconsistent inner theory),
there may be an $\mathsf{U}_{0}$ in $\mathsf{Ty}_{0}$ such that we have
$\mathsf{Tm}\,\Gamma\,(\mathsf{Tm}_{0}\,\mathsf{U}_{0})\equiv\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0}$.
This amounts to having a Russell-style inner universe with type-in-type.
Assume that we have $\mathsf{U}_{1}$ as well, as a meta-level Russell
universe. Then we can map from $\mathsf{Tm}_{0}\,\mathsf{U}_{0}$ to
$\mathsf{U}_{1}$, by taking $A$ to $\mathsf{Tm}_{0}\,A$, but we cannot map in
the other direction.

####  3.3.2 Internal Syntax and Notation

In the rest of this thesis we will often work internally to a 2LTT, i.e. we
use 2LTT as metatheory. We adapt the metatheoretical notations used so far. We
list used features and conventions below.

  * •

We keep previous notation for type formers. For instance, $\Pi$-types are
written as $(x:A)\to B$ or as $A\to B$.

  * •

We assume a Coquand-style universe in the outer layer, named $\mathsf{Set}$.
As before, we leave the sizing levels implicit; if we were fully precise, we
would write $\mathsf{Set}_{i}$ for a hierarchy of outer universes. Despite
having a Coquand universe, we shall omit encoding and decoding in the internal
syntax, and instead work in Russell-style. In practical implementations,
elaborating Russell-style notation to Coquand-style is straightforward to do.

  * •

If the same type formers are supported both in the inner and outer layers, we
may distinguish them by 0 and 1 subscripts, e.g. by having $\mathsf{Bool}_{0}$
and $\mathsf{Bool}_{1}$. We omit some inferable subscripts, e.g. for $\Pi$ and
$\Sigma$-types. In these cases, we usually know from the type parameters which
type former is meant. For example,
$\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}\to\mathsf{Bool}_{1}$ can only refer to
outer functions.

  * •

We have the convention that $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!=\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ refers to the inner
equality type, while $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\equiv\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ refers to the
outer equality type. If the inner equality is extensional, the choice between
$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\\!=\\!\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\equiv\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ is immaterial,
but in Section 3.5 and Chapter 6 we do have intensional inner equality.

  * •

By having $\mathsf{Set}$, we are able to have $\mathsf{Ty}_{0}:\mathsf{Set}$
and $\mathsf{Tm}_{0}:\mathsf{Ty}_{0}\to\mathsf{Set}$. So we do not have to
deal with proper meta-level types, and have a more uniform notation. Notation
and specification for inner type formers changes accordingly. For example, for
inner $\Pi$-types we may write $(x:A)\to B$ if $A:\mathsf{Ty}_{0}$ and $B$
depends on $x:\mathsf{Tm}_{0}\,A$. This also enables a higher-order
specification: if $B:\mathsf{Tm}_{0}\,A\to\mathsf{Ty}_{0}$, then $(x:A)\to
B\,x:\mathsf{Ty}_{0}$, and the specifying isomorphism for $\Pi$ can be written
as $\mathsf{Tm}_{0}\,((x:A)\to
B\,x)\simeq((x:\mathsf{Tm}_{0}\,A)\to\mathsf{Tm}_{0}\,(B\,x))$. Note that the
definition of $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\simeq\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ requires a
meta-level identity type.

######  Notation 8.

An explicit notation for inner function abstraction would look like
$\mathsf{lam}_{0}\,t$ for
$t:(x:\mathsf{Tm}_{0}\,A)\to\mathsf{Tm}_{0}\,(B\,x)$. This results in “double”
abstraction, e.g. in
$\mathsf{lam}_{0}\,(\lambda\,x.\,\mathsf{suc}_{0}\,(\mathsf{suc}_{0}\,x)):\mathsf{Tm}_{0}\,(\mathsf{Nat}_{0}\to\mathsf{Nat}_{0})$.
Instead of this, we write $\lambda_{0}\,x.\,t$ as a notation, thus we write
$\lambda_{0}\,x.\,\mathsf{suc}_{0}\,(\mathsf{suc}_{0}\,x)$ for the above
example. We may also group multiple $\lambda_{0}$ binders together the same
way as with $\lambda$.

  * •

We may omit inferable $\mathsf{Tm}_{0}$ applications. For instance,
$\mathsf{Bool}_{1}\to\mathsf{Bool}_{0}$ can be “elaborated” to
$\mathsf{Bool}_{1}\to\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}$ without ambiguity,
since the function codomain must be on the same level as the domain, and the
only thing we can do to make sense of this is to lift the codomain by
$\mathsf{Tm}_{0}$. Sometimes there is some ambiguity:
$(\mathsf{Bool}_{0}\to\mathsf{Bool}_{0})\to\mathsf{Bool}_{1}$ can be
elaborated both to
$\mathsf{Tm}_{0}\,(\mathsf{Bool}_{0}\to\mathsf{Bool}_{0})\to\mathsf{Bool}_{1}$
and to
$(\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}\to\mathsf{Tm}_{0}\,\mathsf{Bool}_{0})\to\mathsf{Bool}_{1}$.
However, in this case the two output types are definitionally isomorphic
because of the $\Pi$-preservation by $\mathsf{Tm}_{0}$. Hence, the elaboration
choice does not make much difference, so we may still omit $\mathsf{Tm}_{0}$-s
in situations like this.

######  Example 7.

Working in the internal syntax of 2LTT, the specification of
$\mathsf{Bool}_{0}$ looks like the following (omitting $\beta$ again):

$\displaystyle\mathsf{Bool}_{0}$ $\displaystyle:\mathsf{Ty}_{0}$
$\displaystyle\mathsf{true}_{0}$ $\displaystyle:\mathsf{Bool}_{0}$
$\displaystyle\mathsf{false}_{0}$ $\displaystyle:\mathsf{Bool}_{0}$
$\displaystyle\mathsf{BoolInd_{0}}$
$\displaystyle:(B:\mathsf{Bool}_{0}\to\mathsf{Ty}_{0})\to
B\,\mathsf{true}_{0}\to B\,\mathsf{false}_{0}\to(t:\mathsf{Bool}_{0})\to B\,t$

If we elaborate the type of $\mathsf{BoolInd_{0}}$, we get the following:

$\displaystyle\mathsf{BoolInd_{0}}$
$\displaystyle:(B:\mathsf{Tm}_{0}\,\mathsf{Bool}_{0}\to\mathsf{Ty}_{0})\to\mathsf{Tm}_{0}\,(B\,\mathsf{true}_{0})\to\mathsf{Tm}_{0}\,(B\,\mathsf{false}_{0})$
$\displaystyle\to(t:\mathsf{Tm}_{0}\,\mathsf{Bool}_{0})\to\mathsf{Tm}_{0}\,(B\,t)$

Here, the type is forced to live in the outer level because of the dependency
on $\mathsf{Ty}_{0}$. Since $\mathsf{Ty}_{0}$ is an outer type,
$\mathsf{Bool}_{0}\to\mathsf{Ty}_{0}$ must be lifted, which in turn requires
all other types to be lifted as well.

####  3.3.3 Alternative Presentation for 2LTT

We digress a bit on a different way to present 2LTT. In the primary 2LTT
reference [ACKS19], inner and outer layers are specified as follows. We have
two different _family structures_ on the base cwf,
$(\mathsf{Ty}_{0},\,\mathsf{Tm}_{0})$ and
$(\mathsf{Ty}_{1},\,\mathsf{Tm}_{1})$, and a morphism between them. A family
morphism is natural transformation mapping types to types and terms to terms,
which is an isomorphism on terms. We might name the component maps as follows:

$\displaystyle\Uparrow$
$\displaystyle:\mathsf{Ty}_{0}\,\Gamma\to\mathsf{Ty}_{1}\,\Gamma$
$\displaystyle\uparrow$
$\displaystyle:\mathsf{Tm}_{0}\,\Gamma\,A\to\mathsf{Tm}_{1}\,\Gamma\,(\Uparrow\\!A)$
$\displaystyle\downarrow$
$\displaystyle:\mathsf{Tm}_{1}\,\Gamma\,(\Uparrow\\!A)\to\mathsf{Tm}_{0}\,\Gamma\,A$

An advantage of this presentation is that we may close
$(\mathsf{Ty}_{0},\,\mathsf{Tm}_{0})$ under type formers without any encoding
overhead, for example by having $\mathsf{Bool}_{0}:\mathsf{Ty}_{0}\,\Gamma$,
$\mathsf{true}_{0}:\mathsf{Tm}_{0}\,\Gamma\,\mathsf{Bool}_{0}$, etc., without
the Tarski-style decoding. On the other hand, we do not automatically get an
outer universe of inner types. We can recover that in two ways:

  * •

We can assume an inner universe $\mathsf{U}_{0}:\mathsf{Ty}_{0}\,\Gamma$,
which can be lifted to the outer theory as $\Uparrow\\!\mathsf{U}_{0}$.
However, we may not want to make this assumption, in order to keep the inner
theory as simple as possible.

  * •

We can assume an outer universe which classifies elements of
$\mathsf{Ty}_{0}\,\Gamma$. This amounts to reproducing the $\mathsf{Ty}_{0}$
_type_ from our 2LTT presentation, as an additional assumption. But in this
case, we might as well skip the two family structures and the $\Uparrow$
morphism.

In this thesis we make ubiquitous use of the outer universe of inner types, so
we choose that to be the primitive notion, instead of having two family
structures.

Do we lose anything by this? For the purposes of this thesis, not really.
However, if we want to implement 2LTT as a system for two-stage compilation,
the $\Uparrow$ syntax appears to be closer to existing systems. Staging is
about computing all outer redexes but no inner ones, thereby outputting syntax
which is purely in the inner theory. This could be implemented as a stage-
aware variant of normalization-by-evaluation [Abe13, AÖV18, WB18]. We can give
an intuitive staging interpretation for the operators in the $\Uparrow$
syntax:

  * •

$\Uparrow\\!A$ is the type of $A$-expressions. This corresponds to
$a\,\mathsf{code}$ in MetaOcaml [Kis14] and $\mathsf{TExp}\,a$ in typed
Template Haskell [XPL+22].

  * •

$\uparrow$ is _quoting_ , which creates an expression from any inner term.
This is $.\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rangle.$ in
MetaOCaml and $[||\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}||]$ in typed
Template Haskell.

  * •

$\downarrow$ is _splicing_ , which inserts the result of a meta-level
computation into an object-level expression. This is $\sim\\!(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})$ in MetaOCaml and $\$\$(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})$ in typed Template Haskell.

For example, in the $\Uparrow$ syntax, we might write a polymorphic identity
function which acts on inner types in two different ways:

$\displaystyle\mathsf{id}:(A:\mathsf{U}_{0})\to A\to A\hskip 20.00003pt$
$\displaystyle\mathsf{id}^{\prime}:(A:\,\Uparrow\\!\mathsf{U}_{0})\to\,\Uparrow\\!(\downarrow
A)\to\,\Uparrow\\!(\downarrow A)$
$\displaystyle\mathsf{id}:\equiv\lambda_{0}\,A\,x.\,x$
$\displaystyle\mathsf{id}^{\prime}:\equiv\lambda_{1}\,A\,x.\,x$

The first one lives in the inner family structure. The second one is the same
thing, but lifted to the outer theory. The choice between the two allows us to
control staging-time evaluation. If we write
$\mathsf{id}\,\mathsf{Bool}_{0}\,\mathsf{true}_{0}$, that is an inner
expression which goes into the staging output as it is. On the other hand,
$\downarrow(\mathsf{id}^{\prime}\,(\uparrow\,\mathsf{Bool}_{0})\,(\uparrow\,\mathsf{true}_{0}))$
reduces to $\downarrow(\uparrow\,\mathsf{true}_{0})$ which in turn reduces to
$\mathsf{true}_{0}$. The same choice can be expressed in our syntax as well:

$\displaystyle\mathsf{id}:\mathsf{Tm}_{0}\,((A:\mathsf{U}_{0})\to A\to
A)\hskip 20.00003pt$
$\displaystyle\mathsf{id}^{\prime}:(A:\mathsf{Tm}_{0}\,\mathsf{U}_{0})\to\,\mathsf{Tm}_{0}\,A\to\mathsf{Tm}_{0}\,A$
$\displaystyle\mathsf{id}:\equiv\lambda_{0}\,A\,x.\,x$
$\displaystyle\mathsf{id}^{\prime}:\equiv\lambda\,A\,x.\,x$

It remains to be checked which style is preferable in a staging
implementation. In the $\Uparrow$ style, the quoting and splicing operations
add noise to core syntax, but they are also mostly inferable during
elaboration, and they pack stage-changing information into $\uparrow$ and
$\downarrow$, thereby making it feasible to omit stage annotations in other
places in the core syntax. In the $\mathsf{Ty}_{0}$ style, we do not have
quote/splice, but we have to keep track of stages in all type/term formers. It
would be interesting to compare the two flavors in prototype implementations
of staged systems.

###  3.4 Presheaf Semantics of 2LTT

We review the standard semantics of 2LTT which we use in the rest of the
thesis. This justifies the metaprogramming view, that 2LTT allows meta-level
reasoning about an inner theory.

We present it in two steps, by assuming progressively more structure in the
inner theory. First, we only assume a category. This already lets us present a
presheaf semantics for the outer layer. Then, we assume a cwf as the inner
theory, which lets us interpret $\mathsf{Ty}_{0}$ and $\mathsf{Tm}_{0}$ and
also consider inner type formers.

####  3.4.1 Presheaf Model of the Outer Layer

In this subsection we present a presheaf model for the outer layer of 2LTT,
that is, the base category together with the terminal object, the
$(\mathsf{Ty},\,\mathsf{Tm})$ family and some type formers. This presheaf
semantics is well-known in the literature [Hof97]. We give a specification
which follows [Hub16] most closely.

In the following, we work outside 2LTT (since we are defining a model of
2LTT), in a suitable metatheory; an extensional type theory with enough
$\mathsf{Set}$ universes suffices.

We assume a $\mathbb{C}$ category. We write $i,\,j,\,k:|\mathbb{C}|$ for
objects and $f,\,g,\,h\,:\mathbb{C}(i,\,j)$ for morphisms. We use a different
notation than for cwfs before, in order to disambiguate components in
$\mathbb{C}$ from components in the presheaf model of 2LTT. We use
$\hat{\mathbb{C}}$ to refer to the model which is being defined. We use the
same component names for $\hat{\mathbb{C}}$ as in Section 3.2.

##### Model of cwf

######  Definition 23.

$\Gamma:\mathsf{Con}$ is a presheaf over $\mathbb{C}$. Its components are as
follows.

$\displaystyle|\Gamma|$ $\displaystyle:|\mathbb{C}|\to\mathsf{Set}$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rangle$
$\displaystyle:|\Gamma|\,j\to\mathbb{C}(i,\,j)\to|\Gamma|\,i$
$\displaystyle\gamma\langle\mathsf{id}\rangle$ $\displaystyle\equiv\gamma$
$\displaystyle\gamma\langle f\circ g\rangle$ $\displaystyle\equiv\gamma\langle
f\rangle\langle g\rangle$

We flip around the order of arguments in the action of $\Gamma$ on morphisms.
This is more convenient because of the contravariance; we can observe this in
the statement of preservation laws already. The action on morphisms is
sometimes called _restriction_.

######  Definition 24.

$\sigma:\mathsf{Sub}\,\Gamma\,\Delta$ is a natural transformation from
$\Gamma$ to $\Delta$. It has action $|\sigma|:|\Gamma|\,i\to|\Delta|\,i$, such
that $|\sigma|(\gamma\langle f\rangle)\equiv(|\sigma|\gamma)\langle f\rangle$.

######  Definition 25.

$A:\mathsf{Ty}\,\Gamma$ is a displayed presheaf over $\Gamma$. The “displayed”
here is used in exactly the same sense as in “displayed algebra” before. As we
will see in Chapter 4, presheaves can be specified with a signature, in which
case a presheaf is an algebra, and a displayed presheaf is a displayed
algebra. The definition here is equivalent to saying that $A$ is a presheaf
over the category of elements of $\Gamma$, but it is more convenient to use in
concrete definitions and calculations. The components of $A$ are as follows.

$\displaystyle|A|$ $\displaystyle:|\Gamma|\,i\to\mathsf{Set}$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rangle$
$\displaystyle:|A|\,\gamma\to(f:\mathbb{C}(i,\,j))\to|A|\,(\gamma\langle
f\rangle)$ $\displaystyle\alpha\langle\mathsf{id}\rangle$
$\displaystyle\equiv\alpha$ $\displaystyle\alpha\langle f\circ g\rangle$
$\displaystyle\equiv\alpha\langle f\rangle\langle g\rangle$

######  Definition 26.

$t:\mathsf{Tm}\,\Gamma\,A$ is a section of the displayed presheaf $A$. This is
again the same notion of section that we have seen before, instantiated for
presheaves.

$\displaystyle|t|:(\gamma:|\Gamma|\,i)\to|A|\,\gamma$
$\displaystyle|t|(\gamma\langle f\rangle)\equiv(|t|\gamma)\langle f\rangle$

######  Definition 27.

$\Gamma\triangleright A:\mathsf{Con}$ is the total presheaf of the displayed
presheaf $A$. Its action on objects and morphisms is the following.

$\displaystyle|\Gamma\triangleright A|$
$\displaystyle:\equiv(\gamma:|\Gamma|\,i)\times|A\,\gamma|$
$\displaystyle(\gamma,\,\alpha)\langle f\rangle$
$\displaystyle:\equiv(\gamma\langle f\rangle,\,\alpha\langle f\rangle)$

The $\mathsf{id}$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\circ\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ preservation
laws follow immediately.

######  Definition 28.

$A[\sigma]:\mathsf{Ty}\,\Gamma$ is defined as follows, assuming
$A:\mathsf{Ty}\,\Delta$ and $\sigma:\mathsf{Sub}\,\Gamma\,\Delta$.

$\displaystyle|A[\sigma]|\,\gamma$
$\displaystyle:\equiv|A|\,(|\sigma|\,\gamma)$ $\displaystyle\alpha\langle
f\rangle$ $\displaystyle:\equiv\alpha\langle f\rangle$

In the second component, we use $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\langle\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\\!\rangle$ for
$A$ on the right hand side. The definition is well-typed since
$|A|\,(|\sigma|\,(\gamma\langle
f\rangle))\equiv|A|\,((|\sigma|\,\gamma)\langle f\rangle)$ by the naturality
of $\sigma$. Functoriality follows from functoriality of $A$.

It is easy to check that the above definitions can be extended to a cwf.

  * •

For the base category, we take the category of presheaves.

  * •

The empty context $\scaleobj{.75}\bullet$ is the terminal presheaf, i.e. the
constantly $\top$ functor.

  * •

Type substitution is functorial, as it is defined as simple function
composition of actions on objects.

  * •

Term substitution is defined as composition of a section and a natural
transformation; and also functorial for the same reason.

  * •

Context comprehension structure follows from the $\Sigma$-based definition for
context extension.

##### Yoneda embedding

Before continuing with interpreting type formers in $\hat{\mathbb{C}}$, we
review the Yoneda embedding, as it is useful in subsequent definitions.

######  Definition 29.

The Yoneda embedding, denoted $\mathsf{y}$, is a functor from $\mathbb{C}$ to
the underlying category of $\hat{\mathbb{C}}$, defined as follows.

$\displaystyle\mathsf{y}:|\mathbb{C}|\to\mathsf{Con}\hskip 30.00005pt$
$\displaystyle\mathsf{y}:\mathbb{C}(i,\,j)\to\mathsf{Sub}\,(\mathsf{y}\,i)\,(\mathsf{y}\,j)$
$\displaystyle\mathsf{y}\,i:\equiv\mathbb{C}(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt},\,i)$ $\displaystyle|\mathsf{y}\,f|\,g:\equiv
f\circ g$

######  Lemma 1 (Yoneda lemma).

We have $\mathsf{Sub}\,(\mathsf{y}\,i)\,\Gamma\simeq|\Gamma|\,i$ as an
isomorphism of sets, natural in $i$ [ML98, Section III.2].

_Corollary._ If we choose $\Gamma$ to be $\mathsf{y}j$, it follows that
$\mathsf{Sub}\,(\mathsf{y}\,i)\,(\mathsf{y}\,j)\simeq\mathbb{C}(i,\,j)$, i.e.
that $\mathsf{y}$ is bijective on morphisms; hence it is an embedding.

######  Notation 9.

For $\gamma:|\Gamma|\,i$, we use $\gamma\langle\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\rangle:\mathsf{Sub}\,(\mathsf{y}\,i)\,\Gamma$ to
denote transporting right-to-left along the Yoneda lemma. In the other
direction we do not really need a notation, since from
$\sigma:\mathsf{Sub}\,(\mathsf{y}\,i)\,\Gamma$ we get
$|\sigma|\,\mathsf{id}:|\Gamma|\,i$.

##### Type formers

######  Definition 30.

Constant families are displayed presheaves which do not depend on their
context.

$\displaystyle\mathsf{K}$
$\displaystyle:\mathsf{Con}\to\\{\Gamma:\mathsf{Con}\\}\to\mathsf{Ty}\,\Gamma$
$\displaystyle|\mathsf{K}\,\Delta|\,\\{i\\}\,\gamma\,$
$\displaystyle:\equiv|\Delta|\,i$ $\displaystyle\delta\langle f\rangle$
$\displaystyle:\equiv\delta\langle f\rangle$

With this definition, we have
$\mathsf{Tm}\,\Gamma\,(\mathsf{K}\,\Delta)\equiv\mathsf{Sub}\,\Gamma\,\Delta$
so we have strict constant families.

######  Notation 10.

It is useful to consider any set as a constant presheaf, so given
$A:\mathsf{Set}$ we may write $A:\mathsf{Con}$ for the constant presheaf as
well.

######  Definition 31.

From any $A:\mathsf{Set}$, we get $\mathsf{K}\,A:\mathsf{Ty}\,\Gamma$. This
can be used to model negative or positive closed type formers. For example,
natural numbers are modeled as $\mathsf{K}\,\mathbb{N}$, Booleans as
$\mathsf{K}\,\mathsf{Bool}$, the unit type as $\mathsf{K}\,\top$, and so on.

######  Definition 32.

Coquand universes can be defined as follows. We write
$\mathsf{Set}_{\hat{\mathbb{C}}}$ for the outer universe in the model, to
distinguish it from the external $\mathsf{Set}$. Since the
$\mathsf{Set}_{\hat{\mathbb{C}}}$ is a non-dependent type, it is helpful to
define it as a $\mathsf{Set}_{\hat{\mathbb{C}}}:\mathsf{Con}$ such that
$\mathsf{Sub}\,\Gamma\,\mathsf{Set}_{\hat{\mathbb{C}}}\simeq\mathsf{Ty}\,\Gamma$.
The usual universe can be derived from this as
$\mathsf{K}\,\mathsf{Set}_{\hat{\mathbb{C}}}$. Again, we ignore size issues;
the fully formal definition would involve indexing constructions in
$\hat{\mathbb{C}}$ by universe levels.

We can take a hint from the Yoneda lemma. We aim to define
$|\mathsf{Set}_{\hat{\mathbb{C}}}|\,i$, but by the Yoneda lemma it is
isomorphic to $\mathsf{Sub}\,(\mathsf{y}i)\,\mathsf{Set}_{\hat{\mathbb{C}}}$.
However, by specification this should be isomorphic to
$\mathsf{Ty}\,(\mathsf{y}\,i)$, so we take this as definition:

$\displaystyle\mathsf{Set}_{\hat{\mathbb{C}}}$ $\displaystyle:\mathsf{Con}$
$\displaystyle|\mathsf{Set}_{\hat{\mathbb{C}}}|\,i$
$\displaystyle:\equiv\mathsf{Ty}\,(\mathsf{y}\,i)$ $\displaystyle A\langle
f\rangle$ $\displaystyle:\equiv A[\mathsf{y}f]$

In the $A\langle f\rangle$ definition, we substitute
$A:\mathsf{Ty}\,(\mathsf{y}\,i)$ with
$\mathsf{y}f:\mathsf{Sub}\,(\mathsf{y}j)\,(\mathsf{y}i)$ to get an element of
$\mathsf{Ty}\,(\mathsf{y}j)$. The required
$\mathsf{Sub}\,\Gamma\,\mathsf{Set}_{\hat{\mathbb{C}}}\simeq\mathsf{Ty}\,\Gamma$
is straightforward, so we omit the definition.

We note that Russell universes are not supported in the outer layer, as
$\mathsf{Sub}\,\Gamma\,\mathsf{Set}_{\hat{\mathbb{C}}}$ and
$\mathsf{Ty}\,\Gamma$ are not strictly the same, in particular they have a
different number of components as iterated $\Sigma$-types. Nevertheless, as we
mentioned in Section 3.3.2, we use Russell-style notation in the internal 2LTT
syntax, and assume that encoding/decoding is inserted by elaboration.

######  Definition 33.

$\Sigma$-types are defined pointwise. The definitions for pairing and
projections follow straightforwardly.

$\displaystyle\Sigma$
$\displaystyle:(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Ty}\,(\Gamma\triangleright
A)\to\mathsf{Ty}\,\Gamma$ $\displaystyle|\Sigma\,A\,B|\,\gamma$
$\displaystyle:\equiv(\alpha:|A|\,\gamma)\times|B|\,(\gamma,\,\alpha)$
$\displaystyle(\alpha,\,\beta)\langle f\rangle$
$\displaystyle:\equiv(\alpha\langle f\rangle,\,\beta\langle f\rangle)$

######  Definition 34.

We define $\Pi$-types in the following. This is a bit more complicated, so
first we look at the simpler case of presheaf exponentials. We source this
example from [MM12, Section I.]. The reader may refer to ibid. for an overview
of constructions in presheaf categories.

The exponential $\Delta^{\Gamma}:\mathsf{Con}$ is characterized by the
isomorphism
$\mathsf{Sub}\,(\Xi\otimes\Gamma)\,\Delta\,\simeq\,\mathsf{Sub}\,\Xi\,(\Delta^{\Gamma})$,
where we write $\otimes$ for the pointwise product of two presheaves. We can
again use the Yoneda lemma. We want to define $|\Delta^{\Gamma}|\,i$, but this
is isomorphic to $\mathsf{Sub}\,(\mathsf{y}i)\,(\Delta^{\Gamma})$, which
should be isomorphic to $\mathsf{Sub}\,(\mathsf{y}i\otimes\Gamma)\,\Delta$ by
the specification of exponentials. Hence:

$\displaystyle|\Delta^{\Gamma}|\,i$
$\displaystyle:\equiv\mathsf{Sub}\,(\mathsf{y}i\otimes\Gamma)\,\Delta$
$\displaystyle\sigma\langle f\rangle$
$\displaystyle:\equiv\sigma\circ(\mathsf{y}f\circ\mathsf{p},\,\mathsf{q})$

In the definition of presheaf restriction, we use $\mathsf{p}$, $\mathsf{q}$
as projections and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!,\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ as pairing for
$\otimes$. In short, $(\mathsf{y}f\circ\mathsf{p},\,\mathsf{q})$ is the same
as the morphism lifting from Definition 13: it weakens
$\mathsf{y}f:\mathsf{Sub}\,(\mathsf{y}j)\,(\mathsf{y}i)$ to
$\mathsf{Sub}\,(\mathsf{y}j\otimes\Gamma)\,(\mathsf{y}i\otimes\Gamma)$.

The dependently typed case follows the same pattern, except that we use
$\mathsf{Tm}$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\triangleright\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ instead
of $\mathsf{Sub}$ and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\otimes\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$. Additionally,
the action on objects depends on $\gamma:|\Gamma|\,i$, and we make use of
$\gamma\langle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\rangle\,\,:\mathsf{Sub}\,(\mathsf{y}i)\,\Gamma$ (introduced in Notation
9).

$\displaystyle\Pi$
$\displaystyle:(A:\mathsf{Ty}\,\Gamma)\to\mathsf{Ty}\,(\Gamma\triangleright
A)\to\mathsf{Ty}\,\Gamma$ $\displaystyle|\Pi\,A\,B|\,\\{i\\}\,\gamma$
$\displaystyle:\equiv\mathsf{Tm}\,(\mathsf{y}i\triangleright
A[\gamma\langle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\rangle])\,(B[\gamma\langle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\rangle\circ\,\mathsf{p},\,\mathsf{q}])$ $\displaystyle t\langle
f\rangle$ $\displaystyle:\equiv t[\mathsf{y}f\circ\mathsf{p},\,\mathsf{q}]$

Let us unfold the above definition a bit. Assuming
$t:|\Pi\,A\,B|\,\\{i\\}\,\gamma$, we have

$|t|:\\{j:|\mathbb{C}|\\}\to((f,\,\alpha):(f:\mathbb{C}(j,\,i))\times|A|\,(\gamma\langle
f\rangle))\to|B|\,(\gamma\langle f\rangle,\,\alpha)$

This is a bit clearer if we remove the $\Sigma$-type by currying.

$|t|:\\{j:|\mathbb{C}|\\}(f:\mathbb{C}(j,\,i))(\alpha:|A|\,(\gamma\langle
f\rangle))\to|B|\,(\gamma\langle f\rangle,\,\alpha)$

Restriction is functorial since it is defined as $\mathsf{Tm}$ substitution.
The definitions for $\mathsf{lam}$ and $\mathsf{app}$ are left to the reader.

######  Definition 35.

Extensional identity is defined as pointwise equality of sections:

$\displaystyle\mathsf{Id}:\mathsf{Tm}\,\Gamma\,A\to\mathsf{Tm}\,\Gamma\,A\to\mathsf{Ty}\,\Gamma$
$\displaystyle|\mathsf{Id}\,t\,u|\,\gamma:\equiv|t|\,\gamma\equiv|u|\,\gamma$

For the restriction operation, we have to show that
$|t|\,\gamma\equiv|u|\,\gamma$ implies $|t|\,(\gamma\langle
f\rangle)\equiv|u|\,(\gamma\langle f\rangle)$. This follows from congruence by
$\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\langle f\rangle$ and naturality
of $t$ and $u$. The defining
$(\mathsf{reflect},\,\mathsf{refl}):\mathsf{Tm}\,\Gamma\,(\mathsf{Id}\,t\,u)\simeq(t\equiv
u)$ isomorphism is evident from UIP and function extensionality for the
metatheoretic $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\\!\equiv\\!\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ relation.

####  3.4.2 Modeling the Inner Layer

We assume now that $\mathbb{C}$ is a cwf. We write types as
$a,\,b,\,c:\mathsf{Ty}_{\mathbb{C}}\,i$ and terms as
$t,\,u,\,v:\mathsf{Tm}_{\mathbb{C}}\,i\,a$. We reuse $\scaleobj{.75}\bullet$
for the terminal object and $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\triangleright\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ for context
extension, and likewise reuse notation for substitutions.

######  Definition 36 ($\mathsf{Ty}_{0}$, $\mathsf{Tm}_{0}$).

First, note that $\mathsf{Ty}_{\mathbb{C}}$ is a presheaf over $\mathbb{C}$,
and $\mathsf{Tm}_{\mathbb{C}}$ is a displayed presheaf over
$\mathsf{Ty}_{\mathbb{C}}$; this follows from the requirement that they form a
family structure over $\mathbb{C}$. Hence, in the presheaf model
$\mathsf{Ty}_{\mathbb{C}}$ is an element of $\mathsf{Con}$ and
$\mathsf{Tm}_{\mathbb{C}}$ is an element of
$\mathsf{Ty}\,\mathsf{Ty}_{\mathbb{C}}$. Also recall from Definition 30 that
$\mathsf{Tm}\,\Gamma\,(\mathsf{K}\,\Delta)\equiv\mathsf{Sub}\,\Gamma\,\Delta$.
With this is mind, we give the following definitions:

$\displaystyle\mathsf{Ty}_{0}:\mathsf{Ty}\,\Gamma$
$\displaystyle\mathsf{Tm}_{0}:\mathsf{Tm}\,\Gamma\,\mathsf{Ty}_{0}\to\mathsf{Ty}\,\Gamma$
$\displaystyle\mathsf{Ty}_{0}:\equiv\mathsf{K}\,\mathsf{Ty}_{\mathbb{C}}\hskip
20.00003pt$
$\displaystyle\mathsf{Tm}_{0}\,A:\equiv\mathsf{Tm}_{\mathbb{C}}[A]$

$\mathsf{Tm}_{\mathbb{C}}[A]$ is well-typed since
$A:\mathsf{Tm}\,\Gamma\,(\mathsf{K}\,\mathsf{Ty}_{\mathbb{C}})$, thus
$A:\mathsf{Sub}\,\Gamma\,\mathsf{Ty}_{\mathbb{C}}$. In other words, $A$ is a
natural transformation from $\Gamma$ to the presheaf of inner types.

##### Inner type formers

Can type formers in $(\mathsf{Ty}_{\mathbb{C}},\,\mathsf{Tm}_{\mathbb{C}})$ be
transferred to $(\mathsf{Ty}_{0},\,\mathsf{Tm}_{0})$ in the presheaf model of
2LTT? For example, if $\mathbb{C}$ supports $\mathsf{Bool}$, we would like to
model $\mathsf{Bool}_{0}$ in $\mathsf{Ty}_{0}$ as well. The following
explanation is adapted from Capriotti [Cap17, Section 2.3].

Generally, a type former in $\mathbb{C}$ transfers to $\hat{\mathbb{C}}$ if it
can be specified in the internal language of $\hat{\mathbb{C}}$. This is also
a core idea of HOAS: when working in $\hat{\mathbb{C}}$, everything is
natural, and we can omit boilerplate related to contexts and substitutions.
Recall from Section 3.3.2 the higher-order specification of inner functions:

$\displaystyle\Pi_{0}$
$\displaystyle:(A:\mathsf{Ty}_{0})\to(\mathsf{Tm}_{0}\,A\to\mathsf{Ty}_{0})\to\mathsf{Ty}_{0}$
$\displaystyle(\mathsf{app}_{0},\,\mathsf{lam}_{0})$
$\displaystyle:\mathsf{Tm}_{0}\,(\Pi_{0}\,A\,B)\simeq((a:\,\mathsf{Tm}_{0}\,A)\to\,\mathsf{Tm}_{0}\,(B\,a))$

We can say that this _defines_ what it means for $\mathbb{C}$ to support
$\Pi$. More precisely:

  * •

A type former in an object theory is specified with a closed type $A$ in a
2LTT.

  * •

A model of the object theory $\mathbb{C}$ supports a type former $A$ if there
is a global section of the $\hat{\mathbb{C}}$ interpretation of $A$.

  * •

Thus, if $\mathbb{C}$ supports a type former, it is immediate that the
specifying type is inhabited in $\hat{\mathbb{C}}$.

In this thesis we only mention type formers in type theories which can be
specified in such manner.

####  3.4.3 Functions With Inner Domains

There is a useful semantic simplification in the standard presheaf model, in
cases where we have functions of the form $\Pi\,(\mathsf{Tm}_{0}\,A)\,B$. This
greatly reduces encoding overhead when interpreting inductive signatures in
2LTT; we look at examples in Section 3.5. First we look at the simply-typed
case with presheaf exponentials.

######  Lemma 2.

$\mathsf{y}$ preserves finite products up to isomorphism, i.e.
$\mathsf{y}\scaleobj{.75}\bullet\simeq\scaleobj{.75}\bullet$ and
$\mathsf{y}(i\otimes j)\simeq(\mathsf{y}i\otimes\mathsf{y}j)$.

###### Proof.

$\mathsf{y}\scaleobj{.75}\bullet$ is $\mathbb{C}(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt},\,\scaleobj{.75}\bullet)$ by definition, which is
pointwise isomorphic to $\top$, hence isomorphic to
$\scaleobj{.75}\bullet\equiv\mathsf{K}\,\top$. $\mathsf{y}(i\otimes j)$ is
$\mathbb{C}(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\,i\otimes j)$, which
is isomorphic to $\mathsf{y}i\otimes\mathsf{y}j$ by the specification of
products. ∎

######  Lemma 3.

We have the following isomorphism.

$\displaystyle|\Gamma^{\mathsf{y}i}|\,j\equiv\hskip 30.00005pt$
$\displaystyle\mathsf{Sub}\,(\mathsf{y}j\otimes\mathsf{y}i)\,\Gamma\simeq\hskip
30.00005pt$ by product preservation
$\displaystyle\mathsf{Sub}\,(\mathsf{y}(j\otimes i))\,\Gamma\simeq\hskip
30.00005pt$ by Yoneda lemma $\displaystyle|\Gamma|\,(j\otimes i)$

It is possible to rephrase the above derivation for $\Pi$-types. For that, we
would need to define the action of $\mathsf{y}$ on types and terms, consider
the preservation of $\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\triangleright\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ by
$\mathsf{y}$, and also specify a “dependent” Yoneda lemma for $\mathsf{Tm}$.
For the sake of brevity, we omit this, and present the result directly:

$\displaystyle|\Pi\,(\mathsf{Tm}_{0}\,A)\,B|\,\\{i\\}\,\gamma\simeq|B|\,\\{i\triangleright|A|\,\gamma\\}\,(\gamma\langle\mathsf{p}\rangle,\,\mathsf{q})$

In short, depending on an inner domain is the same as depending on an extended
context in $\mathbb{C}$. We expand a bit on the typing of the right hand side.
We have $\gamma:|\Gamma|\,i$, moreover

$\displaystyle|B|$
$\displaystyle:\\{j:\mathbb{C}\\}\to|\Gamma\,\,\triangleright\mathsf{Tm}_{0}\,A|\,j\to\mathsf{Set}$
$\displaystyle|B|$
$\displaystyle:\\{j:\mathbb{C}\\}\to((\gamma^{\prime}:|\Gamma|\,j)\times\mathsf{Tm}_{\mathbb{C}}\,j\,(|A|\,\gamma^{\prime}))\to\mathsf{Set}$
$\displaystyle|B|\,\\{i\triangleright|A|\,\gamma\\}$
$\displaystyle:((\gamma^{\prime}:|\Gamma|\,(i\triangleright|A|\,\gamma))\times\mathsf{Tm}_{\mathbb{C}}\,(i\triangleright|A|\,\gamma)\,(|A|\,\gamma^{\prime}))\to\mathsf{Set}$
$\displaystyle\gamma\langle\mathsf{p}\rangle$
$\displaystyle:|\Gamma|\,(i\triangleright|A|\,\gamma)$
$\displaystyle\mathsf{q}$
$\displaystyle:\mathsf{Tm}_{\mathbb{C}}\,(i\triangleright|A|\,\gamma)\,((|A|\,\gamma)[\mathsf{p}])$
$\displaystyle\mathsf{q}$
$\displaystyle:\mathsf{Tm}_{\mathbb{C}}\,(i\triangleright|A|\,\gamma)\,(|A|\,(\gamma\langle\mathsf{p}\rangle))$

###  3.5 Simple Signatures in 2LTT

We revisit simple inductive signatures in this section, working internally to
2LTT. We review the concepts introduced in Chapter 2 in the same order.

######  Notation 11.

In this section we shall be fairly explicit about writing $\mathsf{Tm}_{0}$-s
and transporting along definitional isomorphisms. The simple setting makes it
feasible to be explicit; in later chapters we are more terse, as signatures
and semantics get more complicated.

####  3.5.1 Theory of Signatures

Signatures are defined exactly in the same way as before: we have
$\mathsf{Con}:\mathsf{Set}$, $\mathsf{Ty}:\mathsf{Set}$,
$\mathsf{Sub}:\mathsf{Con}\to\mathsf{Con}\to\mathsf{Set}$,
$\mathsf{Var}:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{Set}$ and
$\mathsf{Tm}:\mathsf{Con}\to\mathsf{Ty}\to\mathsf{Set}$. However, now by
$\mathsf{Set}$ we mean the outer universe of 2LTT. Thus signatures are
inductively defined in the outer layer.

####  3.5.2 Algebras

Again we compute algebras by induction on signatures, but now we use inner
types for carriers of algebras. We interpret types as follows:

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{A}:\mathsf{Ty}\to\mathsf{Ty}_{0}\to\mathsf{Set}$
$\displaystyle\iota^{A}\,$ $\displaystyle X:\equiv\mathsf{Tm}_{0}\,X$
$\displaystyle(\iota\to A)^{A}\,$ $\displaystyle X:\equiv\mathsf{Tm}_{0}\,X\to
A^{A}\,X$

Elsewhere, we change the type of the $X$ parameters accordingly:

$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$
$\displaystyle:\mathsf{Con}\to\mathsf{Ty}_{0}\to\mathsf{Set}$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$
$\displaystyle:\mathsf{Var}\,\Gamma\,A\to\\{X:\mathsf{Ty}_{0}\\}\to\Gamma^{A}\,X\to
A^{A}\,X$ $\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$
$\displaystyle:\mathsf{Tm}\,\Gamma\,A\to\\{X:\mathsf{Ty}_{0}\\}\to\Gamma^{A}\,X\to
A^{A}\,X$ $\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{A}$
$\displaystyle:\mathsf{Sub}\,\Gamma\,\Delta\to\\{X:\mathsf{Ty}_{0}\\}\to\Gamma^{A}\,X\to\Delta^{A}\,X$

We also define $\mathsf{Alg}\,\Gamma$ as
$(X:\mathsf{Ty}_{0})\times\Gamma^{A}\,X$.

######  Example 8.

Inside 2LTT we have the following:333Up to isomorphism, since we previously
defined $\Gamma^{A}$ as a function type instead of an iterated product type.

$\mathsf{Alg}\,\mathsf{NatSig}\equiv(X:\mathsf{Ty}_{0})\times(\mathit{zero}:\mathsf{Tm}_{0}\,X)\times(\mathit{suc}:\mathsf{Tm}_{0}\,X\to\mathsf{Tm}_{0}\,X)$

Then, we may assume any cwf $\mathbb{C}$, and interpret the above closed type
in the presheaf model $\hat{\mathbb{C}}$, and evaluate the result at
$\scaleobj{.75}\bullet$ and the unique element of the terminal presheaf
$\mathsf{K}\,\top$:

$|\mathsf{Alg}\,\mathsf{NatSig}|\,\\{\scaleobj{.75}\bullet\\}\,\mathsf{tt}:\mathsf{Set}$

We compute the definitions now. We use the simplified semantics for
$\mathit{suc}:\mathsf{Tm}_{0}\,X\to\mathsf{Tm}_{0}\,X$, since the function
domain is an inner type.

$|\mathsf{Alg}\,\mathsf{NatSig}|\,\\{\scaleobj{.75}\bullet\\}\,\mathsf{tt}\equiv(X:\mathsf{Ty}_{\mathbb{C}}\,\scaleobj{.75}\bullet)\times(\mathit{zero}:\mathsf{Tm}_{\mathbb{C}}\,\scaleobj{.75}\bullet\,X)\times(\mathit{suc}:\mathsf{Tm}_{\mathbb{C}}\,(\scaleobj{.75}\bullet\triangleright
X)\,X)$

Using the same computation, we get the following for binary trees:

$|\mathsf{Alg}\,\mathsf{TreeSig}|\,\\{\scaleobj{.75}\bullet\\}\,\mathsf{tt}\equiv(X:\mathsf{Ty}_{\mathbb{C}}\,\scaleobj{.75}\bullet)\times(\mathit{leaf}:\mathsf{Tm}_{\mathbb{C}}\,\scaleobj{.75}\bullet\,X)\times(\mathit{node}:\mathsf{Tm}_{\mathbb{C}}\,(\scaleobj{.75}\bullet\triangleright
X\triangleright X)\,X)$

We can also get internal algebras in any $\mathbb{C}$ category with finite
products because we can build cwfs from all such $\mathbb{C}$.

######  Definition 37.

Assuming $\mathbb{C}$ with finite products, we build a cwf by setting
$\mathsf{Con}:\equiv|\mathbb{C}|$, $\mathsf{Ty}\,\Gamma:\equiv|\mathbb{C}|$,
$\mathsf{Sub}\,\Gamma\,\Delta:\equiv\mathbb{C}(\Gamma,\,\Delta)$,
$\mathsf{Tm}\,\Gamma\,A:\equiv\mathbb{C}(\Gamma,\,A)$, $\Gamma\triangleright
A:\equiv\Gamma\otimes A$ and
$\scaleobj{.75}\bullet:\equiv\scaleobj{.75}\bullet_{\mathbb{C}}$. In short, we
build a non-dependent (simply-typed) cwf.

Now we can effectively interpret signatures in finite product categories. For
example:

$|\mathsf{Alg}\,\mathsf{NatSig}|\,\\{\scaleobj{.75}\bullet\\}\,\mathsf{tt}\equiv(X:|\mathbb{C}|)\times(\mathit{zero}:\mathbb{C}(\scaleobj{.75}\bullet,\,X))\times(\mathit{suc}:\mathbb{C}(\scaleobj{.75}\bullet\otimes
X,\,X))$

This is almost the same as what we would write by hand for the specification
of natural number objects; the only difference is the extra
$\scaleobj{.75}\bullet\otimes\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}$ in
$\mathit{suc}$.

####  3.5.3 Morphisms

We get an additional degree of freedom in the computation of morphisms:
preservation equations can be inner or outer. The former option is _weak_ or
_propositional_ preservation, while the latter is _strict_ preservation. In
the presheaf model of 2LTT, outer equality is definitional equality of inner
terms, while inner equality is propositional equality in the inner theory. Of
course, if the inner theory has extensional identity type, weak and strict
equations in 2LTT are equivalent for inner types. We compute weak preservation
for types as follows.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{M}:(A:\mathsf{Ty})\\{X_{0}\,X_{1}:\mathsf{Ty}_{0}\\}(X^{M}:\mathsf{Tm}_{0}\,X_{0}\to\mathsf{Tm}_{0}\,X_{1})\to
A^{A}\,X_{0}\to A^{A}\,X_{1}\to\mathsf{Set}$ $\displaystyle\iota^{M}\,$
$\displaystyle
X^{M}\,\alpha_{0}\,\,\alpha_{1}:\equiv\mathsf{Tm}_{0}\,(X^{M}\,\alpha_{0}=\alpha_{1})$
$\displaystyle(\iota\to A)^{M}\,$ $\displaystyle
X^{M}\,\alpha_{0}\,\,\alpha_{1}:\equiv(x:\mathsf{Tm}_{0}\,X_{0})\to
A^{M}\,X^{M}\,(\alpha_{0}\,x)\,(\alpha_{1}\,(X^{M}\,x))$

For strict preservation, we simply change
$\mathsf{Tm}_{0}\,(X^{M}\,\alpha_{0}=\alpha_{1})$ to
$X^{M}\,\alpha_{0}\equiv\alpha_{1}$. The definition of morphisms is the same
as before:

$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{M}:(\Gamma:\mathsf{Con}_{1})\\{X_{0}\,X_{1}:\mathsf{Ty}_{0}\\}\to(\mathsf{Tm}_{0}\,X_{0}\to\mathsf{Tm}_{0}\,X_{1})\to\Gamma^{A}\,X_{0}\to\Gamma^{A}\,X_{1}\to\mathsf{Set}$
$\displaystyle\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}:\equiv\\{A\\}(x:\mathsf{Var}_{1}\,\Gamma\,A)\to
A^{M}\,X^{M}\,(\gamma_{0}\,x)\,(\gamma_{1}\,x)$
$\displaystyle\mathsf{Mor}:\\{\Gamma:\mathsf{Con}_{1}\\}\to\mathsf{Alg}\,\Gamma\to\mathsf{Alg}\,\Gamma\to\mathsf{Set}$
$\displaystyle\mathsf{Mor}\,\\{\Gamma\\}\,(X_{0},\,\gamma_{0})\,(X_{1},\,\gamma_{1}):\equiv(X^{M}:\mathsf{Tm}_{0}\,X_{0}\to\mathsf{Tm}_{0}\,X_{1})\times\Gamma^{M}\,X^{M}\,\gamma_{0}\,\gamma_{1}$

We omit here the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{M}$ definitions
for terms and substitutions.

####  3.5.4 Displayed Algebras

We present $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{D}$ only for types
below.

$\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}^{D}:(A:\mathsf{Ty})\\{X\\}\to(\mathsf{Tm}_{0}\,X\to\mathsf{Ty}_{0})\to
A^{A}\,X\to\mathsf{Set}$ $\displaystyle\iota^{D}\,$ $\displaystyle
X^{D}\,\alpha:\equiv\mathsf{Tm}_{0}\,(X^{D}\,\alpha)$ $\displaystyle(\iota\to
A)^{D}\,$ $\displaystyle
X^{D}\,\alpha:\equiv(x:\mathsf{Tm}_{0}\,X)(x^{D}:\mathsf{Tm}_{0}\,(X^{D}\,x))\to
A^{D}\,X^{D}\,(\alpha\,x)$

Note that in the presheaf model, inhabitants of
$\mathsf{Tm}_{0}\,X\to\mathsf{Ty}_{0}$ are inner types depending on contexts
extended with the interpretation of $X$.

######  Example 9.

Assume a closed $(X,\,\mathit{zero},\,\mathit{suc})$ $\mathsf{Nat}$-algebra in
2LTT. We have the following computation:

$\mathsf{DispAlg}\,\\{\mathsf{NatSig}\\}\,(X,\,\mathit{zero},\,\mathit{suc})\equiv$
$\displaystyle(X^{D}$ $\displaystyle:\mathsf{Tm}_{0}\,X\to\mathsf{Ty}_{0})$
$\displaystyle\times\,$ $\displaystyle(\mathit{zero^{D}}$
$\displaystyle:\mathsf{Tm}_{0}\,(X^{D}\,\mathit{zero}))$
$\displaystyle\times\,$ $\displaystyle(\mathit{suc^{D}}$
$\displaystyle:(n:\mathsf{Tm}_{0}\,X)\to\mathsf{Tm}_{0}\,(X^{D}\,n)\to\mathsf{Tm}_{0}\,(X^{D}\,(\mathit{suc}\,n)))$

Let us look at the presheaf interpretation. We simplify functions with inner
domains everywhere. Also note that for
$\mathsf{suc}:\mathsf{Tm}_{0}\,X\to\mathsf{Tm}_{0}\,X$, we get
$|\mathsf{suc}|\,\mathsf{tt}:\mathsf{Tm}_{\mathbb{C}}\,(\scaleobj{.75}\bullet\triangleright
n:|X|\,\mathsf{tt})\,(|X|\,\mathsf{tt})$ in the semantics, so a
$\mathsf{suc}\,t$ application is translated as a substitution
$(|\mathsf{suc}|\,\mathsf{tt})[n\mapsto|t|\,\mathsf{tt}]$.

$|\mathsf{DispAlg}\,\\{\mathsf{NatSig}\\}\,(X,\,\mathit{zero},\,\mathit{suc})|\,\\{\scaleobj{.75}\bullet\\}\,\mathsf{tt}\equiv$
$\displaystyle(X^{D}$
$\displaystyle:\mathsf{Ty}_{\mathbb{C}}\,(\scaleobj{.75}\bullet\triangleright
n:|X|\,\mathsf{tt}))$ $\displaystyle\times\,$
$\displaystyle(\mathit{zero^{D}}$
$\displaystyle:\mathsf{Tm}_{\mathbb{C}}\,\scaleobj{.75}\bullet\,(X^{D}[n\mapsto|\mathit{zero}|\,\mathsf{tt}]))$
$\displaystyle\times\,$ $\displaystyle(\mathit{suc^{D}}$
$\displaystyle:\mathsf{Tm}_{\mathbb{C}}\,(\scaleobj{.75}\bullet\triangleright
n:|X|\,\mathsf{tt}\triangleright
n^{D}:X^{D}[n\mapsto|\mathit{zero}|\,\mathsf{tt}])\,(X^{D}[n\mapsto(|\mathit{suc}|\,\mathsf{tt})[n\mapsto
n]))$

To explain $(|\mathsf{suc}|\,\mathsf{tt})[n\mapsto n])$: we have
$\mathsf{suc}\,n$ in 2LTT, where $n$ is an inner variable, and in the presheaf
model inner variables become actual variables in the inner theory. Hence, we
map the $n$ which $\mathsf{suc}$ depends on to the concrete $n$ in the
context.

We can also interpret displayed algebras in finite product categories: