Eötvös Loránd University, Budapest,
Hungarybocquet@inf.elte.huhttps://orcid.org/0000-0001-6484-9570 Eötvös Loránd
University, Budapest,
Hungaryakaposi@inf.elte.huhttp://orcid.org/0000-0001-9897-8936 Supported by
the Bolyai Fellowship of the Hungarian Academy of Sciences and by the
“Application Domain Specific Highly Reliable IT Solutions” project of the
National Research, Development and Innovation Fund of Hungary, financed under
the Thematic Excellence Programme TKP2020-NKA-06 funding scheme. Chalmers
University of Technology,
Swedensattler@chalmers.sehttps://orcid.org/0000-0001-6374-4427 Rafaël Bocquet
and Ambrus Kaposi and Christian Sattler [500]Theory of computation Logic Type
theory Marco Gaboardi and Femke van Raamsdonk 2 8th International Conference
on Formal Structures for Computation and Deduction (FSCD 2023) FSCD 2023 FSCD
2023 July 3–6, 2023 Rome, Italy 260 14

# For the Metatheory of Type Theory, Internal Sconing Is Enough

Rafaël Bocquet  Ambrus Kaposi  Christian Sattler

###### Abstract

Metatheorems about type theories are often proven by interpreting the syntax
into models constructed using categorical gluing. We propose to use only
sconing (gluing along a global section functor) instead of general gluing. The
sconing is performed internally to a presheaf category, and we recover the
original glued model by externalization.

Our method relies on constructions involving two notions of models: first-
order models (with explicit contexts) and higher-order models (without
explicit contexts). Sconing turns a displayed higher-order model into a
displayed first-order model.

Using these, we derive specialized induction principles for the syntax of type
theory. The input of such an induction principle is a boilerplate-free
description of its motives and methods, not mentioning contexts. The output is
a section with computation rules specified in the same internal language. We
illustrate our framework by proofs of canonicity, normalization and syntactic
parametricity for type theory.

###### keywords:

type theory, presheaves, canonicity, normalization, sconing, gluing

###### category:

##  1 Introduction

The syntax of a type theory can be presented as the initial object in the
category of models of a generalized algebraic theory (GAT), i.e. as a quotient
inductive-inductive type (QIIT). Initiality provides an induction principle
for the syntax, namely the dependent eliminator of the QIIT. Metatheoretic
properties of the syntax, such as canonicity or normalization, can then be
proven by carefully constructing models of the theory displayed over the
syntax, or equivalently the motives and methods of the induction principle.
However, the presentation of the syntax as a QIIT includes an explicit
encoding of the substitution calculus of the theory; in particular every type
or term former comes with a substitution rule. If all of the components of a
complicated model are written explicitly, one has to prove that they all
respect substitution. More importantly, when working exclusively at this level
of generality, it is not easy to abstract the proof methods into reusable
theorems.

An alternative to the (first-order) genereralized algebraic presentation is to
present a type theory as a second-order or higher-order theory, for example by
using a Logical Framework [21] or Uemura’s representable map categories [38].
A higher-order presentation enables the use of higher-order abstract syntax
(HOAS), in which binders are encoded by metatheoretic functions. In practice,
this means that stability under substitution is implicit. Semantically, HOAS
admits an interpretation in the internal language of presheaf categories [23].
Within the internal language of a presheaf category, all constructions are
automatically stable under the morphisms of the base category.

In this work we propose an approach that combines the strengths of the first-
order and higher-order presentations. We consider two notions of models of a
type theory: first-order models correspond to the first-order presentation,
while higher-order models correspond to the higher-order presentation.
Typically, first-order models are categorical models of type theory
(categories with families equipped with additional structure), while higher-
order models are approximately universes closed under the type formers of the
theory. Both of these notions make sense both externally and in the internal
language of a presheaf category. We also have notions of displayed higher-
order and first-order models, corresponding to the motives and methods of
induction principles. We present a small number of constructions switching
between external, internal, first-order and higher-order models. Any of these
constructions is individually simple, but they can be composed to derive the
induction principles we need to prove metatheoretic results. The constructions
are listed below (FOM = first-order model, HOM = higher-order model). The
restriction and externalization operations can also be applied to displayed
first-order models and morphisms of first-order models.
Construction Input Output Internalization FOM $\mathcal{M}$ HOM $\mathbb{C}$
in $\mathbf{Psh}(\mathcal{M})$ $\mathbf{Set}$-contextualization HOM
$\mathbb{M}$ FOM $\mathbf{Set}_{\mathbb{M}}$ Telescopic contextualization HOM
$\mathbb{M}$ FOM $\mathbf{Tele}_{\mathbb{M}}$ Restriction Functor
$F:\mathcal{C}\to\mathcal{D}$, FOM $F^{\ast}(\mathcal{M})$ in
$\mathbf{Psh}(\mathcal{C})$ FOM $\mathcal{M}$ in $\mathbf{Psh}(\mathcal{D})$
Externalization FOM $\mathcal{M}$ in $\mathbf{Psh}(\mathcal{D})$ External FOM
$1_{\mathcal{D}}^{\ast}(\mathcal{M})$ $\mathbf{Scone}$-contextualization FOM
$\mathcal{M}$, Displayed FOM $\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ over
$\mathcal{M}$ Displayed HOM $\mathbb{M}^{\bullet}$ over $\mathcal{M}$

The most notable operations are the contextualizations111The word
contextualization reflects the fact that these operations make contexts
explicit. It is not related to the notion of contextual model., which turn
higher-order models into first-order models. The
$\mathbf{Set}$-contextualization generalizes the construction of a first-order
model from a universe; its underlying category is always the category of sets.
The telescopic contextualization is the contextual core of the
$\mathbf{Set}$-contextualization; it restricts the underlying category to a
category of telescopes. The $\mathbf{Scone}$-contextualization is a
generalization of the $\mathbf{Set}$-contextualization to displayed higher-
order and first-order models, which correspond to the motives and methods of
induction principles; its underlying category is always the Sierpinski cone,
also called scone, of some first-order model $\mathcal{M}$.

Our main observation is that sconing (that is
$\mathbf{Scone}$-contextualization) internally to a presheaf category
corresponds when viewed externally to a more complicated gluing construction.
For example, the normalization model from [13] can be recovered as the
externalization of the $\mathbf{Scone}$-contextualization of a displayed
higher-order model constructed in presheaves over the category of renamings.

The main intended application of these constructions is the statement and
proofs of relative induction principles. It is typically the case that the
result of induction over the syntax of type theory only holds over some of the
syntactic contexts, or is only stable under some of the syntactic
substitutions. For example, canonicity only holds over the empty context.
Normalization holds over every context, but is only stable under renamings.
This situation is described by a functor into the syntax
$F:\mathcal{R}\to\mathcal{S}$: the result of the induction should be stable
under the morphisms of $\mathcal{R}$. These functors are called “figure
shapes” by Sterling [34], they are also related to worlds in Twelf [31]. We
prove the relative induction principles for the following functors.

$\displaystyle 1_{\mathbf{Cat}}$ $\displaystyle{}\to{}$
$\displaystyle\mathcal{S}_{\mathcal{T}}$ Canonicity [13] (Theorem 4.1)
$\displaystyle\mathbf{Ren}_{\mathcal{S}}$ $\displaystyle{}\to{}$
$\displaystyle\mathcal{S}_{\mathcal{T}}$ Normalization [4, 13] (Theorem 5.3)
$\displaystyle\square$ $\displaystyle{}\to{}$
$\displaystyle\mathcal{S}_{\mathsf{CTT}}$ (Homotopy/strict) canonicity for
cubical type theory [14] (Theorem C.3) $\displaystyle\mathcal{A}_{\square}$
$\displaystyle{}\to{}$ $\displaystyle\mathcal{S}_{\mathsf{CTT}}$ Normalization
for cubical type theory [36] (Theorem C.7)

We also show how to prove canonicity and normalization by instantiating the
relative induction principles for
$1_{\mathbf{Cat}}\to\mathcal{S}_{\mathcal{T}}$ and
$\mathbf{Ren}_{\mathcal{S}}\to\mathcal{S}_{\mathcal{T}}$. We don’t prove
canonicity nor normalization for cubical type theory, but we expect that the
currently known proofs could be reformulated as instances of the relative
induction principles for $\square\to\mathcal{S}_{\mathsf{CTT}}$ and
$\mathcal{A}_{\square}\to\mathcal{S}_{\mathsf{CTT}}$.

Typically, the category $\mathcal{R}$ can be described as the initial object
of some category of structured categories. A relative induction principle with
respect to the functor $F$ is an induction principle that combines the
universal properties of $\mathcal{R}$ and $\mathcal{S}$. In our previous work
[10], the relative induction principles were stated in terms of the rather ad-
hoc notions of “displayed models without context extensions” and “relative
sections”. In the present work, the input of a relative induction principle is
a displayed higher-order model $\mathbb{S}^{\bullet}$, and the result is just
a (first-order) section ${\llbracket-\rrbracket}$ of
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$. The previous notion of “displayed
model without context extension” is recovered in the special case of displayed
higher-order models over $F^{\ast}(\mathbf{Tele}_{\mathbb{S}})$. The following
diagram illustrates the constructions involved in the statement and proof of a
relative induction principle ($F:\mathcal{R}\to\mathcal{S}$).
ExternalInternal to $\mathbf{Psh}(\mathcal{S})$Internal to
$\mathbf{Psh}(\mathcal{R})$First-orderHigher-
order$\mathcal{S}$$\mathbb{S}$$\mathbf{Tele}_{\mathbb{S}}$$F^{\ast}(\mathbf{Tele}_{\mathbb{S}})$$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$$\mathbb{S}^{\bullet}$Internalization
Telescopic contextualization Restriction  $\mathbf{Scone}$- contextualization

Both $\mathbb{S}^{\bullet}$ and $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ are
displayed over the internal first-order model
$F^{\ast}(\mathbf{Tele}_{\mathbb{S}})$.

${\mathbb{S}^{\bullet}}$${\mathbf{Scone}_{\mathbb{S}^{\bullet}}}$${F^{\ast}(\mathbf{Tele}_{\mathbb{S}})}$$\scriptstyle{{\llbracket-\rrbracket}}$

An important feature of our work is that the section ${\llbracket-\rrbracket}$
admits good computational behaviour, although we do not formally analyze this
behaviour. In fact, part of our understanding comes from looking at the
computational behaviour of the congruence operation $\mathsf{ap}$ in higher
observational type theory [33, 6], which is also a morphism of (first-order)
models internally to presheaves over the syntax of H.O.T.T.

### Related work

#### Logical relations and categorical gluing.

The initial motivation for this work was the understanding of algebraic and
reduction-free normalization proofs for dependent type theories. Variants of
categorical gluing were used to prove canonicity or normalization for simple
types [2, 16, 37], System F [3], and dependent types [4, 13, 15]. These can be
contrasted with reduction based normalization proofs such as [1, 32].

Logical relations were used to prove syntactic parametricity for type theory
[9, 5] and definability for simply typed lambda calculus [26]. It was shown
that categorical gluing generalizes both syntactic parametricity and
canonicity proofs [28].

#### Logical frameworks and higher-order abstract syntax.

Higher-order abstract syntax (HOAS) is the use of metatheoretic functions to
specify syntactic binders. Hofmann [23] has explained how HOAS can be
interpreted in the internal language of presheaf categories.

Uemura [38] has given a general definition of type theory based on these
ideas, which we will call second-order generalized algebraic theories
(SOGATs). It generalizes notions of second-order algebraic theories that have
been studied by Fiore and Mahmoud [17]. Harper presents an equational variant
of logical framework [20] for defining theories with bindings corresponding to
SOGATs. We believe that the constructions in our paper generalize to any
SOGAT. Gratzer and Sterling [19] propose using LCCCs to define higher order
theories (without representability conditions) which correspond to our higher
order models, but we also consider first order models.

#### Synthetic Tait computability.

Synthetic Tait computability (STC, [34, 35]) is an approach that relies on the
internal language of the Artin gluing of toposes, typically constructed by
gluing syntactic and semantic toposes. A pair of open/closed modalities can be
used to distinguish the syntactic and semantic parts in the internal language
of the Artin gluing. STC has been applied to proofs of normalization for
cubical type theory [36], multimodal type theory [18] and simplicial type
theory [39].

Both STC and our approach provide a synthetic setting for proofs of
metatheorems. Our approach is perhaps simpler in some aspects, e.g. we don’t
use any modalities and don’t need to use realignment; we acknowledge that this
is partly a matter of preference. The main advantage of our approach over STC
is that we have an internal specification of the result of an induction
principle.

In his thesis [34], Sterling briefly discusses the notion of Henkin model of a
higher-order theory. A Henkin model is a higher-order model with a non-
standard interpretation of the dependent products. We note that Henkin models
are closely related to first-order models: the Henkin models of a second-order
theory are equivalent to the democratic first-order models (this is [38,
Theorem 7.30]).

### Contributions

The main takeaway of this paper is that when using HOAS, we should not discard
the first order presentation, even in an internal setting. In particular, the
right notion of displayed higher-order model (input of an induction principle)
lies over a first-order model. The output of an induction principle is also a
section of first-order models, still internal.

The technical contributions are:

  * •

the relative induction principles which combine the initiality of the
underlying category and initiality of the syntax; we derive four such
induction principles;

  * •

the internalization, contextualization, externalization constructions which
let us formulate the relative induction principles;

  * •

the derivation of internal sections by analyzing the category of sections.

The main takeaway is supported by applications of the induction principles:
boilerplate-free proofs of canonicity, normalization and syntactic
parametricity. To our knowledge, this paper is the first defining the latter
in a synthetic setting. The fact that the notion of section is specified
internally has the feature that we can reuse it directly in subsequent
inductions. We exploit this in the proof of uniqueness of normal forms which
is proven in a separate step after normalization, relying on how the section
computes normal forms.

### Structure of the paper

In Section 2 we define first-order- and higher-order models of an example type
theory, and constructions relating them. In Section 3, we define displayed
higher order models which collect the motives and methods of an induction
principle. We also define sconing which turns a displayed higher order model
into its first order variant, also providing a notion of section. Then we move
on to applications: we prove canonicity in Section 4 using an induction
principle relative to the empty context (Theorem 4.1) which is a trivial
consequence of our previous definitions. In Section 5, we prove normalization
using an induction principle relative to renamings (Theorem 5.3). This
induction principle is proved using the methods described in Section 6.
Another application (syntactic parametricity) of Theorem 4.1 is described in
Appendix B, and the cubical variants of the above induction principles are
proven in Appendix C.

### Background

We assume some familiarity with the categorical semantics of type theory [11,
5] and with the use of extensional type theory as the internal language of
presheaf categories [22].

We use the notion of locally representable dependent presheaf to encode
context extensions (see Definition A.1). This definition is a more indexed
formulation of the notion of representable natural transformation, which was
used by Awodey to give an alternative definition of CwFs, known as natural
models [8].

##  2 First-order and higher-order models

Our running example is a minimal dependent type theory $\mathcal{T}$ with only
$\Pi$-types, but our constructions directly generalize to larger type
theories. Some other type theories are considered in the appendix, including
dependent type theories with universes and cubical type theories. We leave
generalization to arbitrary second-order generalized algebraic theories to
future work.

We define notions of higher-order and first-order models for $\mathcal{T}$. A
higher-order model is essentially a universe closed under dependent products,
while a first-order model is a category with families (CwF) equipped with
$\Pi$-types. The higher-order models are the models of some higher-order
theory $\mathcal{T}^{\mathsf{ho}}$ (a theory whose operations can have a
higher-order sort; classified by some locally cartesian closed category),
whereas the first-order models are the models of some (first-order)
essentially222The distinction between generalized algebraic theories and
essentially algebraic theories is not relevant in this paper. algebraic theory
$\mathcal{T}^{\mathsf{fo}}$ (a theory whose operations have a first-order
sort; classified by some finitely complete category).

###  2.1 Definitions

######  Definition 2.1.

A higher-order model of $\mathcal{T}$ consists of the following families and
operations:

$\displaystyle\mathsf{Ty}$ $\displaystyle:\mathrm{Set},$
$\displaystyle\mathsf{Tm}$ $\displaystyle:\mathsf{Ty}\to\mathrm{Set},$
$\displaystyle\Pi$
$\displaystyle:\forall(A:\mathsf{Ty})(B:\mathsf{Tm}(A)\to\mathsf{Ty})\to\mathsf{Ty},$
$\displaystyle\mathsf{app}$ $\displaystyle:\forall A\ B\
(f:\mathsf{Tm}(\Pi(A,B)))\ (a:\mathsf{Tm}(A))\to\mathsf{Tm}(B(a)),$
$\displaystyle\mathsf{lam}$ $\displaystyle:\forall A\ B\
(b:(a:\mathsf{Tm}(A))\to\mathsf{Tm}(B(a)))\to\mathsf{Tm}(\Pi(A,B)),$

subject to equations corresponding to the $\beta$\- and $\eta$-rules:
$\mathsf{lam}(\lambda a\mapsto\mathsf{app}(f,a))=f,$
$\mathsf{app}(\mathsf{lam}(b),a)=b(a).$

######  Definition 2.2.

A first-order model of $\mathcal{T}$ is a CwF $\mathcal{C}$ equipped with
$\Pi$-types.  $\lrcorner$

The notion of first-order model can be presented by a first-order generalized
algebraic theory $\mathcal{T}^{\mathsf{fo}}$. Equivalently, a first-order
model is a category $\mathcal{C}$ with a terminal object $1_{\mathcal{C}}$,
along with a (global) higher-order model $\mathbb{C}$ of $\mathcal{T}$ in
$\mathbf{Psh}(\mathcal{C})$ such that the dependent presheaf
$\mathbb{C}.\mathsf{Tm}$ is locally representable. The higher-order model
$\mathbb{C}$ is called the internalization of $\mathcal{C}$.

We use blackboard bold letters $\mathbb{M}$, $\mathbb{N}$, $\mathbb{C}$,
$\mathbb{S}$, $\mathbb{R}$, etc. to refer to higher-order models, and
calligraphic letters $\mathcal{M}$, $\mathcal{N}$, $\mathcal{C}$,
$\mathcal{S}$, $\mathcal{R}$, etc. to refer to first-order models. We try to
use the corresponding letter for the underlying internal higher-order model of
a first-order model, e.g. if $\mathcal{C}$ is an external first-order model,
we use $\mathbb{C}$ for its underlying internal higher-order model in
$\mathbf{Psh}(\mathcal{C})$. We denote the components of a model by
$\mathbb{C}.\mathsf{Ty}$, $\mathcal{C}.\mathsf{Tm}$, $\mathcal{C}.\Pi$, etc.

We write $\mathbf{Mod}_{\mathcal{T}}$ for the $1$-category of first-order
models of $\mathcal{T}$, and $\mathcal{S}_{\mathcal{T}}$ or just $\mathcal{S}$
for its initial object (the letter “S” standing for both syntax and
substitutions).

###  2.2 Contextualization

In general, we almost never want to construct all of the components of a
first-order model explicitly, because checking functoriality and naturality
conditions without relying on the internal language of a presheaf model is
tedious. For some models however, the functoriality and naturality conditions
hold trivially. This is the case for the “standard model” of type theory over
the category of sets: when defining this standard model in intensional type
theory, all naturality and functoriality conditions hold definitionally.

The construction of the standard model generalizes to the construction of a
first-order model from a higher-order model, which we now describe.

######  Construction 2.3 ($\mathbf{Set}$-Contextualization).

Let $\mathbb{M}$ be a higher-order model of $\mathcal{T}$. We construct a
first-order model $\mathbf{Set}_{\mathbb{M}}$, called the
$\mathbf{Set}$-contextualization of $\mathbb{M}$. Its underlying category is
the category $\mathbf{Set}$ of sets.

The types and terms of $\mathbf{Set}_{\mathbb{M}}$ are indexed families of
types and terms of $\mathbb{M}$:

  * •

A type over $\Gamma\in\mathbf{Set}$ is a function
$\Gamma\to\mathbb{M}.\mathsf{Ty}$.

  * •

Type substitution along a function $f:\Delta\to\Gamma$ is precomposition with
$f$.

  * •

A term of type $A:\Gamma\to\mathbb{M}.\mathsf{Ty}$ is a dependent function
$(\gamma:\Gamma)\to\mathbb{M}.\mathsf{Tm}(A(\gamma))$.

  * •

Term substitution along a function $f:\Delta\to\Gamma$ is precomposition with
$f$.

  * •

The functoriality of substitution is associativity of function composition.

The context extensions are given by dependent sums in $\mathbf{Set}$:

$\displaystyle(\Gamma.A)$ $\displaystyle\triangleq{}$
$\displaystyle(\gamma:\Gamma)\times\mathbb{M}.\mathsf{Tm}(A(\gamma)).$

The type-theoretic operations are all defined pointwise:

$\displaystyle\mathbf{Set}_{\mathbb{M}}.\Pi(\Gamma,A,B)$
$\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma\mapsto\mathbb{M}.\Pi(A(\gamma),\lambda a\mapsto
B(\gamma,a)),$
$\displaystyle\mathbf{Set}_{\mathbb{M}}.\mathsf{app}(\Gamma,f,a)$
$\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma\mapsto\mathbb{M}.\mathsf{app}(f(\gamma),a(\gamma)),$
$\displaystyle\mathbf{Set}_{\mathbb{M}}.\mathsf{lam}(\Gamma,b)$
$\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma\mapsto\mathbb{M}.\mathsf{lam}(\lambda a\mapsto
b(\gamma,a)).$

The $\beta$\- and $\eta$-rules for $\mathbf{Set}_{\mathbb{M}}$ hold as a
consequence of the corresponding rules for $\mathbb{M}$.

The naturality conditions are all trivial. For example, in the case of the
$\Pi$ type former, we have to check
$\Pi(\Gamma,A,B)[f]=\Pi(\Delta,A[f],B[f^{+}])$ for any $f:\Delta\to\Gamma$,
where $f^{+}(\gamma,a)=(f(\gamma),a)$. This amounts to checking the equality

$(\lambda\gamma\mapsto\mathbb{M}.\Pi(A(\gamma),\lambda a\mapsto
B(\gamma,a)))\circ f=(\lambda\gamma\mapsto\mathbb{M}.\Pi((A\circ
f)(\gamma),\lambda a\mapsto(B\circ f^{+})(\gamma,a))).\penalty
9999\hbox{}\nobreak\hfill\quad\hbox{$\lrcorner$}{}$

######  Remark 2.4.

Note that the underlying category $\mathbf{Set}$ of
$\mathbf{Set}_{\mathbb{M}}$ now has two CwF structures:

  * •

An _inner_ CwF structure, as defined in 2.3.

  * •

An _outer_ CwF structure, corresponding to the usual CwF structure on the
category of sets, modeling extensional type theory.

Together, they form a model of two-level type theory [7].

###  2.3 Telescopic contextualization

A first-order order model is said to be contextual when every object can be
uniquely written as an iterated context extension starting from the empty
context. The contextual first-order models form a coreflective subcategory
$\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}$ of $\mathbf{Mod}_{\mathcal{T}}$:
the inclusion
$\mathbf{Mod}_{\mathcal{T}}^{\mathsf{cxl}}\to\mathbf{Mod}_{\mathcal{T}}$ has a
right adjoint $\mathsf{cxl}$: the _contextual core_
$\mathsf{cxl}(\mathcal{C})$ has as objects the iterated context extensions of
$\mathcal{C}$, also known as telescopes, over the empty context.

######  Definition 2.5.

Let $\mathbb{M}$ be a higher-order model of $\mathcal{T}$. The telescopic
contextualization $\mathbf{Tele}_{\mathbb{M}}$ is the contextual core of the
$\mathbf{Set}$-contextualization $\mathbf{Set}_{\mathbb{M}}$.  $\lrcorner$

By general properties of the contextual core, there is a model morphism
${\lfloor-\rfloor}:\mathbf{Tele}_{\mathbb{M}}\to\mathbf{Set}_{\mathbb{M}}$
that is bijective on types and terms. (There is a cofibrantly generated
factorization system on first-order models with such morphisms as its right
class. The contextual models are precisely those in the left class.)

When working internally to some presheaf category $\mathbf{Psh}(\mathcal{C})$,
another related construction involves the internal subcategory spanned by
$\text{\char 136\relax}:\mathsf{Ob}_{\mathcal{C}}\to\mathrm{Set}$, where
$\mathsf{Ob}_{\mathcal{C}}$ is the discrete presheaf on the set of objects of
$\mathcal{C}$, and  internalizes the Yoneda embedding. This “Yoneda universe”
has been used by Hu et al. [24] to give semantics to contextual types.

###  2.4 Internal first-order models

Since the notion of first-order model is described by an essentially algebraic
theory, it can be interpreted in any finitely complete category. In
particular, there is a notion of internal first-order model in any category
$\widehat{\mathcal{C}}$ of small presheaves, obtained by letting
$\mathrm{Set}$ stand for the Hofmann-Streicher universe of the presheaf topos
$\mathbf{Psh}(\mathcal{C})$ in the definition of model.

######  Proposition 2.6.

The following three notions are equivalent:

  1. 1.

First-order models of $\mathcal{T}$ in $\mathbf{Psh}(\mathcal{C})$;

  2. 2.

Finite limit preserving functors
$\mathcal{T}^{\mathsf{fo}}\to\widehat{\mathcal{C}}$, where
$\mathcal{T}^{\mathsf{fo}}$ is the finitely complete category classifying the
first-order models of $\mathcal{T}$;

  3. 3.

Functors $\mathcal{C}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}$.

######  Proof 2.7.

This is well-known [25, D1.2.14]. The equivalence between (1) and (2) is the
fact that $\mathcal{T}^{\mathsf{fo}}$ classifies the first-order models of
$\mathcal{T}$. The equivalence between (2) and (3) follows from the fact that
finite limits in $\widehat{\mathcal{C}}$ are computed pointwise.

###  2.5 Restriction and externalization

Another important operation on first-order models is the restriction of a
first-order model $\mathcal{M}$ internal to $\mathbf{Psh}(\mathcal{D})$ along
a functor $F:\mathcal{C}\to\mathcal{D}$. This restricted model
$F^{\ast}(\mathcal{M})$ is a first-order model internal to
$\mathbf{Psh}(\mathcal{C})$. If $\mathcal{M}$ is seen as a functor
$\mathcal{D}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}$, then the restriction
$F^{\ast}(\mathcal{M}):\mathcal{C}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}$
is simply the precomposition $(\mathcal{M}\circ F)$. If $\mathcal{M}$ is seen
instead as a finite-limits preserving functor
$\mathcal{T}^{\mathsf{fo}}\to\mathbf{Psh}(\mathcal{D})$, then
$F^{\ast}(\mathcal{M})$ is postcomposition with the inverse image functor
$F^{\ast}:\mathbf{Psh}(\mathcal{D})\to\mathbf{Psh}(\mathcal{C})$. These two
definitions coincide up to the equivalence of Proposition 2.6; which is thus
natural in the base category.

######  Remark 2.8.

A more explicit computation of the restriction can be given in the internal
language of $\mathbf{Psh}(\mathcal{C})$ using the dependent right adjoint
associated to the adjunction $(F_{!}\dashv F^{\ast})$. When $\mathcal{M}$ is
the $\mathbf{Set}$\- or telescopic contextualization of a higher-order model,
then the dependent right adjoint allows for the use of HOAS when working with
$F^{\ast}(\mathcal{M})$.  $\lrcorner$

A special case of the restriction is the _externalization_ of an internal
first-order model.

######  Definition 2.9.

Let $\mathcal{C}$ be any category with a terminal object $1_{\mathcal{C}}$,
and consider the functor $1_{\mathcal{C}}:1_{\mathbf{Cat}}\to\mathcal{C}$ that
selects this terminal object. For any internal first-order model $\mathcal{M}$
in $\mathbf{Psh}(\mathcal{C})$, we have an external first-order model
$1_{\mathcal{C}}^{\ast}(\mathcal{M})$, called the externalization of
$\mathcal{M}$.  $\lrcorner$

Given any higher-order model $\mathbb{M}$ in $\mathbf{Psh}(\mathcal{C})$, we
can construct the externalization
$1_{\mathcal{C}}^{\ast}(\mathbf{Tele}_{\mathbb{M}})$ of its telescopic first-
order model. Up to isomorphism, all external contextual first-order models
arise as the externalization of a telescopic contextualization.

######  Lemma 2.10.

Let $\mathcal{C}$ be an external first-order model, with $\mathbb{C}$ its
underlying internal higher-order model. Then
$1_{\mathcal{C}}^{\ast}(\mathsf{Tele}_{\mathbb{C}})$ is the contextual core of
$\mathcal{C}$.

######  Proof 2.11.

See Corollary A.5.

In particular, since the initial model $\mathcal{S}$ is contextual, the
externalization $1_{\mathcal{S}}^{\ast}(\mathsf{Tele}_{\mathbb{S}})$ of its
telescopic contextualization is isomorphic to $\mathcal{S}$.

We can also construct the externalization
$1_{\mathcal{C}}^{\ast}(\mathbf{Set}_{\mathbb{C}})$ of the internal
$\mathbf{Set}$-contextualization of an higher-order model $\mathbb{C}$. The
underlying category of $1_{\mathcal{C}}^{\ast}(\mathbf{Set}_{\mathbb{C}})$ is
the category of presheaves over $\mathcal{C}$ (restricted to some universe
level); and $1_{\mathcal{C}}^{\ast}(\mathbf{Set}_{\mathbb{C}})$ is an external
model of two-level type theory (its underlying category is the restriction of
$\mathbf{Psh}(\mathcal{C})$ to some universe level). Recall that there is,
internally to $\mathbf{Psh}(\mathcal{C})$, a morphism
${\lfloor-\rfloor}:\mathbf{Tele}_{\mathbb{C}}\to\mathbf{Set}_{\mathbb{C}}$ of
first-order models. This morphism can also be externalized, giving an external
morphism
$1_{\mathcal{C}}^{\ast}({\lfloor-\rfloor}):1_{\mathcal{C}}^{\ast}(\mathsf{Tele}_{\mathbb{C}})\to
1_{\mathcal{C}}^{\ast}(\mathbf{Set}_{\mathbb{C}})$ of first-order models. When
$1_{\mathcal{C}}^{\ast}(\mathsf{Tele}_{\mathbb{C}})\cong\mathcal{C}$, this is
a simple construction of the embedding of $\mathcal{C}$ into the presheaf
model of two-level type theory.

##  3 Displayed higher-order models

###  3.1 Motives and methods

We now define the notion of displayed higher-order model, which collects the
motives and methods of induction principles. One could expect that a displayed
higher-order model would be displayed over a base higher-order model. We
instead define the notion of displayed higher-order model over a base first-
order model; it is always possible to turn higher-order models into first-
order models using a contextualization, but not every first-order model arises
in this way.

######  Definition 3.1.

Let $\mathcal{M}$ be a first-order model of $\mathcal{T}$. A displayed higher-
order model $\mathbb{M}^{\bullet}$ over $\mathcal{M}$ consists of the
following data:

$\displaystyle\mathsf{Ty}^{\bullet}$ $\displaystyle:{}$
$\displaystyle\mathcal{M}.\mathsf{Ty}(1_{\mathcal{M}})\to\mathrm{Set},$
$\displaystyle\mathsf{Tm}^{\bullet}$ $\displaystyle:{}$
$\displaystyle\forall(A:\mathcal{M}.\mathsf{Ty}(1_{\mathcal{M}}))\
(A^{\bullet}:\mathsf{Ty}^{\bullet}(A))\to\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},A)\to\mathrm{Set},$
$\displaystyle\Pi^{\bullet}$ $\displaystyle:{}$
$\displaystyle\forall(A:\mathcal{M}.\mathsf{Ty}(1_{\mathcal{M}}))\
(A^{\bullet}:\mathsf{Ty}^{\bullet}(A))$
$\displaystyle\phantom{\forall}(B:\mathcal{M}.\mathsf{Ty}(1_{\mathcal{M}}.A))\
(B^{\bullet}:\forall(a:\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},A))(a^{\bullet}:\mathsf{Tm}^{\bullet}(A^{\bullet},a))\to\mathsf{Ty}^{\bullet}(B[a]))$
$\displaystyle{}\to\mathsf{Ty}^{\bullet}(\Pi(A,B)),$
$\displaystyle\mathsf{app}^{\bullet}$ $\displaystyle:{}$ $\displaystyle\forall
A\ A^{\bullet}\ B\ B^{\bullet}\
(f:\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},\Pi(A,B)))\
(f^{\bullet}:\mathsf{Tm}^{\bullet}(\Pi^{\bullet}(A^{\bullet},B^{\bullet}),f))$
$\displaystyle\phantom{\forall}(a:\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},A))\
(a^{\bullet}:\mathsf{Tm}^{\bullet}(A^{\bullet},a))$
$\displaystyle{}\to\mathsf{Tm}^{\bullet}(B^{\bullet}(a^{\bullet}),\mathsf{app}(f,a)),$
$\displaystyle\mathsf{lam}^{\bullet}$ $\displaystyle:{}$ $\displaystyle\forall
A\ A^{\bullet}\ B\ B^{\bullet}\
(b:\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}}.(a:A),B[a]))$
$\displaystyle\phantom{\forall}(b^{\bullet}:\forall(a:\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},A))(a^{\bullet}:\mathsf{Tm}^{\bullet}(A^{\bullet},a))\to\mathsf{Tm}^{\bullet}(B^{\bullet}(a^{\bullet}),b[a]))$
$\displaystyle{}\to\mathsf{Tm}^{\bullet}(\Pi^{\bullet}(A^{\bullet},B^{\bullet}),\mathsf{lam}(b)),$

such that the following equalities hold:
$\mathsf{app}^{\bullet}(\mathsf{lam}^{\bullet}(b^{\bullet}),a^{\bullet})=b^{\bullet}(a^{\bullet}),$
$\mathsf{lam}^{\bullet}(\lambda
a^{\bullet}\mapsto\mathsf{app}^{\bullet}(f^{\bullet},a^{\bullet}))=f^{\bullet}.$

Most of the components of a displayed higher-order model only depend on the
closed types and terms of $\mathcal{M}$; only the binders need to refer to
open types and terms.

Note that the data of a displayed higher-order model over the terminal first-
order model is equivalent to the data of a non-displayed higher-order model.

###  3.2 Displayed contextualization

Given any displayed higher-order model $\mathbb{M}^{\bullet}$ over
$\mathcal{M}$, we construct a displayed first-order model over $\mathcal{M}$.
This construction is a displayed generalization of the
$\mathbf{Set}$-contextualization.

The underlying displayed category of this construction is the _Sierpinski
cone_ , or scone, of $\mathcal{M}$. The scone of a category $\mathcal{C}$ with
a terminal object is the comma category
$(\mathbf{Set}\downarrow\Gamma_{\mathcal{C}})$, where
$\Gamma_{\mathcal{C}}:\mathcal{C}\to\mathbf{Set}$ is the global section
functor $\Gamma_{\mathcal{C}}=\mathcal{C}(1_{\mathcal{C}},-)$.

######  Construction 3.2 (Displayed contextualization).

Fix a displayed higher-order model $\mathbb{M}^{\bullet}$ over a first-order
model $\mathcal{M}$. We construct a displayed first-order model
$\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ over $\mathcal{M}$, called the
displayed contextualization of $\mathbb{M}^{\bullet}$.

  * •

An object of $\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ over
$\Gamma\in\mathcal{M}$ is a family

$\Gamma^{\dagger}:\mathcal{M}(1_{\mathcal{M}},\Gamma)\to\mathrm{Set}$

over the global elements (i.e. closing substitutions) of $\Gamma$.

  * •

A morphism of $\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ from $\Gamma^{\dagger}$
to $\Delta^{\dagger}$ over a base morphism $f:\mathcal{M}(\Gamma,\Delta)$ is a
family

$f^{\dagger}:\forall(\gamma:\mathcal{M}(1_{\mathcal{M}},\Gamma))\to\Gamma^{\dagger}(\gamma)\to\Delta^{\dagger}(f\circ\gamma).$

The identity displayed morphism is given by

$\mathsf{id}^{\dagger}\triangleq\lambda\gamma\
\gamma^{\bullet}\mapsto\gamma^{\bullet},$

whereas the composition of two displayed morphisms $f^{\dagger}$ and
$g^{\dagger}$ is

$f^{\dagger}\circ^{\dagger}g^{\dagger}\triangleq\lambda\gamma\
\gamma^{\bullet}\mapsto f^{\dagger}(g^{\dagger}(\gamma^{\bullet})).$

  * •

A type of $\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ over an object
$\Gamma^{\dagger}$ and a type $A:\mathcal{M}.\mathsf{Ty}(\Gamma)$ is a
function

$A^{\dagger}:\forall\gamma\
(\gamma^{\dagger}:\Gamma^{\dagger}(\gamma))\to\mathsf{Ty}^{\bullet}(A[\gamma]).$

The restriction of $A^{\dagger}$ along a displayed morphism $f^{\dagger}$ is

$A^{\dagger}[f^{\dagger}]\triangleq\lambda\gamma^{\bullet}\mapsto
A^{\dagger}(f^{\dagger}(\gamma^{\bullet})).$

  * •

A term of $\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ of type $A^{\dagger}$ over
an object $\Gamma^{\dagger}$ and a term $a:\mathcal{M}.\mathsf{Tm}(\Gamma,A)$
is a function

$a^{\dagger}:\forall\gamma\
(\gamma^{\bullet}:\Gamma^{\dagger}(\gamma))\to\mathsf{Tm}^{\bullet}(A^{\dagger}(\gamma^{\bullet}),a[\gamma]).$

The restriction of $a^{\dagger}$ along a displayed morphism $f^{\dagger}$ is

$a^{\dagger}[f^{\dagger}]\triangleq\lambda\gamma^{\bullet}\mapsto
a^{\dagger}(f^{\dagger}(\gamma^{\bullet})).$

  * •

The empty displayed context is the family

$1^{\dagger}\triangleq\lambda\\_\mapsto\mathbf{1}.$

  * •

The extension of a displayed context $\Gamma^{\dagger}$ by a displayed type
$A^{\dagger}$ is the family

$(\Gamma^{\dagger}.A^{\dagger})\triangleq\lambda{\left\langle\gamma,a\right\rangle}\mapsto(\gamma^{\bullet}:\Gamma^{\dagger}(\gamma))\times
A^{\dagger}(\gamma^{\bullet},a).$

  * •

All type- and term- formers are defined pointwise using the corresponding
component of $\mathbb{M}^{\bullet}$:

$\displaystyle\Pi^{\dagger}(A^{\dagger},B^{\dagger})$
$\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma^{\bullet}\mapsto\Pi^{\bullet}(A^{\dagger}(\gamma^{\bullet}),\lambda
a^{\bullet}\mapsto B^{\dagger}(\gamma^{\bullet},a^{\bullet})),$
$\displaystyle\mathsf{app}^{\dagger}(f^{\dagger},a^{\dagger})$
$\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma^{\bullet}\mapsto\mathsf{app}^{\bullet}(f^{\dagger}(\gamma^{\bullet}),a^{\dagger}(\gamma^{\bullet})),$
$\displaystyle\mathsf{lam}^{\dagger}(b^{\dagger})$ $\displaystyle\triangleq{}$
$\displaystyle\lambda\gamma^{\bullet}\mapsto\mathsf{lam}^{\bullet}(\lambda
a^{\bullet}\mapsto b^{\dagger}(\gamma^{\bullet},a^{\bullet})).$

  * •

The $\beta$\- and $\eta$-rules hold as a consequence of the $\beta$\- and
$\eta$-rules of $\mathbb{M}^{\bullet}$.

  * •

All naturality conditions are trivial.  $\lrcorner$

Note that when $\mathbb{M}$ is a higher-order model seen as a displayed
higher-order model over the terminal first-order model, then
$\mathbf{Scone}_{\mathbb{M}}$ is equivalent to $\mathbf{Set}_{\mathbb{M}}$.

###  3.3 Sections of a displayed higher-order model

The notion of displayed higher-order model corresponds to the motives and
methods of an induction principle. We now define the notion of section of a
displayed higher-order model, corresponding to the result of applying an
induction principle: it is simply defined as a section of the displayed
contextualization.

######  Definition 3.3.

A section of a displayed higher-order model $\mathbb{M}^{\bullet}$ is a
section ${\llbracket-\rrbracket}$ of its displayed contextualization
$\mathbf{Scone}_{\mathbb{M}^{\bullet}}$ (in $\mathbf{Mod}_{\mathcal{T}}$).
$\lrcorner$

The definition of section of a displayed higher-order model
$\mathbb{M}^{\bullet}$ over $\mathcal{M}$ can be unfolded to the following
components:

  * •

For every object $\Gamma:\mathcal{M}$, a family

${\llbracket\Gamma\rrbracket}:\mathcal{M}(1_{\mathcal{M}},\Gamma)\to\mathbf{Set}$

of _environments_.

  * •

For every morphism $f:\mathcal{M}(\Gamma,\Delta)$, a family

${\llbracket
f\rrbracket}:\forall\gamma\to{\llbracket\Gamma\rrbracket}(\gamma)\to{\llbracket\Delta\rrbracket}(f\circ\gamma)$

of maps between environments.

  * •

For every type $A:\mathcal{M}.\mathsf{Ty}(\Gamma)$, a family

${\llbracket A\rrbracket}:\forall\gamma\
(\gamma^{\bullet}:{\llbracket\Gamma\rrbracket}(\gamma))\to\mathsf{Ty}^{\bullet}(A[\gamma])$

of displayed types over closures of $A$.

  * •

For every term $a:\mathcal{M}.\mathsf{Tm}(\Gamma,A)$, a family

${\llbracket a\rrbracket}:\forall\gamma\
(\gamma^{\bullet}:{\llbracket\Gamma\rrbracket}(\gamma))\to\mathsf{Tm}^{\bullet}({\llbracket
A\rrbracket}(\gamma^{\bullet}),a[\gamma])$

of displayed terms over closures of $a$.

  * •

Subject to functoriality and naturality equations:

$\displaystyle{\llbracket\mathsf{id}\rrbracket}(\gamma^{\bullet})=\gamma^{\bullet},$
$\displaystyle{\llbracket f\circ g\rrbracket}(\gamma^{\bullet})={\llbracket
f\rrbracket}({\llbracket g\rrbracket}(\gamma^{\bullet})),$
$\displaystyle{\llbracket A[f]\rrbracket}(\gamma^{\bullet})={\llbracket
A\rrbracket}({\llbracket f\rrbracket}(\gamma^{\bullet})),$
$\displaystyle{\llbracket a[f]\rrbracket}(\gamma^{\bullet})={\llbracket
A\rrbracket}({\llbracket f\rrbracket}(\gamma^{\bullet})).$

  * •

Such that context extensions are preserved:

$\displaystyle{\llbracket 1_{\mathcal{M}}\rrbracket}(\star)=\\{\star\\},$
$\displaystyle{\llbracket\Gamma.A\rrbracket}(\gamma,a)=(\gamma^{\bullet}:{\llbracket\Gamma\rrbracket}(\gamma))\times(a^{\bullet}:\mathsf{Tm}^{\bullet}({\llbracket
A\rrbracket}(\gamma^{\bullet}),a)),$
$\displaystyle{\llbracket\lambda\gamma\mapsto(\delta(\gamma),a(\gamma))\rrbracket}(\gamma)=({\llbracket\delta\rrbracket}(\gamma),{\llbracket
a\rrbracket}(\gamma)).$

  * •

With computation rules for every type and term former:

$\displaystyle{\llbracket\lambda\gamma\mapsto\Pi(A(\gamma),\lambda a\mapsto
B(\gamma,a))\rrbracket}(\gamma^{\bullet})=\Pi^{\bullet}({\llbracket
A\rrbracket}(\gamma^{\bullet}),\lambda a^{\bullet}\mapsto{\llbracket
B\rrbracket}(\gamma^{\bullet})),$
$\displaystyle{\llbracket\lambda\gamma\mapsto\mathsf{app}(f(\gamma),a(\gamma))\rrbracket}(\gamma^{\bullet})=\mathsf{app}^{\bullet}({\llbracket
f\rrbracket}(\gamma^{\bullet}),{\llbracket a\rrbracket}(\gamma^{\bullet})),$
$\displaystyle{\llbracket\lambda\gamma\mapsto\mathsf{lam}(b(\gamma))\rrbracket}(\gamma^{\bullet})=\mathsf{lam}^{\bullet}(\lambda
a^{\bullet}\mapsto{\llbracket b\rrbracket}(\gamma^{\bullet},a^{\bullet})).$

When $x$ is a closed type or term of $\mathcal{M}$, we write ${\llbracket
x\rrbracket}$ for the interpretation ${\llbracket x\rrbracket}(\star)$ of $x$
in the empty environment. We may use underlined names to distinguish the
variable of open terms. For instance, we may write
${\llbracket\mathsf{app}(\underline{f},\underline{a})\rrbracket}[\underline{f}\mapsto
f^{\prime},\underline{a}\mapsto a^{\prime}]$ instead of
${\llbracket\lambda(f,a)\mapsto\mathsf{app}(f,a)\rrbracket}(f^{\prime},a^{\prime})$.

######  Remark 3.4.

Let $\mathbb{S}^{\bullet}$ be a displayed higher-order model over the first-
order model $F^{\ast}(\mathsf{Tele}_{\mathbb{S}})$ in
$\mathbf{Psh}(\mathcal{C})$, for some functor $F:\mathcal{C}\to\mathcal{S}$.
The displayed contextualization $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ is a
displayed first-order model over $F^{\ast}(\mathsf{Tele}_{\mathbb{S}})$. Then
its externalization
$1^{\ast}_{\mathcal{C}}(\mathbf{Scone}_{\mathbb{S}^{\bullet}})$ is an external
displayed first-order model lying over
$1^{\ast}_{\mathcal{C}}(F^{\ast}(\mathsf{Tele}_{\mathbb{S}}))=1^{\ast}_{\mathcal{S}}(\mathsf{Tele}_{\mathbb{S}})$.
Up to the isomorphism
$1^{\ast}_{\mathcal{S}}(\mathsf{Tele}_{\mathbb{S}})\cong\mathcal{S}$, the
externalized $\mathbf{Scone}$-contextualization
$1^{\ast}_{\mathcal{C}}(\mathbf{Scone}_{\mathbb{S}^{\bullet}})$ coincides with
gluing. Its underlying category is the comma category $(\mathcal{S}\downarrow
N_{F})$, where $N_{F}:\mathcal{S}\to\mathbf{Psh}(\mathcal{C})$ is the nerve
functor $\mathcal{S}\xrightarrow{\text{\char
136\relax}}\mathbf{Psh}(\mathcal{S})\xrightarrow{F^{\ast}}\mathbf{Psh}(\mathcal{C})$.
$\lrcorner$

##  4 Example: canonicity proof

As a first example of a relative induction principle and its application, we
prove canonicity for $\mathcal{T}$ extended with booleans (given by a type
former $\mathsf{Bool}$ with constructors $\mathsf{true}$ and $\mathsf{false}$
and a dependent eliminator $\mathsf{elim}_{\mathsf{Bool}}$ with two
computation rules).

We use the induction principle relative to the functor
$1_{\mathcal{S}}:1_{\mathbf{Cat}}\to\mathcal{S}$ that selects the terminal
object in the syntax $\mathcal{S}$. It turns out that proving this specific
relative induction principle is trivial.

######  Theorem 4.1 (Induction principle for $\mathbb{S}$ relative to
$1_{\mathcal{S}}:1_{\mathbf{Cat}}\to\mathcal{S}$).

Let $\mathbb{S}^{\bullet}$ be a displayed higher-order model over the initial
model $\mathcal{S}$, or equivalently over
$1_{\mathcal{S}}^{\ast}(\mathsf{Tele}_{\mathbb{S}})$. Then
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ admits a section
${\llbracket-\rrbracket}$ over $\mathcal{S}$.

######  Proof 4.2.

By initiality of $\mathcal{S}$.

We now construct the displayed higher-order model $\mathbb{S}^{\bullet}$ over
$1_{\mathcal{S}}^{\ast}(\mathsf{Tele}_{\mathbb{S}})$ that will be used to
prove canonicity. A displayed type $A^{\bullet}$ over a closed type
$A:\mathcal{S}.\mathsf{Ty}(1_{\mathcal{S}})$ is a $\mathrm{Set}$-valued
logical predicate over the closed terms of type $A$:

$\mathsf{Ty}^{\bullet}(A)\triangleq\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},A)\to\mathrm{Set}.$

A displayed term $a^{\bullet}$ of type $A^{\bullet}$ over a closed term
$a:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},A)$ is an element of the logical
predicate $A^{\bullet}$ evaluated at $a$:

$\mathsf{Tm}^{\bullet}(A^{\bullet},a)\triangleq A^{\bullet}(a).$

Given logical predicates $A^{\bullet}$ and $B^{\bullet}$, the logical
predicate $\Pi^{\bullet}(A^{\bullet},B^{\bullet})$ expresses the fact that
functions $f:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},\Pi(A,B))$ should
preserve the logical predicates.

$\displaystyle\Pi^{\bullet}(A^{\bullet},B^{\bullet})$
$\displaystyle\triangleq{}$
$\displaystyle\lambda(f:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},\Pi(A,B)))\mapsto(\forall
a\ a^{\bullet}\to B^{\bullet}(a^{\bullet},\mathsf{app}(f,a))),$
$\displaystyle\mathsf{app}^{\bullet}(f^{\bullet},a^{\bullet})$
$\displaystyle\triangleq{}$ $\displaystyle f^{\bullet}(a^{\bullet}),$
$\displaystyle\mathsf{lam}^{\bullet}(b^{\bullet})$ $\displaystyle\triangleq{}$
$\displaystyle\lambda a^{\bullet}\mapsto b^{\bullet}(a^{\bullet}).$

It is easy to check that the displayed $\beta$\- and $\eta$-rules hold. The
logical predicate
$\mathsf{Bool}^{\bullet}:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},\mathsf{Bool})\to\mathrm{Set}$
is defined as an inductive family with two constructors
$\mathsf{true}^{\bullet}:\mathsf{Bool}^{\bullet}(\mathsf{true})$ and
$\mathsf{false}^{\bullet}:\mathsf{Bool}^{\bullet}(\mathsf{false})$. The
displayed eliminator $\mathsf{elim}_{\mathsf{Bool}}^{\bullet}$ is defined
using the elimination principle of $\mathsf{Bool}^{\bullet}$ and the displayed
$\beta$-laws hold. This concludes the definition of all components of
$\mathbb{S}^{\bullet}$.

######  Theorem 4.3.

The initial model $\mathbb{S}$ satisfies canonicity: any closed boolean term
$b:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},\mathsf{Bool})$ is canonical, i.e.
equal to exactly one of $\mathsf{true}$ or $\mathsf{false}$.

######  Proof 4.4.

By the relative induction principle Theorem 4.1, the displayed higher-order
model $\mathbb{S}^{\bullet}$ admits a section ${\llbracket-\rrbracket}$. Now
given a closed boolean term
$b:\mathcal{S}.\mathsf{Tm}(1_{\mathcal{S}},\mathsf{Bool})$, we have
${\llbracket
b\rrbracket}:\mathsf{Tm}^{\bullet}({\llbracket\mathsf{Bool}\rrbracket},b)$. By
the computation rule of the section for $\mathsf{Bool}$,
$\mathsf{Tm}^{\bullet}({\llbracket\mathsf{Bool}\rrbracket},b)=\mathsf{Bool}^{\bullet}(b)$.
Thus, ${\llbracket b\rrbracket}:\mathsf{Bool}^{\bullet}(b)$ witnesses the fact
that $b$ is canonical.

Since ${\llbracket\mathsf{true}\rrbracket}=\mathsf{true}^{\bullet}$,
${\llbracket\mathsf{false}\rrbracket}=\mathsf{false}^{\bullet}$ and
$\mathsf{true}^{\bullet}\neq\mathsf{false}^{\bullet}$, we know that
$\mathsf{true}\neq\mathsf{false}$.

Note that in the canonicity proof, we have not needed to evaluate the section
${\llbracket-\rrbracket}$ on non-closed types or terms. Evaluating the section
on open types and terms is usually only needed when encountering binders: the
evaluation of the section on a closed binder depends on the evaluation of the
section on an open type or term. The following is an example of the
computation of the evaluation of the section ${\llbracket-\rrbracket}$ on the
application of the boolean negation function $\mathsf{lam}(\lambda
b\mapsto\mathsf{elim}_{\mathsf{Bool}}(\mathsf{Bool},\mathsf{false},\mathsf{true},b))$
to $\mathsf{true}$.

$\displaystyle{\llbracket\mathsf{app}(\mathsf{lam}(\lambda
b\mapsto\mathsf{elim}_{\mathsf{Bool}}(\mathsf{Bool},\mathsf{false},\mathsf{true},b)),\mathsf{true})\rrbracket}$
$\displaystyle\quad={\llbracket\mathsf{lam}(\lambda
b\mapsto\mathsf{elim}_{\mathsf{Bool}}(\mathsf{Bool},\mathsf{false},\mathsf{true},b))\rrbracket}({\llbracket\mathsf{true}\rrbracket})$
$\displaystyle\quad=(\lambda
b^{\bullet}\mapsto{\llbracket\mathsf{elim}_{\mathsf{Bool}}(\mathsf{Bool},\mathsf{false},\mathsf{true},\underline{b})\rrbracket}[\underline{b}\mapsto
b^{\bullet}])(\mathsf{true}^{\bullet})$
$\displaystyle\quad={\llbracket\mathsf{elim}_{\mathsf{Bool}}(\mathsf{Bool},\mathsf{false},\mathsf{true},\underline{b})\rrbracket}[\underline{b}\mapsto\mathsf{true}^{\bullet}]$
$\displaystyle\quad=\mathsf{elim}_{\mathsf{Bool}}^{\bullet}(\mathsf{Bool}^{\bullet},\mathsf{false}^{\bullet},\mathsf{true}^{\bullet},\mathsf{true}^{\bullet})$
$\displaystyle\quad=\mathsf{false}^{\bullet}.$

##  5 Example: normalization proof

In this section we prove normalization for the initial model $\mathcal{S}$ of
$\mathcal{T}$ using an induction principle relative to
$F:\mathbf{Ren}_{\mathcal{S}}\to\mathcal{S}$, where
$\mathbf{Ren}_{\mathcal{S}}$ is the category of renamings of $\mathcal{S}$,
i.e. the category whose morphisms are the substitutions of $\mathcal{S}$ that
are built out of variables. We use the alternative definition from [10] of
$\mathbf{Ren}_{\mathcal{S}}$ as the initial object in a category of first-
order renaming algebras.

###  5.1 The category of renamings

######  Definition 5.1.

Let $\mathcal{C}$ be a first-order model of $\mathcal{T}$. A higher-order
renaming algebra $\mathbb{C}$ over $\mathcal{C}$ consists of:

$\displaystyle\mathbb{C}.\mathsf{Var}$ $\displaystyle:{}$
$\displaystyle\mathcal{C}.\mathsf{Ty}(1_{\mathcal{C}})\to\mathcal{U},$
$\displaystyle\mathbb{C}.\mathsf{var}$ $\displaystyle:{}$
$\displaystyle(A:\mathcal{C}.\mathsf{Ty}(1_{\mathcal{C}}))\to\mathbb{C}.\mathsf{Var}(A)\to\mathcal{C}.\mathsf{Tm}(1_{\mathcal{C}},A).$
$\lrcorner$

######  Definition 5.2.

Let $\mathcal{D}$ be a first-order model of $\mathcal{T}$. A first-order
renaming algebra over $\mathcal{D}$ is a category $\mathcal{C}$ with a
terminal object along with a functor $F:\mathcal{C}\to\mathcal{D}$ that
preserves the terminal object and with the structure of a global higher-order
renaming algebra $\mathbb{C}$ over $F^{\ast}(\mathsf{Tele}_{\mathbb{D}})$ such
that $\mathbb{C}.\mathsf{Var}$ is locally representable and
$\mathbb{C}.\mathsf{var}$ strictly preserves context extensions.  $\lrcorner$

Equivalently, a first-order renaming algebra over $\mathcal{D}$ is a CwF
$\mathcal{C}$ together with a CwF morphism $F:\mathcal{C}\to\mathcal{D}$ whose
action on types is bijective. (There is a cofibrantly generated factorization
system with such morphisms as its right class. The renaming algebras are the
objects in the left class.) The category of first-order renaming algebras over
$\mathcal{S}$ is locally finitely presentable, and there is an initial first-
order renaming algebra $\mathbf{Ren}_{\mathcal{S}}$. The category
$\mathbf{Ren}_{\mathcal{S}}$ is the category of renamings of $\mathcal{S}$; in
this section we write $F$ for the functor
$F:\mathbf{Ren}_{\mathcal{S}}\to\mathcal{S}$.

###  5.2 Relative induction principle

We pose $\mathcal{S}_{F}\triangleq F^{\ast}(\mathbf{Tele}_{\mathbb{S}})$;
$\mathcal{S}_{F}$ is an internal first-order model in
$\mathbf{Psh}(\mathbf{Ren}_{\mathcal{S}})$.

######  Theorem 5.3 (Induction principle for $\mathbb{S}$ relative to
$F:\mathbf{Ren}_{\mathcal{S}}\to\mathcal{S}$).

Let $\mathbb{S}^{\bullet}$ be a displayed higher-order model over
$\mathcal{S}_{F}$. Given the additional data of

$\displaystyle\mathsf{var}^{\bullet}$ $\displaystyle:{}$
$\displaystyle\forall(A:\mathcal{S}_{F}.\mathsf{Ty}(1_{\mathcal{S}_{F}}))\
(A^{\bullet}:\mathsf{Ty}^{\bullet}(A))\
(x:\mathsf{Var}(A))\to\mathsf{Tm}^{\bullet}(A^{\bullet},\mathsf{var}(x)),$

the displayed contextualization $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ admits
a section ${\llbracket-\rrbracket}$ that satisfies the additional computation
rule
${\llbracket\mathsf{var}_{A}(x)\rrbracket}=\mathsf{var}^{\bullet}({\llbracket
A\rrbracket},x).$

######  Proof 5.4.

See A.18.

Note that $\mathsf{var}_{A}(x)$ is always a closed term of $\mathcal{S}_{F}$,
thus ${\llbracket\mathsf{var}_{A}(x)\rrbracket}$ does not depend on any
environment.

###  5.3 Normal forms

Neutrals and normal forms are defined internally to
$\mathbf{Psh}(\mathbf{Ren}_{\mathcal{S}})$, as inductive families

$\mathsf{Ne},\mathsf{Nf}:\forall(A:\mathcal{S}_{F}.\mathsf{Ty}(1_{\mathcal{S}_{F}}))\
(a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A))\to\mathrm{Set},$

generated by the following constructors:

$\displaystyle\mathsf{var}^{\mathsf{ne}}$ $\displaystyle:{}$
$\displaystyle(x:\mathsf{Var}(A))\to\mathsf{Ne}_{A}(\mathsf{var}(x)),$
$\displaystyle\mathsf{app}^{\mathsf{ne}}$ $\displaystyle:{}$
$\displaystyle\mathsf{Ne}_{\Pi(A,B)}(f)\to\mathsf{Nf}_{A}(a)\to\mathsf{Ne}_{B[a]}(\mathsf{app}(f,a)),$
$\displaystyle\mathsf{lam}^{\mathsf{nf}}$ $\displaystyle:{}$
$\displaystyle((a:\mathsf{Var}(A))\to\mathsf{Nf}_{B[a]}(b[a]))\to\mathsf{Nf}_{\Pi(A,B)}(\mathsf{lam}(b)).$

The goal of normalization is to prove that every term has a unique normal
form:

$\forall(A:\mathcal{S}_{F}.\mathsf{Ty}(1_{\mathcal{S}_{F}}))\
(a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A))\to\mathrm{isContr}(\mathsf{Nf}_{A}(a)).$

This is accomplished in two steps. First a normalization function is obtained
from the relative induction principle, witnessing the existence of normal
forms. Then the uniqueness of normal forms is derived from the stability of
the normalization; a fact that is proven by mutual induction on neutrals and
normal forms.

###  5.4 Normalization displayed model

We now construct the normalization displayed higher-order model
$\mathbb{S}^{\bullet}$ over $\mathcal{S}_{F}$.

A displayed type $A^{\bullet}:\mathsf{Ty}^{\bullet}(A)$ over a type
$A:\mathcal{S}_{F}.\mathsf{Ty}(1_{\mathcal{S}_{F}})$ is a triple
$(A^{\bullet}_{p},A^{\bullet}_{u},A^{\bullet}_{q})$ consisting of a logical
_predicate_
$A^{\bullet}_{p}:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A)\to\mathrm{Set}$,
over the terms of type $A$, valued in the universe of sets; an _unquoting_ (or
reflection) function
$A^{\bullet}_{u}:(a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A))\to\mathsf{Ne}_{A}(a)\to
A^{\bullet}_{p}(a)$, witnessing the fact that any neutral term satisfies the
logical predicate $A^{\bullet}_{p}$; a _quoting_ (or reification) function
$A^{\bullet}_{q}:(a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A))\to
A^{\bullet}_{p}(a)\to\mathsf{Nf}_{A}(a)$, witnessing the fact a term
satisfying the logical predicate $A^{\bullet}_{p}$ admits a normal form. A
displayed term $a^{\bullet}$ of type $A^{\bullet}$ over a term
$a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A)$ is an element of
$A^{\bullet}_{p}(a)$: $\mathsf{Tm}^{\bullet}(A^{\bullet},a)\triangleq
A^{\bullet}_{p}(a)$. The logical predicate for $\Pi$-types is defined in the
same way as in the canonicity model.

$\Pi_{p}^{\bullet}(A^{\bullet},B^{\bullet})(f)\triangleq(\forall a\
a^{\bullet}\to B^{\bullet}_{p}(a^{\bullet},\mathsf{app}(f,a))).$

The unquoting function relies on the unquoting function of the codomain and
the quoting function of the domain.

$\Pi_{u}^{\bullet}(A^{\bullet},B^{\bullet})(f^{\mathsf{ne}})\triangleq\lambda
a^{\bullet}\mapsto
B^{\bullet}_{u}(a^{\bullet},\mathsf{app}^{\mathsf{ne}}(f^{\mathsf{ne}},A^{\bullet}_{q}(a^{\bullet}))).$

The quoting function says that any element of a $\Pi$-type is a lambda, as
implied by the $\eta$-rule. It relies on the quoting function of the codomain
and the unquoting function of the domain, and on the fact that every variable
is neutral.

$\Pi_{q}^{\bullet}(A^{\bullet},B^{\bullet})(f^{\bullet})\triangleq\mathsf{lam}^{\mathsf{nf}}(\lambda
a\mapsto\mathsf{let}\
a^{\bullet}=A^{\bullet}_{u}(\mathsf{var}^{\mathsf{ne}}(a))\ \mathsf{in}\
B^{\bullet}_{q}(a^{\bullet},f^{\bullet}(a^{\bullet}))).$

This completes the definition of the displayed higher-order model
$\mathbb{S}^{\bullet}$. It remains to check the last hypothesis of the
relative induction principle:

$\displaystyle\mathsf{var}^{\bullet}$ $\displaystyle:{}$ $\displaystyle\forall
A\ A^{\bullet}\
(x:\mathsf{Var}(A))\to\mathsf{Tm}^{\bullet}(A^{\bullet},\mathsf{var}(x)),$
$\displaystyle\mathsf{var}^{\bullet}(A^{\bullet},x)$
$\displaystyle\triangleq{}$ $\displaystyle
A^{\bullet}_{u}(\mathsf{var}^{\mathsf{ne}}(x)).$

By the relative induction principle (Theorem 5.3), we obtain a section
${\llbracket-\rrbracket}$ of $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$. We can
then define the normalization function as follows:

$\displaystyle\mathsf{norm}$ $\displaystyle:{}$ $\displaystyle\forall A\
(a:\mathcal{S}_{F}.\mathsf{Tm}(1_{\mathcal{S}_{F}},A))\to\mathsf{Nf}_{A}(a),$
$\displaystyle\mathsf{norm}_{A}(a)$ $\displaystyle\triangleq{}$
$\displaystyle{\llbracket A\rrbracket}_{q}({\llbracket a\rrbracket}).$

###  5.5 Stability of normalization and uniqueness of normal forms

Finally, we show the uniqueness of normal forms following [27]: we prove that
normalization is stable, that is every normal form for a term $a$ is equal to
the normal form of $a$ obtained from the normalization function. As the proof
relies on most of the computation rules of the section
${\llbracket-\rrbracket}$, it is a good example of computations with a
section.

######  Lemma 5.5 (Stability).

Given any normal form $a^{\mathsf{nf}}:\mathsf{Nf}_{A}(a)$, we have
$a^{\mathsf{nf}}=\mathsf{norm}_{A}(a)$.

######  Proof 5.6.

We prove the following two facts, by mutual induction on neutrals and normal
forms:
$(a^{\mathsf{ne}}:\mathsf{Ne}_{A}(a))\to{\llbracket a\rrbracket}={\llbracket
A\rrbracket}_{u}(a^{\mathsf{ne}}),$ $(a^{\mathsf{nf}}:\mathsf{Nf}_{A}(a))\to
a^{\mathsf{nf}}={\llbracket A\rrbracket}_{q}({\llbracket a\rrbracket}).$
Each case involves some of the computation rules of ${\llbracket-\rrbracket}$.

Case $a^{\mathsf{ne}}=\mathsf{var}^{\mathsf{ne}}(A,x)$

$\displaystyle{\llbracket\mathsf{var}_{A}(x)\rrbracket}$
$\displaystyle\quad=\mathsf{var}^{\bullet}({\llbracket A\rrbracket},x)$ (by
the computation rule for ${\llbracket\mathsf{var}(-)\rrbracket}$)
$\displaystyle\quad={\llbracket A\rrbracket}_{u}(a^{\mathsf{ne}}).$ (by
definition of $\mathsf{var}^{\bullet}$)

Case
$a^{\mathsf{ne}}=\mathsf{app}^{\mathsf{ne}}(f^{\mathsf{ne}},a^{\mathsf{nf}})$

$\displaystyle{\llbracket\mathsf{app}(f,a)\rrbracket}$
$\displaystyle\quad=\mathsf{app}^{\bullet}({\llbracket
f\rrbracket},{\llbracket a\rrbracket})$ (by the computation rule for
${\llbracket\mathsf{app}(-)\rrbracket}$) $\displaystyle\quad={\llbracket
f\rrbracket}({\llbracket a\rrbracket})$ (by definition of
$\mathsf{app}^{\bullet}$)
$\displaystyle\quad={\llbracket\Pi(A,B)\rrbracket}_{u}(f^{\mathsf{ne}},{\llbracket
a\rrbracket})$ (by the induction hypothesis for $f^{\mathsf{ne}}$)
$\displaystyle\quad={\llbracket
B[a]\rrbracket}_{u}(\mathsf{app}^{\mathsf{ne}}(f^{\mathsf{ne}},a^{\mathsf{nf}})).$
(by definition of $\Pi^{\bullet}_{u}$ and the induction hypothesis for
$a^{\mathsf{nf}}$)

Case $a^{\mathsf{nf}}=\mathsf{lam}^{\mathsf{nf}}(b^{\mathsf{nf}})$

$\displaystyle{\llbracket\Pi(A,B)\rrbracket}_{q}({\llbracket\mathsf{lam}(b)\rrbracket})$
$\displaystyle\quad=\Pi_{q}^{\bullet}({\llbracket A\rrbracket},\lambda
a^{\bullet}\mapsto{\llbracket B(\underline{a})\rrbracket}[\underline{a}\mapsto
a^{\bullet}])(\lambda a^{\bullet}\mapsto{\llbracket
b(\underline{a})\rrbracket}[\underline{a}\mapsto a^{\bullet}])$ (by the
computation rules for ${\llbracket\Pi(-)\rrbracket}$ and
${\llbracket\mathsf{lam}\rrbracket}$)
$\displaystyle\quad=\mathsf{lam}^{\mathsf{nf}}(\lambda a\mapsto\mathsf{let}\
a^{\bullet}={\llbracket A\rrbracket}_{u}(\mathsf{var}^{\mathsf{ne}}(a))\
\mathsf{in}\ {({\llbracket B(\underline{a})\rrbracket}[\underline{a}\mapsto
a^{\bullet}])}_{q}({\llbracket
b(\underline{a})\rrbracket}[\underline{a}\mapsto a^{\bullet}])$ (by definition
of $\Pi^{\bullet}_{q}$) $\displaystyle\quad=\mathsf{lam}^{\mathsf{nf}}(\lambda
a\mapsto{({\llbracket
B(\underline{a})\rrbracket}[\underline{a}\mapsto{\llbracket\mathsf{var}(a)\rrbracket}])}_{q}({\llbracket
b(\underline{a})\rrbracket}[\underline{a}\mapsto{\llbracket\mathsf{var}(a)\rrbracket}]))$
(by the computation rule for ${\llbracket\mathsf{var}(a)\rrbracket}$)
$\displaystyle\quad=\mathsf{lam}^{\mathsf{nf}}(\lambda a\mapsto{\llbracket
B[\mathsf{var}(a)]\rrbracket}_{q}({\llbracket b[\mathsf{var}(a)]\rrbracket}))$
(by the naturality of ${\llbracket-\rrbracket}$)
$\displaystyle\quad=\mathsf{lam}^{\mathsf{nf}}(b^{\mathsf{nf}}).$ (by the
induction hypothesis for $b^{\mathsf{nf}}$)

##  6 The category of sections of a displayed first-order model

The last tool that is needed for the proofs of relative induction principles
is the _category of sections_ of an internal displayed higher-order model.
This replaces the use of a displayed inserter in our previous work [10].

Let $\mathcal{M}^{\bullet}$ be a global internal displayed first-order model
over a first-order model $\mathcal{M}$, internally to some presheaf category
$\mathbf{Psh}(\mathcal{C})$. We see $\mathcal{M}$ as a functor
$\mathcal{M}:\mathcal{C}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}$, as
justified by Proposition 2.6. Write $\mathbf{DispMod}_{\mathcal{T}}$ for the
external category of a first-order model of $\mathcal{T}$ with a displayed
first-order model over it. There is a forgetful functor
$U:\mathbf{DispMod}_{\mathcal{T}}\to\mathbf{Mod}_{\mathcal{T}}$. Since the
notion of displayed first-order model is also essentially algebraic, we can
also view $\mathcal{M}^{\bullet}$ as a functor
$\mathcal{C}\to\mathbf{DispMod}_{\mathcal{T}}^{\mathsf{op}}$ such that
$U\circ\mathcal{M}^{\bullet}=\mathcal{M}$. Similarly, writing
$\mathbf{Sect}_{\mathcal{T}}$ for the category of a displayed first-order
model of $\mathcal{T}$ with a section, a section of $\mathcal{M}^{\bullet}$
can be identified with a functor
${\llbracket-\rrbracket}:\mathcal{C}\to\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}$
such that $V\circ{\llbracket-\rrbracket}=\mathcal{M}^{\bullet}$, where $V$ is
the forgetful functor
$\mathbf{Sect}_{\mathcal{T}}\to\mathbf{DispMod}_{\mathcal{T}}$.

######  Definition 6.1.

The category
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ of sections
of $\mathcal{M}^{\bullet}$ is the pullback (in $\mathbf{Cat}$)

${\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]}$${\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}}$${\mathcal{C}}$${\mathbf{DispMod}_{\mathcal{T}}^{\mathsf{op}}}$${\lrcorner}$$\scriptstyle{\pi_{0}}$$\scriptstyle{{\llbracket-\rrbracket}_{0}}$$\scriptstyle{V}$$\scriptstyle{\mathcal{M}^{\bullet}}$

By the universal property of the pullback, the data of a section of
$\mathcal{M}^{\bullet}$ is equivalent to the data of a section of $\pi_{0}$ in
$\mathbf{Cat}$. The category
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ is itself
equipped with a section ${\llbracket-\rrbracket}_{0}$ of
$\pi_{0}^{\ast}(\mathcal{M}^{\bullet})$, which is called the _generic section_
of $\mathcal{M}^{\bullet}$.

In order to prove an induction principle such as Theorem 5.3, we want to use
the initiality of $\mathcal{C}$ in some category to obtain section of
$\pi_{0}$. For example, when $\mathcal{C}$ is the category of renamings, it
suffices to equip
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ with the
structure of a renaming algebra that is preserved by $\pi_{0}$.

This typically involves lifting the terminal object and context extensions of
$\mathcal{C}$ to
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$. Conditions
for the lifting of these finite limits are given in Section A.3; the
initiality of the syntax is needed to lift the terminal object.

## References

  * [1] Andreas Abel, Joakim Öhman, and Andrea Vezzosi.  Decidability of conversion for type theory in type theory.  Proc. ACM Program. Lang., 2(POPL):23:1–23:29, 2018.  doi:10.1145/3158111.
  * [2] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher.  Categorical reconstruction of a reduction free normalization proof.  In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS ’95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182–199. Springer, 1995.  doi:10.1007/3-540-60164-3\\_27.
  * [3] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher.  Reduction-free normalisation for a polymorphic system.  In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 98–106. IEEE Computer Society, 1996.  doi:10.1109/LICS.1996.561309.
  * [4] Thorsten Altenkirch and Ambrus Kaposi.  Normalisation by Evaluation for Dependent Types.  In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  URL: http://drops.dagstuhl.de/opus/volltexte/2016/5972, doi:10.4230/LIPIcs.FSCD.2016.6.
  * [5] Thorsten Altenkirch and Ambrus Kaposi.  Type theory in type theory using quotient inductive types.  In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, pages 18–29, New York, NY, USA, 2016. ACM.  URL: http://doi.acm.org/10.1145/2837614.2837638, doi:10.1145/2837614.2837638.
  * [6] Thorsten Altenkirch, Ambrus Kaposi, and Michael Shulman.  Towards higher observational type theory.  In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes, 2022.  URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_37.pdf.
  * [7] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler.  Two-level type theory and applications.  CoRR, abs/1705.03307, 2019.  URL: http://arxiv.org/abs/1705.03307, arXiv:1705.03307.
  * [8] Steve Awodey.  Natural models of homotopy type theory.  Mathematical Structures in Computer Science, 28(2):241–286, 2018\.  doi:10.1017/S0960129516000268.
  * [9] Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson.  Proofs for free — parametricity for dependent types.  Journal of Functional Programming, 22(02):107–152, 2012.  URL: https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=135303, doi:10.1017/S0956796812000056.
  * [10] Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler.  Relative induction principles for type theories.  CoRR, abs/2102.11649, 2021.  URL: https://arxiv.org/abs/2102.11649, arXiv:2102.11649.
  * [11] Simon Castellan, Pierre Clairambault, and Peter Dybjer.  Categories with families: Unityped, simply typed, and dependently typed.  CoRR, abs/1904.00827, 2019.  URL: http://arxiv.org/abs/1904.00827, arXiv:1904.00827.
  * [12] Thierry Coquand.  Presheaf model of type theory.  Available at https://www.cse.chalmers.se/~coquand/presheaf.pdf, 2013\.
  * [13] Thierry Coquand.  Canonicity and normalization for dependent type theory.  Theor. Comput. Sci., 777:184–191, 2019.  doi:10.1016/j.tcs.2019.01.015.
  * [14] Thierry Coquand, Simon Huber, and Christian Sattler.  Canonicity and homotopy canonicity for cubical type theory, 2021.  arXiv:1902.06572.
  * [15] Thierry Coquand, Simon Huber, and Christian Sattler.  Canonicity and homotopy canonicity for cubical type theory.  Log. Methods Comput. Sci., 18(1), 2022.  doi:10.46298/lmcs-18(1:28)2022.
  * [16] Marcelo P. Fiore.  Semantic analysis of normalisation by evaluation for typed lambda calculus.  In Proceedings of the 4th international ACM SIGPLAN conference on Principles and practice of declarative programming, October 6-8, 2002, Pittsburgh, PA, USA (Affiliated with PLI 2002), pages 26–37. ACM, 2002.  doi:10.1145/571157.571161.
  * [17] Marcelo P. Fiore and Ola Mahmoud.  Second-order algebraic theories.  CoRR, abs/1308.5409, 2013.  URL: http://arxiv.org/abs/1308.5409, arXiv:1308.5409.
  * [18] Daniel Gratzer.  Normalization for multimodal type theory.  In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, New York, NY, USA, 2022. Association for Computing Machinery.  URL: https://jozefg.github.io/papers/2022-normalization-for-multimodal-type-theory-short.pdf, doi:10.1145/3531130.3532398.
  * [19] Daniel Gratzer and Jonathan Sterling.  Syntactic categories for dependent type theory: sketching and adequacy.  CoRR, abs/2012.10783, 2020.  URL: https://arxiv.org/abs/2012.10783, arXiv:2012.10783.
  * [20] Robert Harper.  An equational logical framework for type theories.  CoRR, abs/2106.01484, 2021.  URL: https://arxiv.org/abs/2106.01484, arXiv:2106.01484.
  * [21] Robert Harper, Furio Honsell, and Gordon D. Plotkin.  A framework for defining logics.  J. ACM, 40(1):143–184, 1993.  doi:10.1145/138027.138060.
  * [22] Martin Hofmann.  Syntax and semantics of dependent types.  In Semantics and Logics of Computation, pages 79–130. Cambridge University Press, 1997.
  * [23] Martin Hofmann.  Semantical analysis of higher-order abstract syntax.  In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 204–213. IEEE Computer Society, 1999\.  doi:10.1109/LICS.1999.782616.
  * [24] Jason Z. S. Hu, Brigitte Pientka, and Ulrich Schöpp.  A category theoretic view of contextual types: from simple types to dependent types.  CoRR, abs/2206.02831, 2022.  arXiv:2206.02831, doi:10.48550/arXiv.2206.02831.
  * [25] Peter T Johnstone.  Sketches of an elephant: a Topos theory compendium.  Oxford logic guides. Oxford Univ. Press, New York, NY, 2002.  URL: https://cds.cern.ch/record/592033.
  * [26] Achim Jung and Jerzy Tiuryn.  A new characterization of lambda definability.  In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 245–257. Springer, 1993.  doi:10.1007/BFb0037110.
  * [27] Ambrus Kaposi.  Type theory in a type theory with quotient inductive types.  PhD thesis, University of Nottingham, UK, 2017.  URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.713896.
  * [28] Ambrus Kaposi, Simon Huber, and Christian Sattler.  Gluing for type theory.  In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 25:1–25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPIcs.FSCD.2019.25.
  * [29] Krzysztof Kapulkin and Peter LeFanu Lumsdaine.  The homotopy theory of type theories.  Advances in Mathematics, 337:1–38, 2018.  URL: https://www.sciencedirect.com/science/article/pii/S0001870818303062, doi:https://doi.org/10.1016/j.aim.2018.08.003.
  * [30] András Kovács.  Generalized universe hierarchies and first-class universe levels.  In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 28:1–28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022\.  doi:10.4230/LIPIcs.CSL.2022.28.
  * [31] Frank Pfenning and Carsten Schürmann.  System description: Twelf - A meta-logical framework for deductive systems.  In Harald Ganzinger, editor, Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume 1632 of Lecture Notes in Computer Science, pages 202–206. Springer, 1999.  doi:10.1007/3-540-48660-7\\_14.
  * [32] Loïc Pujet and Nicolas Tabareau.  Impredicative Observational Equality.  In POPL 2023 - 50th ACM SIGPLAN Symposium on Principles of Programming Languages, volume 7 of Proceedings of the ACM on programming languages, page 74, Boston, United States, January 2023.  URL: https://hal.science/hal-03857705, doi:10.1145/3571739.
  * [33] Michael Shulman.  Towards a third-generation HOTT.  Talk series at the Homotopy Type Theory at CMU seminar, 2022.
  * [34] Jonathan Sterling.  First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory.  PhD thesis, Carnegie Mellon University, 2021.  Version 1.1, revised May 2022.  doi:10.5281/zenodo.6990769.
  * [35] Jonathan Sterling.  Naïve logical relations in synthetic Tait computability.  Unpublished manuscript, June 2022.
  * [36] Jonathan Sterling and Carlo Angiuli.  Normalization for cubical type theory.  CoRR, abs/2101.11479, 2021.  URL: https://arxiv.org/abs/2101.11479, arXiv:2101.11479.
  * [37] Jonathan Sterling and Bas Spitters.  Normalization by gluing for free $\lambda$-theories.  CoRR, abs/1809.08646, 2018.  URL: http://arxiv.org/abs/1809.08646, arXiv:1809.08646.
  * [38] Taichi Uemura.  A general framework for the semantics of type theory.  CoRR, abs/1904.04097, 2019.  URL: http://arxiv.org/abs/1904.04097, arXiv:1904.04097.
  * [39] Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz, and Paige North.  Synthetic Tait computability for simplicial type theory.  In 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022.  URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_17.pdf.

##  Appendix A Technical results

###  A.1 Local representability

We recall the definition of the notion of locally representable dependent
presheaf, which encodes the notion of context extension.

######  Definition A.1.

Let $\mathcal{C}$ be a category, $X$ be a presheaf over $\mathcal{C}$ and $Y$
be a dependent presheaf over $X$. Then $Y$ is said to be locally representable
if for every element $x:X(\Gamma)$, the presheaf

$\displaystyle Y_{\mid
x}:{(\mathcal{C}/\Gamma)}^{\mathsf{op}}\to\mathbf{Set},$ $\displaystyle
Y_{\mid x}(\Delta,\rho)\triangleq Y(\Delta,x[\rho])$

is representable. The representing object, consisting of an extended context
and a projection map, is written $(\Gamma.Y[x],\bm{p}_{x})$ and the generic
element is written $\bm{q}_{x}:Y(\Gamma.Y[x],x[\bm{p}_{x}])$.

Given any object $\Delta\in\mathcal{C}$, map $\rho:\Delta\to\Gamma$ and
element $y:Y(\Delta,x[\rho])$, we write ${\left\langle\rho,a\right\rangle}$
for the unique morphism such that
$\bm{p}_{x}\circ{\left\langle\rho,y\right\rangle}=\rho$ and
$\bm{q}_{x}[{\left\langle\rho,y\right\rangle}]=y$.  $\lrcorner$

###  A.2 Characterization of the telescopic contextualization

We define the contextual slices of a first-order model (which are called
fibrant slices in [29]).

######  Definition A.2 (Contextual slice).

Let $\mathcal{C}$ be a first-order model of $\mathcal{T}$. Given
$\Gamma\in\mathcal{C}$, the contextual slice $(\mathcal{C}\sslash\Gamma)$ is
the contextual first-order model given by:

  * •

Objects of $(\mathcal{C}\sslash\Gamma)$ are telescopes (iterated context
extensions) over $\Gamma$.

  * •

Morphisms from $\Delta_{1}$ to $\Delta_{2}$ are morphisms from
$\Gamma.\Delta_{1}$ to $\Gamma.\Delta_{2}$ in $(\mathcal{C}/\Gamma)$.

  * •

The rest of the structure is inherited from $\mathcal{C}$ along the projection

$(\mathcal{C}\sslash\Gamma)\ni\Delta\mapsto\Gamma.\Delta\in\mathcal{C}.$

The contextual slice is functorial in both $\mathcal{C}$ and (contravariantly)
$\Gamma$:

  * •

For any $f:\Delta\to\Gamma$, there is a pullback morphism
$f^{\ast}:(\mathcal{C}\sslash\Gamma)\to(\mathcal{C}\sslash\Delta)$. Its
actions on objects, substitutions, types and terms are all given by
substitution along $f$.

  * •

For any $F:\mathcal{C}\to\mathcal{D}$, there is a morphism
$(F\sslash\Gamma):(\mathcal{C}\sslash\Gamma)\to(\mathcal{D}\sslash
F(\Gamma))$. Its actions on objects, substitutions, types and terms are given
by the actions of $F$ on telescopes, substitutions, types and terms.

  * •

The following diagrams commute (for any $F:\mathcal{C}\to\mathcal{D}$ and
$f:\Delta\to\Gamma$):

${(\mathcal{C}\sslash\Gamma)}$${(\mathcal{D}\sslash
F(\Gamma))}$${(\mathcal{C}\sslash\Delta)}$${(\mathcal{D}\sslash
F(\Delta))\hbox to0.0pt{\
.\hss}}$$\scriptstyle{(F\sslash\Gamma)}$$\scriptstyle{f^{\ast}}$$\scriptstyle{f^{\ast}}$$\scriptstyle{(F\sslash\Delta)}$

  * •

For any $f:\Theta\to\Gamma$ and object $\Delta$ of
$(\mathcal{C}\sslash\Gamma)$, we have
$(f^{\ast}\sslash\Delta)={\left\langle\bm{p}_{\Delta}^{\ast}(f),\bm{q}_{\Delta}\right\rangle}^{\ast}$
as a morphism from $(\mathcal{C}\sslash\Gamma.\Delta)$ to
$(\mathcal{C}\sslash\Theta.f^{\ast}(\Delta))$. Here ${\left\langle
f\circ\bm{p}_{f^{\ast}(\Delta)},\bm{q}_{f^{\ast}(\Delta)}\right\rangle}$ is a
morphism from $\Theta.f^{\ast}(\Delta)$ to $\Gamma.\Delta$.

######  Lemma A.3.

Let $\mathcal{C}$ be a first-order model of $\mathcal{T}$. Then the telescopic
contextualization $\mathbf{Tele}_{\mathbb{C}}$ corresponds the contextual
slice functor

$(\mathcal{C}\sslash-):\mathcal{C}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}.$

######  Proof A.4.

Immediate from unfolding the definitions.

######  Corollary A.5.

The externalization $1_{\mathcal{C}}^{\ast}(\mathbf{Tele}_{\mathbb{C}})$ is
the contextual core of $\mathcal{C}$.

######  Proof A.6.

By Lemma A.3, $1_{\mathcal{C}}^{\ast}(\mathbf{Tele}_{\mathbb{C}})$ is the
contextual slice $(\mathcal{C}\sslash 1_{\mathcal{C}})$, the contextual core
of $\mathcal{C}$.

######  Lemma A.7.

Let $\mathcal{C}$ be a contextual first-order model and
$A:\mathcal{C}.\mathsf{Ty}(1_{\mathcal{C}})$ be a closed type. Then the
contextual slice $(\mathcal{C}\sslash A)$ satisfies the following universal
property: for every model $\mathcal{E}$, morphism
$F:\mathcal{C}\to\mathcal{E}$ and element $a:\mathcal{E}.\mathsf{Tm}(F(A))$,
there is a unique morphism $\widetilde{F}:(\mathcal{C}\sslash
1_{\mathcal{C}}.A)\to\mathcal{E}$ such that
$\widetilde{F}\circ\bm{p}_{A}^{\ast}=F$ and $\widetilde{F}(\bm{q}_{A})=a$.

In other words, $(\mathcal{C}\sslash 1_{\mathcal{C}}.A)$ is the free extension
of $\mathcal{C}$ by a generic element $\bm{q}_{A}$ of type $A$.

######  Proof A.8.

The contextuality of $\mathcal{C}$ implies that
$\mathcal{C}\cong(\mathcal{C}\sslash 1_{\mathcal{C}})$ and thus we have a
weakening morphism $\bm{p}_{A}^{\ast}:\mathcal{C}\to(\mathcal{C}\sslash
1_{\mathcal{C}}.A)$. We write
$A^{\prime}:\mathcal{C}.\mathsf{Ty}(1_{\mathcal{C}}.A)$ for the weakening of
$A$, i.e. $A^{\prime}=\bm{p}_{A}^{\ast}(A)$.

Take a morphism $F:\mathcal{C}\to\mathcal{E}$ and an element
$a:\mathcal{E}.\mathsf{Tm}(F(A))$.

Let $\tilde{F}:(\mathcal{C}\sslash 1_{\mathcal{C}}.A)\to\mathcal{E}$ be any
morphism such that $\tilde{F}\circ\bm{p}_{A}^{\ast}=F$ and
$\tilde{F}(\bm{q}_{A})=a$. Since $(\mathcal{C}\sslash 1_{\mathcal{C}}.A)$ is
contextual, $\tilde{F}$ factors through
$(\tilde{F}\sslash(1_{\mathcal{C}}.A)):(\mathcal{C}\sslash
1_{\mathcal{C}}.A)\to(\mathcal{E}\sslash 1_{\mathcal{E}})$.

The following diagram commutes:

${(\mathcal{C}\sslash 1_{\mathcal{C}}.A)}$${(\mathcal{E}\sslash
1_{\mathcal{E}})}$${(\mathcal{C}\sslash
1_{\mathcal{C}}.A.A^{\prime})}$${(\mathcal{E}\sslash
1_{\mathcal{E}}.\tilde{F}(A^{\prime}))}$${(\mathcal{C}\sslash
1_{\mathcal{C}}.A)}$${(\mathcal{E}\sslash 1_{\mathcal{E}})\hbox to0.0pt{\
.\hss}}$$\scriptstyle{\bm{p}_{A^{\prime}}^{\ast}}$$\scriptstyle{(\tilde{F}\sslash(1_{\mathcal{C}}.A))}$$\scriptstyle{\bm{p}_{\tilde{F}(A^{\prime})}^{\ast}}$$\scriptstyle{(\tilde{F}\sslash(1_{\mathcal{C}}.A).A^{\prime})}$$\scriptstyle{{\left\langle\bm{q}_{A}\right\rangle}^{\ast}}$$\scriptstyle{{\left\langle\tilde{F}(\bm{q}_{A})\right\rangle}^{\ast}}$$\scriptstyle{(\tilde{F}\sslash(1_{\mathcal{C}}.A))}$

By assumptions, we have $\tilde{F}(A^{\prime})=F(A)$ and
$\tilde{F}(\bm{q}_{A})=a$. Thus, $\tilde{F}$ factors as the composition

$(\mathcal{C}\sslash
1_{\mathcal{C}}.A)\xrightarrow{\bm{p}_{A^{\prime}}^{\ast}}(\mathcal{C}\sslash
1_{\mathcal{C}}.A.A^{\prime})\xrightarrow{(\tilde{F}\sslash(1_{\mathcal{C}}.A).A^{\prime})}(\mathcal{E}\sslash
1_{\mathcal{E}}.F(A))\xrightarrow{{\left\langle
a\right\rangle}^{\ast}}(\mathcal{E}\sslash
1_{\mathcal{E}})\xrightarrow{}\mathcal{E}.$

By functoriality of $(-\sslash 1_{\mathcal{C}}.A)$, we have $(F\sslash
1_{\mathcal{C}}.A)=(\tilde{F}\sslash(1_{\mathcal{C}}.A).A^{\prime})\circ(\bm{p}_{A}^{\ast}\sslash
1_{\mathcal{C}}.A)$. We can simplify $(\bm{p}_{A}^{\ast}\sslash
1_{\mathcal{C}}.A)={\left\langle\bm{p}_{A}\circ\bm{p}_{A^{\prime}},\bm{q}_{A^{\prime}}\right\rangle}^{\ast}$.
Finally, we see that
${\left\langle\bm{q}_{A}\right\rangle}^{\ast}\circ{\left\langle\bm{p}_{A}\circ\bm{p}_{A^{\prime}},\bm{q}_{A^{\prime}}\right\rangle}^{\ast}=\mathsf{id}={\left\langle\bm{q}_{A}\right\rangle}^{\ast}\circ\bm{p}_{A^{\prime}}^{\ast}$.

Thus,
$(\tilde{F}\sslash(1_{\mathcal{C}}.A).A^{\prime})\circ\bm{p}_{A^{\prime}}^{\ast}=F_{\ast}(1_{\mathcal{C}}.A)$
and we can simplify the factorization to

$(\mathcal{C}\sslash
1_{\mathcal{C}}.A)\xrightarrow{F_{\ast}(1_{\mathcal{C}}.A)}(\mathcal{E}\sslash
1_{\mathcal{E}}.F(A))\xrightarrow{{\left\langle
a\right\rangle}^{\ast}}(\mathcal{E}\sslash
1_{\mathcal{E}})\xrightarrow{}\mathcal{E}.$

As this composition does not depend on $\tilde{F}$ and satisfies the required
equations, this shows the existence and uniqueness of $\tilde{F}$.

######  Lemma A.9.

Given any $\Gamma\in\mathcal{C}$ and $A:\mathcal{C}.\mathsf{Ty}(\Gamma)$, then
$(\mathcal{C}\sslash\Gamma.A)$ satisfies the following universal property: for
every model $\mathcal{E}$, morphism
$F:(\mathcal{C}\sslash\Gamma)\to\mathcal{E}$ and element
$a:\mathcal{E}.\mathsf{Tm}(F(A))$, there is a unique morphism
$\widetilde{F}:(\mathcal{C}\sslash\Gamma.A)\to\mathcal{E}$ such that
$\widetilde{F}\circ\bm{p}_{A}^{\ast}=F$ and $\widetilde{F}(\bm{q}_{A})=a$.

In other words, $(\mathcal{C}\sslash\Gamma.A)$ is the free extension of
$(\mathcal{C}\sslash\Gamma)$ by a generic element $\bm{q}_{A}$ of type $A$.

######  Proof A.10.

We have $(\mathcal{C}\sslash\Gamma.A)\cong((\mathcal{C}\sslash\Gamma)\sslash
1_{(\mathcal{C}\sslash\Gamma)}.A)$. Then the result follows from Lemma A.7.

###  A.3 Properties of the category of sections

We now prove the properties of the category of sections of a displayed first-
order model. Fix a global internal first-order model
$\mathcal{M}:\mathcal{C}\to\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}$ and a
displayed first-order model
$\mathcal{M}^{\bullet}:\mathcal{C}\to\mathbf{DispMod}_{\mathcal{T}}^{\mathsf{op}}$
over $\mathcal{M}$.

We prove conditions that relate the existence of some finite limits in
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ to the
universal properties of the first-order models $\mathcal{M}(\Gamma)$ for
$\Gamma\in\mathcal{C}$.

We have defined the category
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ of sections
of $\mathcal{M}^{\bullet}$ as the following pullback

${\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]}$${\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}}$${\mathcal{C}}$${\mathbf{DispModel}_{\mathcal{T}}^{\mathsf{op}}\hbox
to0.0pt{\
.\hss}}$${\lrcorner}$$\scriptstyle{\pi_{0}}$$\scriptstyle{{\llbracket-\rrbracket}_{0}}$$\scriptstyle{\mathcal{M}^{\bullet}}$

Unfolding the definition, an object of
$\mathbf{Sect}_{\mathcal{T}}^{\mathsf{op}}[\mathcal{M}^{\bullet}]$ is a pair
$(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ where $\Gamma\in\mathcal{C}$ and
${\llbracket-\rrbracket}_{\Gamma}$ is a section of
$\mathcal{M}^{\bullet}(\Gamma)$ over $\mathcal{M}(\Gamma)$. A morphism of from
$(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ to
$(\Delta,{\llbracket-\rrbracket}_{\Delta})$ is a morphism
$f:\mathcal{C}(\Gamma,\Delta)$ such that the outer square commutes in the
following diagram:

${\mathcal{M}^{\bullet}(\Delta)}$${\mathcal{M}^{\bullet}(\Gamma)}$${\mathcal{M}(\Delta)}$${\mathcal{M}(\Gamma)\hbox
to0.0pt{\
.\hss}}$$\scriptstyle{\mathcal{M}^{\bullet}(f)}$$\scriptstyle{\mathcal{M}(f)}$$\scriptstyle{{\llbracket-\rrbracket}_{\Gamma}}$$\scriptstyle{{\llbracket-\rrbracket}_{\Delta}}$

######  Lemma A.11.

If $\mathcal{C}$ has a terminal object $1_{\mathcal{C}}$ and
$\mathcal{M}(1_{\mathcal{C}})$ is the initial model of $\mathcal{T}$, then
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$ has a terminal object
that is strictly preserved by $\pi_{0}$.

######  Proof A.12.

Since $\mathcal{M}(1_{\mathcal{C}})$ is initial, we obtain a section
${\llbracket-\rrbracket}_{1_{\mathcal{C}}}$ of
$\mathcal{M}^{\bullet}(1_{\mathcal{C}})$. We now prove that
$(1_{\mathcal{C}},{\llbracket-\rrbracket}_{1_{\mathcal{C}}})$ is terminal in
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$. Let
$(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ be any object of
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$. A morphism from
$(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ to
$(1_{\mathcal{C}},{\llbracket-\rrbracket}_{1_{\mathcal{C}}})$ is a morphism
$f:\mathcal{C}(\Gamma,1_{\mathcal{C}})$ such that the following square
commutes:

${\mathcal{M}^{\bullet}(1_{\mathcal{C}})}$${\mathcal{M}^{\bullet}(\Gamma)}$${\mathcal{M}(1_{\mathcal{C}})}$${\mathcal{M}(\Gamma)\hbox
to0.0pt{\
.\hss}}$$\scriptstyle{\mathcal{M}^{\bullet}(f)}$$\scriptstyle{{\llbracket-\rrbracket}_{1_{\mathcal{C}}}}$$\scriptstyle{\mathcal{M}(f)}$$\scriptstyle{{\llbracket-\rrbracket}_{\Gamma}}$

Since $1_{\mathcal{C}}$ is terminal, there is only one morphism
$f:\mathcal{C}(\Gamma,1_{\mathcal{C}})$, and the corresponding square commutes
by initiality of $\mathcal{M}(1_{\mathcal{C}})$.

######  Definition A.13.

Let $X$ be a presheaf over $\mathcal{C}$ and $Y$ be a locally representable
dependent presheaf over $X$. Assume given the data of global elements

$\displaystyle f_{X}$ $\displaystyle:{}$ $\displaystyle
X\to\mathcal{M}.\mathsf{Ty}(1_{\mathcal{M}}),$ $\displaystyle f_{Y}$
$\displaystyle:{}$ $\displaystyle(x:X)\to
Y(x)\to\mathcal{M}.\mathsf{Tm}(1_{\mathcal{M}},f_{X}(x))$

of $\mathbf{Psh}(\mathcal{C})$.

We say that $f_{Y}$ is compatible with $\mathcal{M}$ if for every element
$x:X(\Gamma)$, the external first-order model $\mathcal{M}(\Gamma.Y(x))$
satisfies the following universal property: for every first-order model
$\mathcal{E}$, morphism $E:\mathcal{M}(\Gamma)\to\mathcal{E}$ and element
$z:\mathcal{E}.\mathsf{Tm}(1_{\mathcal{E}},E(f_{X}(x)))$, there is a unique
morphism $\widetilde{E}:\mathcal{M}(\Gamma.Y(x))\to\mathcal{E}$ such that
$E=\widetilde{E}\circ\mathcal{M}(\bm{p}_{x})$ and
$z=\widetilde{E}(f_{Y}(x,\bm{q}_{x}))$.

In other words, $\mathcal{M}(\Gamma.Y(x))$ should be the free extension of
$\mathcal{M}(\Gamma)$ by an element $f_{Y}(x,\bm{q}_{x})$ of type $f_{X}(x)$,
the extension being witnessed by the morphism
$\mathcal{M}(\bm{p}_{x}):\mathcal{M}(\Gamma)\to\mathcal{M}(\Gamma.Y(x))$.
$\lrcorner$

######  Lemma A.14.

Let $F:\mathcal{C}\to\mathcal{D}$ be a CwF morphism.

Then the condition of Definition A.13 is satisfied, with
$\mathcal{M}=F^{\ast}(\mathsf{Tele}_{\mathbb{D}})$, $X$ and $Y$ being
respectively the types and terms of $\mathcal{C}$, and $f_{X}$ and $f_{Y}$
being the actions of $F$ on types and terms.

######  Proof A.15.

By Definition A.2, $\mathcal{M}$ correspond to the functor

$\mathcal{C}\ni\Gamma\mapsto(\mathcal{D}\sslash
F(\Gamma))\in\mathbf{Mod}_{\mathcal{T}}^{\mathsf{op}}.$

Thus, we need to check that given any $\Gamma\in\mathcal{C}$ and
$A:\mathcal{C}.\mathsf{Ty}(\Gamma)$, the model $(\mathcal{D}\sslash
F(\Gamma.A))$ is the free extension of $(\mathcal{D}\sslash F(\Gamma))$ by a
generic element of type $F(A)$. Since $F$ preserves extensions,
$F(\Gamma.A)\cong F(\Gamma).F(A)$, and thus the result follows by Lemma A.9.

######  Lemma A.16.

Let $X$ be a presheaf over $\mathcal{C}$ and $Y$ be a locally representable
presheaf family over $X$ equipped with operations $f_{X}$ and $f_{Y}$
satisfying the condition of Definition A.13. Finally, assume that for every
$(\Gamma,{\llbracket-\rrbracket}_{\Gamma})\in\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$,
$\Delta\in\mathcal{C}$, $\gamma:\mathcal{C}(\Delta,\Gamma)$, $x:X(\Gamma)$ and
$y:Y(\Delta,x[\gamma])$ we have

$\displaystyle f_{Y}^{\bullet}(x,y)$ $\displaystyle:{}$
$\displaystyle\mathcal{M}^{\bullet}(\Delta).\mathsf{Tm}^{\bullet}(1^{\bullet},\mathcal{M}^{\bullet}(\gamma)({\llbracket
f_{X}(x)\rrbracket}_{\Gamma}),f_{Y}(x[\gamma],y)),$

naturally in $(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ and $\Delta$.

Consider the presheaf $X_{0}\triangleq\pi_{0}^{\ast}(X)$ over
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$ and the dependent
presheaf $Y_{0}$ over $X_{0}$ specified on objects by:

$\displaystyle Y_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),x)$
$\displaystyle\triangleq{}$ $\displaystyle\\{y:Y(\Gamma,x)\mid{\llbracket
f_{Y}(x,y)\rrbracket}_{\Gamma}=f_{Y}^{\bullet}(x,y)\\}.$

Then the presheaf family $Y_{0}$ is locally representable and the action
induced by the first projections
$Y_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),x)\to Y(\Gamma,x)$ strictly
preserve context extensions.

######  Proof A.17.

Let $(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$ be an object of
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$ and $x:X(\Gamma)$ be an
element of $X_{0}$ at this object. We have to prove that the presheaf
${Y_{0}}_{\mid x}$ over
$(\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}/(\Gamma,{\llbracket-\rrbracket}_{\Gamma}))$
is representable.

Consider the diagram:

${\mathcal{M}^{\bullet}(\Gamma)}$${\mathcal{M}^{\bullet}(\Gamma.Y(x))}$${\mathcal{M}(\Gamma)}$${\mathcal{M}(\Gamma.Y(x))}$$\scriptstyle{\mathcal{M}^{\bullet}(\bm{p}_{x})}$$\scriptstyle{\mathcal{M}(\bm{p}_{x})}$$\scriptstyle{{\llbracket-\rrbracket}_{\Gamma}}$$\scriptstyle{{\llbracket-\rrbracket}_{\Gamma.Y(x)}}$

We construct a section ${\llbracket-\rrbracket}_{\Gamma.Y(x)}$ of
$\mathcal{M}^{\bullet}(\Gamma.Y(x))$ over $\mathcal{M}(\Gamma.Y(x))$. Using
the universal property of $\mathcal{M}(\Gamma.Y(x))$, we define
${\llbracket-\rrbracket}_{\Gamma.Y(x)}$ as the unique extension of
$\mathcal{M}^{\bullet}(\bm{p}_{x})\circ{\llbracket-\rrbracket}_{\Gamma}$ that
sends $f_{Y}(x,\bm{q}_{x})$ to $f^{\bullet}_{Y}(x,\bm{q}_{x})$.

We can check that $\bm{p}_{x}$ lifts to a morphism
$\bm{p}_{x}:(\Gamma.Y(x),{\llbracket-\rrbracket}_{\Gamma.Y(x)})\to(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$
in $\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$.

We now show that
$((\Gamma.Y(x),{\llbracket-\rrbracket}_{\Gamma.Y(x)}),\bm{p}_{x})$ represents
the functor ${Y_{0}}_{\mid x}$. Let
$(\Delta,{\llbracket-\rrbracket}_{\Delta})$ be another object of
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$, with a morphism
$\rho:(\Delta,{\llbracket-\rrbracket}_{\Delta})\to(\Gamma,{\llbracket-\rrbracket}_{\Gamma})$
and an element $y:{Y_{0}}_{\mid
x}((\Delta,{\llbracket-\rrbracket}_{\Delta}),\rho)$. Unfolding the
definitions, we have $y:Y(\Delta,x[\rho])$ with ${\llbracket
f_{Y}(x[\rho],y)\rrbracket}_{\Delta}=f_{Y}^{\bullet}(x[\rho],y)$.

The local representability of $Y$ implies that there is a unique morphism
$\widetilde{\rho}:\Delta\to\Gamma.Y(x)$ in $\mathcal{C}$ such that
$\bm{p}_{x}\circ\widetilde{\rho}=\rho$ and $\bm{q}_{x}[\widetilde{\rho}]=y$.
We have to show that this morphism lifts to
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{M}^{\bullet}}$, i.e. that the following
square commutes:

${\mathcal{M}^{\bullet}(\Gamma.Y(x))}$${\mathcal{M}^{\bullet}(\Delta)}$${\mathcal{M}(\Gamma.Y(x))}$${\mathcal{M}(\Delta)}$$\scriptstyle{\mathcal{M}^{\bullet}(\widetilde{\rho})}$$\scriptstyle{\mathcal{M}(\widetilde{\rho})}$$\scriptstyle{{\llbracket-\rrbracket}_{\Gamma.Y(x)}}$$\scriptstyle{{\llbracket-\rrbracket}_{\Delta}}$

By the universal property of $\mathcal{M}(\Gamma.Y(x))$, it suffices to show
that $f_{Y}(x,\bm{q}_{x})$ is mapped to the same element by the compositions
$\mathcal{M}^{\bullet}(\widetilde{\rho})\circ{\llbracket-\rrbracket}_{\Gamma.Y(x)}$
and ${\llbracket-\rrbracket}_{\Delta}\circ\mathcal{M}(\widetilde{\rho})$. We
compute $\mathcal{M}^{\bullet}(\widetilde{\rho})({\llbracket
f_{Y}(x,\bm{q}_{x})\rrbracket}_{\Gamma.Y(x)})=\mathcal{M}^{\bullet}(\widetilde{\rho})(f_{Y}^{\bullet}(x,\bm{q}_{x}))=f_{Y}^{\bullet}(x[\rho],y)$
and
${\llbracket\mathcal{M}(\widetilde{\rho})(f_{Y}(x,\bm{q}_{x}))\rrbracket}_{\Delta}={\llbracket
f_{Y}(x[\rho],y)\rrbracket}_{\Delta}=f_{Y}^{\bullet}(x[\rho],y)$.

This completes the proof that
$((\Gamma.Y(x),{\llbracket-\rrbracket}_{\Gamma.Y(x)}),\bm{p}_{x})$ represents
the functor ${Y_{0}}_{\mid x}$.

We have proven that ${Y_{0}}_{\mid x}$ is representable for every $x$, i.e.
that $Y_{0}$ is locally representable. The first projections
$Y_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),x)\to Y(\Gamma,x)$ strictly
preserve the chosen representing objects.

###  A.4 Proofs of relative induction principles

######  Proof A.18 (Proof of Theorem 5.3).

We consider the category
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}[\mathbf{Scone}_{\mathbb{S}^{\bullet}}]$
of sections of $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$.

By Lemma A.11, the category
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}[\mathbf{Scone}_{\mathbb{S}^{\bullet}}]$
has a terminal object. We equip it with the structure of a higher-order
renaming algebra $(\mathsf{Var}_{0},\mathsf{var}_{0})$ over
$(F\circ\pi_{0}):\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}[\mathbf{Scone}_{\mathbb{S}^{\bullet}}]\to\mathcal{S}$
as follows:

$\displaystyle\mathsf{Var}_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),A)\triangleq\\{a:\mathsf{Var}(\Gamma,A)\mid{\llbracket\mathsf{var}(\Gamma,a)\rrbracket}_{\Gamma}=\mathsf{var}^{\bullet}(\Gamma,{\llbracket
A\rrbracket}_{\Gamma},a)\\},$
$\displaystyle\mathsf{var}_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),A,a)\triangleq\mathsf{var}(\Gamma,a).$

By Lemma A.14, the action of $F:\mathcal{R}\to\mathcal{S}$ on variables is
compatible with $\mathcal{S}_{F}$. By Lemma A.16, the presheaf family
$\mathsf{Var}_{0}$ is locally representable and the first projections
$\mathsf{Var}_{0}((\Gamma,{\llbracket-\rrbracket}_{\Gamma}),A)\to\mathsf{Var}(\Gamma,A)$
strictly preserve context extensions. By initiality of $\mathcal{R}$ among
first-order renaming algebras, we obtain a section $H$ of $\pi_{0}$ in the
category of first-order renaming algebras.

We thus have a section ${\llbracket-\rrbracket}\triangleq
H^{\ast}({\llbracket-\rrbracket}_{0})$ of
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ in $\mathbf{Psh}(\mathcal{R})$. The
action of $H$ on variables proves that it satisfies the equality
${\llbracket\mathsf{var}_{A}(x)\rrbracket}=\mathsf{var}^{\bullet}({\llbracket
A\rrbracket},x)$.

##  Appendix B Example: Syntactic parametricity

In this appendix, we show how our constructions can be combined to obtain a
syntactic parametricity translation for a dependent type theory with
universes. Syntactic parametricity [9, 5] refers to the situation where the
result of the translation itself consists of types and terms from the syntax,
as opposed to metatheoretic entities such as sets or presheaves.

Syntactic parametricity is an interesting application of our methods because
the motives and methods of the induction are given over some category (here
the syntax), but the result of the induction is only obtained over some other
category (here the terminal category, selecting the empty context). We
construct a displayed higher-order model and its
$\mathbf{Scone}$-contextualization in presheaves over the syntax, but we only
look at the section of its externalization, and never obtain a section of the
full $\mathbf{Scone}$-contextualization.

Let $\mathcal{T}$ be a dependent type theory with a hierarchy of Coquand
universes [12, 30], such that types at every level are closed under
$\Pi$-types. This means that a higher-order model of $\mathcal{T}$ consists of
the following data, where every line quantifies over a universe level
$i\in\mathbb{N}$:

$\displaystyle\mathsf{Ty}_{i}:\mathrm{Set},$
$\displaystyle\mathsf{Tm}_{i}:\mathsf{Ty}_{i}\to\mathrm{Set},$
$\displaystyle\mathcal{U}_{i}:\mathsf{Ty}_{i+1},$
$\displaystyle\mathsf{El}_{i}:\mathsf{Tm}(\mathcal{U}_{i})\cong\mathsf{Ty}_{i},$
$\displaystyle\mathsf{Lift}_{i}:\mathsf{Ty}_{i}\to\mathsf{Ty}_{i+1},$
$\displaystyle\mathsf{lift}_{i}:\mathsf{Tm}_{i}(A)\cong\mathsf{Tm}_{i+1}(\mathsf{Lift}_{i}(A)),$
$\displaystyle\Pi:(A:\mathsf{Ty}_{i})\to(\mathsf{Tm}_{i}(A)\to\mathsf{Ty}_{i})\to\mathsf{Ty}_{i},$
$\displaystyle\mathsf{app}:\mathsf{Tm}_{i}(\Pi(A,B))\cong((a:\mathsf{Tm}_{i}(A))\to\mathsf{Tm}_{i}(B(a))).$

We write $\mathcal{S}$ for the syntax of $\mathcal{T}$, that is the initial
first-order model of $\mathcal{T}$; the constructions of the paper generalize
to this theory.

We construct, internally to $\mathbf{Psh}(\mathcal{S})$, a displayed higher-
order model $\mathbb{S}^{\bullet}$ over $\mathsf{Tele}_{\mathbb{S}}$:

  * •

A displayed type over $A:\mathbb{S}.\mathsf{Ty}_{i}$ is a type family

$A^{\bullet}:\mathbb{S}.\mathsf{Tm}(A)\to\mathbb{S}.\mathsf{Ty}_{i}.$

  * •

A displayed term of type $A^{\bullet}$ over $a:\mathbb{S}.\mathsf{Tm}(A)$ is
an element

$a^{\bullet}:\mathbb{S}.\mathsf{Tm}(A^{\bullet}(a)).$

  * •

The displayed universe $\mathcal{U}^{\bullet}_{i}$ is defined as

$\mathcal{U}^{\bullet}_{i}\triangleq\lambda
A\mapsto\Pi(\mathsf{El}(A),\mathcal{U}_{i}),$

so that we have an isomorphism
$\mathcal{U}^{\bullet}_{i}(A)\cong\mathsf{Ty}^{\bullet}_{i}(\mathsf{El}_{i}(A))$.

  * •

The displayed lifting operation $\mathsf{Lift}^{\bullet}_{i}$ is defined by

$\mathsf{Lift}^{\bullet}_{i}(A^{\bullet})\triangleq\lambda
a\mapsto\mathsf{Lift}_{i}(A^{\bullet}(\mathsf{lift}_{i}^{-1}(a)));$

we have an isomorphism
$\mathsf{Tm}^{\bullet}_{i}(A^{\bullet},a)\cong\mathsf{Tm}^{\bullet}_{i+1}(\mathsf{Lift}^{\bullet}_{i}(A^{\bullet}),\mathsf{lift}_{i}(a))$.

  * •

The displayed $\Pi$-type $\Pi^{\bullet}(A^{\bullet},B^{\bullet})$ is defined
as

$\Pi^{\bullet}(A^{\bullet},B^{\bullet})\triangleq\lambda
f\mapsto(\Pi(A,\lambda a\mapsto\Pi(A^{\bullet}(a),\lambda a^{\bullet}\mapsto
B^{\bullet}(a^{\bullet},\mathsf{app}(f,a)))).$

By the induction principle of $\mathcal{S}$ relative to
$1_{\mathcal{S}}:1_{\mathbf{Cat}}\to\mathcal{S}$, we have a section
${\llbracket-\rrbracket}$ of
$1_{\mathcal{S}}^{\ast}(\mathbf{Scone}_{\mathbb{S}^{\bullet}})$. Let $f$ be
any closed term of $\mathcal{S}$ of type $(A:\mathcal{U}_{0})\to A\to A$.

Then ${\llbracket f\rrbracket}$ is a closed term of $\mathcal{S}$ of type
${\llbracket(A:\mathcal{U}_{0})\to A\to A\rrbracket}(f)$ witnessing the fact
that $f$ satisfies parametricity. Using the computation rules of
${\llbracket-\rrbracket}$, we can compute

$\displaystyle{\llbracket(A:\mathcal{U}_{0})\to A\to A\rrbracket}(f)$
$\displaystyle\quad=(A:\mathcal{U}_{0})(A^{\bullet}:A\to\mathcal{U}_{0})\to{\llbracket\lambda
A\mapsto A\to A\rrbracket}(A^{\bullet},f(A))$
$\displaystyle\quad=(A:\mathcal{U}_{0})(A^{\bullet}:A\to\mathcal{U}_{0})(a:A)(a^{\bullet}:A^{\bullet}(A))\to{\llbracket\lambda(A,a)\mapsto
A\rrbracket}((A^{\bullet},a^{\bullet}),f(A,a))$
$\displaystyle\quad=(A:\mathcal{U}_{0})(A^{\bullet}:A\to\mathcal{U}_{0})(a:A)(a^{\bullet}:A^{\bullet}(A))\to
A^{\bullet}(f(A,a)).$

##  Appendix C Induction principles for cubical type theories

In this section we state and prove relative induction principles for a minimal
cubical type theory. It should be possible to use these induction principles
(extended to larger cubical type theories) in order to express in our
framework the known proofs of strict canonicity, homotopy canonicity [15] and
normalization [36] for cubical type theory.

######  Definition C.1.

A higher-order cubical algebra is a set $\mathbb{I}$ with two points
$0,1:\mathbb{I}$.  $\lrcorner$

######  Definition C.2.

A first-order cubical algebra is a category $\mathcal{C}$ with a terminal
object $1_{\mathcal{C}}$, along with a locally representable presheaf
$\mathbb{I}$ with two global elements $0,1$.  $\lrcorner$

The cube category $\square$ is the initial first-order cubical algebra.

We consider a minimal cubical type theory $\mathcal{T}_{\mathsf{CTT}}$ with
only $\Pi$-types and path types. A higher-order model of
$\mathcal{T}_{\mathsf{CTT}}$ consists of the following data:

$\displaystyle\mathbb{I}:\mathrm{Set},$ $\displaystyle 0,1:\mathbb{I},$
$\displaystyle\mathsf{Ty}:\mathrm{Set},$
$\displaystyle\mathsf{Tm}:\mathsf{Ty}\to\mathrm{Set},$
$\displaystyle\Pi:(A:\mathsf{Ty})\to(\mathsf{Tm}(A)\to\mathsf{Ty})\to\mathsf{Ty},$
$\displaystyle\mathsf{app}:\mathsf{Tm}(\Pi(A,B))\cong((a:\mathsf{Tm}(A))\to\mathsf{Tm}(B(a))),$
$\displaystyle\mathsf{Path}:(A:\mathbb{I}\to\mathsf{Ty})\to\mathsf{Tm}(A(0))\to\mathsf{Tm}(A(1))\to\mathsf{Ty},$
$\displaystyle\mathsf{papp}:\mathsf{Tm}(\mathsf{Path}(A,x,y))\to(i:\mathbb{I})\to\mathsf{Tm}(A(i)),$
$\displaystyle(p:\mathsf{Tm}(\mathsf{Path}(A,x,y)))\to\mathsf{papp}(p,0)=x,$
$\displaystyle(p:\mathsf{Tm}(\mathsf{Path}(A,x,y)))\to\mathsf{papp}(p,1)=y,$
$\displaystyle\mathsf{plam}:(A:\mathbb{I}\to\mathsf{Ty})\to(p:(i:\mathbb{I})\to\mathsf{Tm}(A(i)))\to\mathsf{Tm}(\mathsf{Path}(A,p(0),p(1))).$

We write $\mathcal{S}_{\mathsf{CTT}}$ for the initial first-order model of
$\mathcal{T}_{\mathsf{CTT}}$.

By the universal property of $\square$, the cubical algebra
$(\mathcal{S}_{\mathsf{CTT}}.\mathbb{I},\mathcal{S}_{\mathsf{CTT}}.0,\mathcal{S}_{\mathsf{CTT}}.1)$
specifies a morphism $F:\square\to\mathcal{S}_{\mathsf{CTT}}$ of first-order
cubical algebras. We pose $\mathcal{S}_{F}\triangleq
F^{\ast}(\mathbf{Tele}_{\mathbb{S}_{\mathsf{CTT}}})$. We write
$\mathsf{int}:\square.\mathbb{I}\to\mathcal{S}_{F}.\mathbb{I}$ for the action
of $F$ on elements of the interval in $\mathbf{Psh}(\square)$.

######  Theorem C.3 (Induction principle relative to
$F:\square\to\mathcal{S}_{\mathrm{CTT}}$).

Let $\mathbb{S}^{\bullet}$ be a displayed higher-order model of CTT over
$\mathcal{S}_{F}$, and assume given the additional data of a function

$\displaystyle\mathsf{int}^{\bullet}:(i:\square.\mathbb{I})\to\mathbb{I}^{\bullet}(\mathsf{int}(i))$

such that

$\displaystyle\mathsf{int}^{\bullet}(0)=0^{\bullet},$
$\displaystyle\mathsf{int}^{\bullet}(1)=1^{\bullet}.$

Then there exists a section ${\llbracket-\rrbracket}$ of
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$. It satisfies the additional equality

$\displaystyle{\llbracket\mathsf{int}(i)\rrbracket}=\mathsf{int}^{\bullet}(i).$

######  Proof C.4.

We consider the category
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}[\mathbf{Scone}_{\mathbb{S}^{\bullet}}]$
of sections of $\mathbf{Scone}_{\mathbb{S}^{\bullet}}$.

By Lemma A.11, the category
$\mathbf{Sect}^{\mathsf{op}}_{\mathcal{T}}[\mathbf{Scone}_{\mathbb{S}^{\bullet}}]$
has a terminal object. We equip it with a higher-order cubical algebra
$(\mathbb{I}_{0},0_{0},1_{0})$ as follows:

$\displaystyle\mathbb{I}_{0}(\Gamma,{\llbracket-\rrbracket}_{\Gamma})\triangleq\\{i:\square.\mathbb{I}(\Gamma)\mid{\llbracket\mathsf{int}(i)\rrbracket}_{\Gamma}=\mathsf{int}^{\bullet}(\Gamma,i)\\},$
$\displaystyle 0_{0}\triangleq\square.0,$ $\displaystyle
1_{0}\triangleq\square.1.$

The required equalities
${\llbracket\mathsf{int}(\square.0)\rrbracket}_{\Gamma}=\mathsf{int}^{\bullet}(\Gamma,\square.0)$
and
${\llbracket\mathsf{int}(\square.1)\rrbracket}_{\Gamma}=\mathsf{int}^{\bullet}(\Gamma,\square.1)$
follow from the assumptions $\mathsf{int}^{\bullet}(\square.0)=0^{\bullet}$
and $\mathsf{int}^{\bullet}(\square.1)=1^{\bullet}$.

By Lemma A.14, the action of $F:\square\to\mathcal{S}$ on the elements of
$\square.\mathbb{I}$ is compatible with $\mathcal{S}_{F}$. By Lemma A.16, the
presheaf $\mathbb{I}_{0}$ is locally representable and the first projections
$\mathbb{I}_{0}(\Gamma,{\llbracket-\rrbracket}_{\Gamma})\to\square.\mathbb{I}(\Gamma)$
strictly preserve context extensions. By initiality of $\square$ among first-
order cubical algebras, we obtain a section $H$ of $\pi_{0}$ in the category
of first-order cubical algebras.

We thus have a section ${\llbracket-\rrbracket}\triangleq
H^{\ast}({\llbracket-\rrbracket}_{0})$ of
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$ in $\mathbf{Psh}(\square)$. The action
of $H$ on elements of the interval proves that ${\llbracket-\rrbracket}$
satisfies the equality
${\llbracket\mathsf{int}(i)\rrbracket}=\mathsf{int}^{\bullet}(i)$.

######  Definition C.5.

Let $\mathcal{C}$ be a first-order model of $\mathcal{T}_{\mathsf{CTT}}$. A
higher-order cubical renaming algebra $\mathbb{C}$ over $\mathcal{C}$ consists
of a higher-order renaming algebra
$(\mathbb{C}.\mathsf{Var},\mathbb{C}.\mathsf{var})$ over $\mathcal{C}$, a
higher-order cubical algebra
$(\mathbb{C}.\mathbb{I},\mathbb{C}.0,\mathbb{C}.1)$, and an operation

$\mathbb{C}.\mathsf{int}:\mathbb{C}.\mathbb{I}\to\mathcal{C}.\mathbb{I}(1_{\mathcal{C}})$

such that $\mathbb{C}.\mathsf{int}(0)=0$ and $\mathbb{C}.\mathsf{int}(1)=1$.
$\lrcorner$

######  Definition C.6.

Let $\mathcal{D}$ be a first-order model of $\mathcal{T}_{\mathsf{CTT}}$. A
first-order cubical renaming algebra over $\mathcal{D}$ is a category
$\mathcal{C}$ with a terminal object along with a functor
$F:\mathcal{C}\to\mathcal{D}$ that preserves the terminal object and with the
structure of a global higher-order cubical renaming algebra $\mathbb{C}$ over
$F^{\ast}(\mathsf{Tele}_{\mathbb{D}})$ such that both $\mathbb{C}.\mathbb{I}$
and $\mathbb{C}.\mathsf{Var}$ are locally representable and both
$\mathbb{C}.\mathsf{int}$ and $\mathbb{C}.\mathsf{var}$ strictly preserve
context extensions.  $\lrcorner$

The category $\mathcal{A}_{\square}$ of cubical renamings (or category of
atomic cubical contexts and substitutions) is the initial first-order cubical
renaming algebra over $\mathcal{S}_{\mathsf{CTT}}$. We write $G$ for the
functor $G:\mathcal{A}_{\square}\to\mathcal{S}_{\mathsf{CTT}}$, and pose
$\mathcal{S}_{G}\triangleq
G^{\ast}(\mathbf{Tele}_{\mathbb{S}_{\mathsf{CTT}}})$.

######  Theorem C.7 (Induction principle relative to
$F:\mathcal{A}_{\square}\to\mathcal{S}_{\mathrm{CTT}}$).

Let $\mathbb{S}^{\bullet}$ be a displayed higher-order model of CTT over
$\mathcal{S}_{G}$, and assume given the additional data of functions

$\displaystyle\mathsf{var}^{\bullet}:\forall A\
(A^{\bullet}:\mathsf{Ty}^{\bullet}(A))\
(a:\mathsf{Var}(A))\to\mathsf{Tm}^{\bullet}(A^{\bullet},\mathsf{var}(a)),$
$\displaystyle\mathsf{int}^{\bullet}:(i:\square.\mathbb{I})\to\mathbb{I}^{\bullet}(\mathsf{int}(i))$

such that

$\displaystyle\mathsf{int}^{\bullet}(0)=0^{\bullet},$
$\displaystyle\mathsf{int}^{\bullet}(1)=1^{\bullet}.$

Then there exists a section ${\llbracket-\rrbracket}$ of
$\mathbf{Scone}_{\mathbb{S}^{\bullet}}$. It satisfies the additional
equalities

$\displaystyle{\llbracket\mathsf{var}_{A}(a)\rrbracket}=\mathsf{var}^{\bullet}({\llbracket
A\rrbracket},a),$
$\displaystyle{\llbracket\mathsf{int}(i)\rrbracket}=\mathsf{int}^{\bullet}(i).$

######  Proof C.8.

By the same methods as the proofs of Theorem 5.3 and Theorem C.3.