# Kripke-Joyal forcing for type theory
and uniform fibrations

Steve Awodey  Department of Philosophy, Carnegie Mellon University, USA
<EMAIL_ADDRESS>,  Nicola Gambino  School of Mathematics, University of Leeds,
UK<EMAIL_ADDRESS>and  Sina Hazratpour  Department of Mathematics,
Johns Hopkins University, USA<EMAIL_ADDRESS>
(Date: October 27th, 2021)

###### Abstract.

We introduce a new method for precisely relating certain kinds of algebraic
structures in a presheaf category and judgements of its internal type theory.
The method provides a systematic way to organise complex diagrammatic
reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an
application, we prove several properties of algebraic weak factorisation
systems considered in Homotopy Type Theory.

## Introduction

In one of the seminal papers on topos theory [10], the links between algebraic
topology and mathematical logic are described as being only embryonic. Since
then, however, the situation has changed dramatically, thanks to the discovery
of deep connections between Quillen’s homotopical algebra [38] and Martin-Löf
type theory [34], which have given rise to Homotopy Type Theory [49] and
Voevodsky’s Univalent Foundations programme [50]. At the core of these
connections is the precise link between the orthogonality property of a weak
factorisation system (wfs for short) and the axioms for identity types [6,
18].

Presheaf categories play a fundamental role in this context because of the
abundance of wfs’s and model structures on them [14]. For applications in both
type theory [15] and homotopical algebra [39], however, it is sometimes useful
to work with refinements of wfs’s known as algebraic weak factorisation
systems (awfs’s for short) [23, 24], where maps satisfying an orthogonality
property are replaced by maps equipped with algebraic structure, providing
diagonal fillers for lifting problems and satisfying suitable uniformity
conditions. The theory of awfs’s is analogous to that of wfs’s and is
supported by a myriad of examples [11, 12], including the notions of a uniform
Kan fibration studied in Homotopy Type Theory [1, 7, 22, 41, 45, 46]. Yet,
working with awfs’s diagrammatically can be very complex, since the algebraic
structure on a map is in general not unique, and thus needs to be carried
around explicitly. Because of this, the construction of some important objects
(such as that of fibration structures on a given map) using only diagrams can
be a daunting task.

An alternative approach is provided by what may be called the _internal type
theory_ of a presheaf category, which is a highly expressive extensional
dependent type theory [33, 37, 42], in which it is possible to handle not only
the basic categorical structure, but also locally cartesian closed structure.
This idea, suggested by Thierry Coquand [16], has been successfully applied to
Homotopy Type Theory in [35], where parts of the theory of uniform fibrations
were developed in type-theoretic terms. As we will see here, this approach
makes it feasible to write down, say, the object of fibration structures on a
map and reason about it formally. At present, however, in order to link these
two approaches one needs to unfold the interpretation of the internal type
theory into the presheaf category [27], which can be a difficult and laborious
process due to the subtleties introduced by the iterated type dependency.

Our first main contribution is to introduce and develop a new tool to relate
the category-theoretic and the type-theoretic methods for describing
structures in presheaf categories: namely, we extend the Kripke-Joyal forcing
of the higher-order logic of a presheaf category $\tE$ — a powerful, long-
established, technique of categorical logic [32, 36] — to a precisely stated
internal type theory of $\tE$. In particular, we show how Kripke-Joyal forcing
for this type theory allows us to test the validity of type-theoretic
judgements in $\tE$ (4.8), unfold explicitly what forcing amounts to for
various forms of type, such as dependent products (4.16), which are very
important for our applications, and relate it precisely to the ordinary
forcing of higher-order logic (4.19). This technique then also permits
intricate type-theoretic constructions of bespoke _classifying types_ which,
via forcing, represent familiar and important fibrations of structures (as
studied in [44, 47]), a possibility that promises many further applications.

The second main contribution of the paper is to the study of the awfs’s
considered in Homotopy Type Theory, using a combination of the new Kripke-
Joyal forcing for the internal type theory and the usual internal reasoning
therein. We thereby reconcile the category-theoretic and type-theoretic
descriptions of awfs’s considered in [1, 9, 22, 41, 45, 46] and give simple
proofs of several properties of cofibrations and uniform (trivial) fibrations.
In particular, we use Kripke-Joyal forcing to provide a type-theoretic
characterisation of cofibrations (5.6) and a new proof that the pointed
endofunctor of cofibrant partial elements admits the structure of a monad
6.7).

Importantly, we show how the uniformity condition that is part of the
definition of a uniform (trivial) fibration arises naturally from the forcing
conditions for dependent products (7.5). We also use Kripke-Joyal forcing to
provide a new, simpler, proof that the uniform fibration structures on a map
are exactly the algebra structures for a pointed endofunctor (7.7). With these
results in place, we then give an account of the basic properties of uniform
fibrations, combining category-theoretic and type-theoretic reasoning. In
particular, we describe type-theoretically the object of uniform fibration
structures on a map (8.7) and use it to construct a universal uniform
fibration (8.9). We also describe the homotopical semantics of identity types
as path types (9.4).

We hope that these applications demonstrate the utility of Kripke-Joyal
forcing for researchers in mathematical logic, category theory and algebraic
topology. We should also mention that, while our applications are to the
theory of awfs’s and Homotopy Type Theory, our Kripke-Joyal forcing for type
theory is applicable to many other kinds of algebraic structures that may
occur on presheaves, a topic that we leave for future research.

In order to briefly explain our approach in more detail, let us recall that
the standard Kripke-Joyal forcing provides a way to test the validity of a
formula of the internal logic of a presheaf category
$\tE=[{\mathbb{C}}^{\smash{\mathrm{op}}},\mathop{\mathbf{Set}}]$. Given a
formula $\sigma\colon X\to\Omega$, i.e. a map into subobject classifier of
$\tE$, and a generalised element $x\colon\mathsf{y}c\to X$ (where
$\mathsf{y}c$ is the Yoneda embedding applied to $c\in\cC$), we say that $c$
forces $\sigma(x)$ if there exists a (necessarily unique) map as indicated by
the dotted arrow in the diagram

${\\{x\colon
X\mid\sigma(x)\\}}$${1}$${\mathsf{y}c}$${X}$${\Omega\mathrlap{,}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{x}$$\scriptstyle{\sigma}$

where $\\{x\colon X\mid\sigma(x)\\}\rightarrowtail X$ is the subobject of $X$
obtained by pullback of the subobject classifier $\mathsf{true}\colon
1\to\Omega$ along $\sigma$. In order to introduce our Kripke-Joyal forcing, we
follow [2] and set up the internal type theory of $\tE$ by regarding types as
maps into the Hofmann-Streicher universe $U$ in $\tE$ associated to an
inaccessible cardinal $\kappa$ in $\mathop{\mathbf{Set}}$ [28], an approach
which deals correctly with coherence issues [26, 37]. Then, given a type
$\alpha\colon X\to U$ and a generalised element $x\colon\mathsf{y}c\to X$, we
define our Kripke-Joyal forcing by saying that $c$ forces
$a\mathord{\,:\,}\alpha(x)$ if we have a (no longer unique) map as indicated
by the dotted arrow in the diagram

${X.\alpha}$${E}$${\mathsf{y}c}$${X}$${U\mathrlap{,}}$$\scriptstyle{\pi}$$\scriptstyle{x}$$\scriptstyle{(x,a)}$$\scriptstyle{\alpha}$

where $X.\alpha\to X$ is the display map obtained by pullback of the small map
classifier $\pi\colon E\to U$, in the sense of [30], along $\alpha$. As is the
case for Kripke-Joyal forcing of logical formulas, unfolding this condition
recursively according to the form of the type $\alpha$ provides a quasi-
mechanical method to determine necessary and sufficient conditions for the
validity of type-theoretic judgements in $\tE$, something which may be
difficult to obtain by other means.

Our approach to the internal type theory of $\tE$ also allows us to obtain
some new results regarding the relationship between propositions and types in
a presheaf category. In particular, we show how the image factorisation of the
small map classifier provides a convenient way of expressing the operation of
propositional truncation in the type theory (2.4). We use this to provide a
precise account of the relationship between provability of formulas and
inhabitation of associated types (2.5 and 2.7), which is of independent
interest. Finally, we note that our Kripke-Joyal forcing semantics for type
theory is _complete_ with respect to the standard notion of deduction for
Martin-Löf type theory (4.26), in the same way that conventional Kripke
semantics is complete for (intuitionistic) first-order logic, something that
fails for Kripke-Joyal forcing for higher-order logic.

Outline of the paper. The paper is divided into two parts. The first part,
which includes Sections 1, 2, 3 and 4, sets up the general framework,
definition and fundamental results on Kripke-Joyal forcing for the presheaf
type theory. The second part, which includes Sections 5, 6, 7, 8 and 9,
applies Kripke-Joyal forcing to the study of cofibrations, partial elements,
uniform trivial fibrations, uniform fibrations and path types, respectively.
We end the paper in Section 10 with some directions for future work.

Notation. For a category $\tC$ and $X,Y\in\tC$, we write $\tC(X,Y)$ for the
class of maps from $X$ to $Y$. For maps $f\colon X\to Y$ and $g\colon Y\to Z$,
we write $g\circ f$ or simply $gf$ for their composite. For $X\in\tC$, we
write $\operatorname{id}_{X}\colon X\to X$ for the identity map at $X$. We
write $0$ and $1$ for the initial and terminal object, $X\times Y$ for
product, $X+Y$ for coproduct, and more generally $X\times_{Z}Y$ for pullback
and $X+_{Z}Y$ for pushout. Given categories $\tC$ and $\tD$ and functors
$F\colon\tC\to\tD$ and $G\colon\tD\to\tC$, we write $F\dashv G$ to mean that
$F$ is left adjoint to $G$. In this case, there is a family of natural
bijections $\tC(X,GA)\cong\tD(FX,A)$, for $X\in\tC$ and $A\in\tD$. The
transpose of a map $f$ (in either direction) is written $f^{\sharp}$. As
usual, unit and counit of the adjunction are denoted
$\eta\colon\operatorname{id}_{\tC}\rightarrow GF$ and $\varepsilon\colon
FG\rightarrow\operatorname{id}_{\tD}$. For a category $\tE$ and $X\in\tE$, we
write $\tE/_{X}$ for the slice category of objects over $X$.

Throughout the paper, we shall work assuming a fixed inaccessible cardinal
$\kappa$.111Alternatively, we could have assumed an internal full subcategory
of $\tE$ closed under the appropriate category-theoretic operations. We say
that a set is $\kappa$-small if it has cardinality less than $\kappa$. We say
that a category is locally small or locally $\kappa$-small if its hom-classes
are sets or $\kappa$-small sets, respectively. Similarly, we say that a
category is small or $\kappa$-small if its class of objects is a set and it is
locally small or its class of objects is $\kappa$-small and it is locally
$\kappa$-small, respectively. We write $\mathop{\mathbf{Set}}$ for the
category of sets and functions, ${\mathop{\mathbf{Set}}}^{\bullet}$ for the
category of pointed sets and point-preserving functions,
${\mathop{\mathbf{Set}}}_{\kappa}$ for the category of $\kappa$-small sets and
functions and ${\mathop{\mathbf{Set}}}^{\bullet}_{\kappa}$ for the category of
pointed $\kappa$-small sets.

Acknowledgements. We are grateful to Thierry Coquand and Andy Pitts for
helpful conversations on the topic of this paper and comments on a draft
version of it. Steve Awodey and Nicola Gambino are grateful for the support of
the Centre for Advanced Study at the Norwegian Academy of Science and Letters,
where this research was begun. Awodey was also supported by the Air Force
Office of Scientific Research under MURI grant FA9550-15-1-0053 and award
number FA9550-21-1-0009. Gambino was supported by EPSRC via grant EP/V002325/1
and AFOSR under agreements FA9550-17-1-0290 and FA9550-21-1-0007. The work in
this paper was carried out while Sina Haztratpour was a research fellow at the
University of Leeds, supported by AFOSR under agreement FA9550-17-1-0290.

##  1\. Presheaf categories

### Preliminaries

For a small category $\cC$, we write $\mathrm{Psh}(\cC)$ for the category of
presheaves over $\cC$ and $\mathsf{y}\colon\cC\to\mathrm{Psh}(\cC)$ for the
Yoneda embedding. Sometimes we identify objects and maps in $\cC$ with the
representable presheaves and natural transformations between them.
Furthermore, for a presheaf $X$, we often identify elements $x\in X(c)$ with
maps $x\colon\mathsf{y}c\to X$, as permitted by the Yoneda lemma. For
$X\in\mathrm{Psh}(\cC)$, we write $\int\\!X$ for its category of elements.
Recall the equivalence of categories

$\textstyle\mathrm{Psh}(\cC)/_{X}\simeq\mathrm{Psh}(\int\\!X)\mathrlap{.}$
(1.1)

If $X=\mathsf{y}c$, then $\int\\!X=\cC/_{c}$ and we have an equivalence of
categories

$\mathrm{Psh}(\cC)/_{\mathsf{y}c}\simeq\mathrm{Psh}(\cC/_{c})\mathrlap{.}$
(1.2)

Let us now fix a small category $\cC$ and define
$\tE=_{\mathrm{def}}\mathrm{Psh}(\cC)$. We now review some of the basic
structure of $\tE$ in order to fix notation. Foremost, $\tE$ is locally
cartesian closed, i.e. it has a terminal object $1$ and all of its slice
categories $\tE/_{X}$ are cartesian closed. Thus for every $f\colon Y\to X$
the pullback functor ${f}^{*}\colon\tE/_{X}\to\tE/_{Y}$ has both a left and a
right adjoint, written $\Sigma_{f}\colon\tE/_{Y}\to\tE/_{X}$ and
$\Pi_{f}\colon\tE/_{Y}\to\tE/_{X}$, respectively. The action of $\Sigma_{f}$
is given simply by composition with $f\colon Y\to X$.

### Small maps

We introduce the notion of a small map in $\tE$, which is determined by the
Grothendieck universe of $\kappa$-small sets in the ambient set theory.

######  Definition 1.1.

  1. (i)

We say $A\in\tE$ is small if all its values are small sets.

  2. (ii)

We say that $p\colon A\to X$ in $\tE$ is a small map if, for every
$x\colon\mathsf{y}c\to X$, the presheaf $A_{x}$ obtained by the pullback

${A_{x}}$${A}$${\mathsf{y}c}$${X}$$\scriptstyle{p}$$\scriptstyle{x}$

is small.

Observe that (ii) is equivalent to the condition that for every
$x\colon\mathsf{y}c\to X$ the set of all lifts $a\colon\mathsf{y}c\to A$
across $p\colon A\to X$, so $pa=x$, is small.

We write $\tS$ for the class of small maps in $\tE$. For $X\in\tE$, we write
$\tS/_{X}$ for the full subcategory of $\tE/_{X}$ spanned by small maps. The
category $\tE$ admits a classifier for small maps (cf. [3, Definition 57]),
given by the Hofmann-Streicher universe $U\in\tE$ [28], which is defined by
letting, for $c\in\cC$,

$U(c)=_{\mathrm{def}}\mathrm{Obj}\big{[}{(\cC/_{c})}^{\smash{\mathrm{op}}}\,,{\mathop{\mathbf{Set}}}_{\kappa}\big{]}\,.$
(1.3)

Explicitly, an element $\alpha\in U(c)$ is a presheaf on the slice category
$\cC/_{c}$ whose values are small sets. Note that we consider $U(c)$ as a set.
The action on $U$ of an arrow $d\to c$ in $\cC$ is by precomposition with the
composition functor $\cC/_{d}\to\cC/_{c}$. Similarly, define $E\in\tE$ for
$c\in\cC$ by letting,

$E(c)=_{\mathrm{def}}\mathrm{Obj}\big{[}{(\cC/_{c})}^{\smash{\mathrm{op}}}\,,{\mathop{\mathbf{Set}}}^{\bullet}_{\kappa}\big{]}\,.$

Thus, an element $\alpha\in E(c)$ is a contravariant functor on the slice
category $\cC/_{c}$ whose values are _pointed_ small sets. The forgetful
functor
${\mathop{\mathbf{Set}}}^{\bullet}_{\kappa}\to{\mathop{\mathbf{Set}}}_{\kappa}$
induces a natural transformation

$\pi\colon E\to U$ (1.4)

by composition. We call $\pi$ the small map classifier. This terminology is
justified by the fact that $\pi$ is small and, for every small map $p\colon
A\to X$, there exists a pullback diagram

${A}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{p}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(1.5)

Indeed, given a small map $p\colon A\to X$, a canonical map $\alpha$ can be
defined as follows. For $c\in\cC$ and $x\in X(c)$ we require an element
$\alpha_{x}\in U(c)$, which is a presheaf
$\alpha_{x}\colon{{\cC}/_{c}}^{\smash{\mathrm{op}}}\to\mathop{\mathbf{Set}}_{\kappa}$.
This is defined for $f\colon d\to c$ by,

$\alpha_{x}(f)=\\{a\in A(d)\ |\ p_{d}(a)=x.f\\}\mathrlap{,}$ (1.6)

which is the set of all $a$ making the following commute,

${\mathsf{y}d}$${A}$${\mathsf{y}c}$${X{.}}$$\scriptstyle{a}$$\scriptstyle{f}$$\scriptstyle{p}$$\scriptstyle{x}$

Note that the values of $\alpha_{x}$ are small, as $p\colon A\to X$ is a small
map. We call $\alpha\colon X\to U$ the characteristic map of $p\colon A\to X$
and say that $p$ is _classified_ by $\alpha$.

We introduce some notation for canonical pullbacks of $\pi\colon E\to U$.
First, for each $\alpha\colon\mathsf{y}c\to U$, there is a canonical pullback
square

${\mathsf{y}c.\alpha}$${E}$${\mathsf{y}c}$${U\mathrlap{,}}$$\scriptstyle{{p}_{\mathchoice{\raisebox{-2.0pt}{$\scriptstyle\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptscriptstyle\alpha$}}}}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(1.7)

given by taking $\mathsf{y}c.\alpha$ at $d\in\cC$ to be
$(\mathsf{y}c.\alpha)(d)\ =_{\mathrm{def}}\ \coprod_{f\in\cC(d,c)}\alpha(f)$.
Note that this is the object of
$\tE/_{\mathsf{y}c}\simeq\mathrm{Psh}(\cC/_{c})$ associated to
$\alpha\colon{{\cC}/_{c}}^{\smash{\mathrm{op}}}\to\mathop{\mathbf{Set}}_{\kappa}$
under (1.2) . The rest of the pullback in (1.7) is then evident.

This assignment then determines a choice of pullback for each $\alpha\colon
X\to U$,

${X.\alpha}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{{p}_{\mathchoice{\raisebox{-2.0pt}{$\scriptstyle\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptscriptstyle\alpha$}}}}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(1.8)

We call $X.\alpha$ the comprehension of $\alpha$ with respect to $U$ and
${p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}}\colon
X.\alpha\to X$ the display map associated to $\alpha$. Since $\pi$ is a small
map, so is $X.\alpha\to X$. In this way, every small map is isomorphic to a
display map. Explicitly, for every small map $p\colon A\to X$, there is a
diagram

${A}$${X.\alpha}$${E}$${X}$${U\mathrlap{,}}$$\scriptstyle{p}$$\scriptstyle{\cong}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(1.9)

where $\alpha$ is the characteristic map of $p$. In this situation, we say
that the small map $p$ is displayed. We summarise the notation for these
equivalent notions:

$p\colon A\to X\text{ small map}\mathrlap{,}\qquad\alpha\colon X\to
U\mathrlap{,}\qquad{p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}}\colon
X.\alpha\to X\text{ display map}\mathrlap{.}$

In the following, all three points of view will be exploited.

######  Remark 1.2.

Let $X$ be an object of $\tE=\mathrm{Psh}(\cC)$ and consider the slice topos
$\tE/_{X}$. Up to the equivalence of categories (1.1), this is the presheaf
topos $\mathrm{Psh}(\int\\!X)$, with a notion of small map according to 1.1,
and an associated small map classifier $\pi_{X}\colon E_{X}\to U_{X}$. One can
show that this map is obtained by composition (and whiskering) of the
presheaves $E$ and $U$ (and the natural transformation $\pi\colon E\to U$)
with the forgetful functor
${(\int\\!X)}^{\smash{\mathrm{op}}}\to{\cC}^{\smash{\mathrm{op}}}$. In
particular, $E_{X}(c,x)=E(c)$ and $U_{X}(c,x)=U(c)$, for $c$ in $\cC$ and
$x\in X(c)$. In $\tE/_{X}$, the small map classifier $\pi_{X}\colon E_{X}\to
U_{X}$ corresponds under (1.1) to the base change $X^{*}\pi$ of the small map
classifier $\pi$ in $\tE$,

${X^{*}E}$${E\times X}$${E}$${X^{*}U}$${U\times
X}$${U\mathrlap{.}}$$\scriptstyle{X^{*}\pi}$$\scriptstyle{\pi\times
X}$$\scriptstyle{\pi}$ (1.10)

Thus in particular,

$\textstyle\mathrm{Psh}(\cC)(X,U)\ \cong\ \mathrm{Psh}(\cC)/_{X}(1,X^{*}U)\
\cong\ \mathrm{Psh}(\int\\!X)(1,U_{X})\,.$ (1.11)

We will sometimes notationally _identify_ a type $\alpha\colon X\to U$ in
$\mathrm{Psh}(\cC)$ with the associated closed type $\alpha\colon 1\to U_{X}$
in $\mathrm{Psh}(\int\\!X)$ under this isomorphism.

### Dependent sums and products of small maps

Small maps are closed under a variety of operations. In particular, the
pullback of a small map along any map $f\colon Y\to X$ is again a small map.
Furthermore, if $p\colon A\to X$ is a small map, then the left and right
adjoints to pullback along $p$ restrict to small maps, in the sense that there
are serially-commuting diagrams as follows.

${\tS/_{A}}$${\tS/_{X}}$${\tE/_{A}}$${\tE/_{X}}$$\scriptstyle{\Sigma_{p}}$$\scriptstyle{{p}^{*}}$$\scriptstyle{\Sigma_{p}}$$\scriptstyle{{p}^{*}}$
${\tS/_{X}}$${\tS/_{A}}$${\tE/_{X}}$${\tE/_{A}\mathrlap{.}}$$\scriptstyle{{p}^{*}}$$\scriptstyle{\Pi_{p}}$$\scriptstyle{{p}^{*}}$$\scriptstyle{\Pi_{p}}$
(1.12)

The action of these adjoints is reflected into operations on classifying maps,
as we now explain.

Consider first the pullback along any map $f\colon Y\to X$. Given
$\alpha\colon X\to U$ with its small display map
${p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}}\colon
X.\alpha\to X$ the pullback
$f^{*}({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})$
is classified by the composite $\alpha f\colon Y\to U$, by the two pullbacks
lemma,

${Y.\alpha
f}$${X.\alpha}$${E}$${Y}$${X}$${U\mathrlap{.}}$$\scriptstyle{f}$$\scriptstyle{\alpha}$
(1.13)

In this way, the pullback operation on small maps
$f^{*}\colon\tS/_{X}\to\tS/_{Y}$ is induced, up to isomorphism, by
precomposition of the associated characteristic maps, $f^{*}p_{\alpha}\cong
p_{\alpha f}$. We have the following characterisation of the sections of the
small display map $Y.\alpha f\to Y$, which will be used to validate the
substitution rule in 3.4.

######  Proposition 1.3.

Let $f\colon Y\to X$ and $\alpha\colon X\to U$. Then the following data are in
bijective correspondence:

  1. (i)

sections $a\colon Y\to Y.\alpha f$ over $Y$,

  2. (ii)

lifts $a^{\prime}\colon Y\to X.\alpha$ of $f$ across $p_{\alpha}$. ∎

Now consider the left adjoint. Given $\alpha\colon X\to U$ and $\beta\colon
X.\alpha\to U$, let $p\colon X.\alpha\to X$ and $q\colon X.\alpha.\beta\to
X.\alpha$ be the associated display maps. Since $p$ and $q$ are small, we
obtain a small map $\Sigma_{p}(q)$ in $\tS/_{X}$ by application of the functor
$\Sigma_{p}$ in (1.12). This is given simply by composition, so that
$\Sigma_{p}(q)=_{\mathrm{def}}q\circ p$. Let $\Sigma_{\alpha}(\beta)\colon
X\to U$ be the classifier of $\Sigma_{p}(q)\colon X.\alpha.\beta\to X$, giving
rise to the following pullback diagram in which the map labelled
$\mathsf{pair}_{\alpha,\beta}$ is the canonical one.

${X.\Sigma_{\alpha}(\beta)}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{\mathsf{pair}_{\alpha,\beta}}$$\scriptstyle{\Sigma_{\alpha}(\beta)}$
(1.14)

Note that there is an isomorphism $X.\alpha.\beta\cong
X.\Sigma_{\alpha}(\beta)$ over $X$. We therefore obtain maps $\mathsf{p}_{1}$
and $\mathsf{p}_{2}$ fitting into the diagrams

${X.\Sigma_{\alpha}(\beta)}$${E}$${X}$${U\mathrlap{,}}$$\scriptstyle{\mathsf{p}_{1}}$$\scriptstyle{\alpha}$
${X.\Sigma_{\alpha}(\beta)}$${E}$${X.\alpha}$${U\mathrlap{.}}$$\scriptstyle{\mathsf{p}_{2}}$$\scriptstyle{\beta}$
(1.15)

This description implies the following characterisation of the sections of the
display map $X.\Sigma_{\alpha}(\beta)\to X$. It is essentially contained
already in [42], and will be used to show the validity of the rules for
dependent sum types in 3.9.

######  Proposition 1.4.

Let $\alpha\colon X\to U$ and $\beta\colon X.\alpha\to U$. Then the following
data are in bijective correspondence:

  1. (i)

pairs of sections $a\colon X\to X.\alpha$ and $b\colon X\to X.\beta(a)$, both
over $X$,

  2. (ii)

sections $c\colon X\to X.\Sigma_{\alpha}(\beta)$ over $X$. ∎

As shown in [2], the operation mapping $\alpha$ and $\beta$ to
$\Sigma_{\alpha}(\beta)$ can be internalised in $\tE$, by making use of the
polynomial functor $P\colon\tE\to\tE$ associated to the map $\pi\colon E\to
U$, in the sense of [20], i.e. the composite

${\tE}$${\tE/_{E}}$${\tE/_{U}}$${\tE\mathrlap{.}}$$\scriptstyle{(-)\times
E}$$\scriptstyle{\Pi_{\pi}}$$\scriptstyle{\Sigma_{U}}$ (1.16)

Indeed, there is a pullback diagram

${Q}$${E}$${P(U)}$${U\mathrlap{,}}$$\scriptstyle{\mathsf{pair}}$$\scriptstyle{\Sigma}$

such that, for every $\alpha$ and $\beta$ as above, the diagram in (1.14) is
given by a pasting of the form

${X.\Sigma_{\alpha}(\beta)}$${Q}$${E}$${X}$${P(U)}$${U\mathrlap{,}}$$\scriptstyle{\mathsf{pair}}$$\scriptstyle{(\alpha,\beta)}$$\scriptstyle{\Sigma}$

where $(\alpha,\beta)\colon X\to P(U)$ is determined by the universal property
of $P(U)$, and $Q$ can be seen as the object of pairs of sections $(a,b)$ as
in 1.4. In particular, the classifying map $\Sigma_{\alpha}(\beta)\colon X\to
U$ can be defined as the composite $\Sigma(\alpha,\beta)$. This approach is
important to validate the so-called Beck-Chevalley condition, which expresses
the strict commutation between type-formation and substitution.

We now consider the right adjoint. With $p\colon X.\alpha\to X$ and $q\colon
X.\alpha.\beta\to X.\alpha$ as before, let $\Pi_{\alpha}(\beta)$ be the
classifier of the small map $\Pi_{p}(q)$, giving rise to a pullback diagram of
the form

${X.\Pi_{\alpha}(\beta)}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{\lambda_{\alpha,\beta}}$$\scriptstyle{\Pi_{\alpha}(\beta)}$
(1.17)

The map on the left hand side is isomorphic to $\Pi_{p}(q)$ in $\tE/_{X}$ and
hence inherits its universal property. In particular, the counit of the
adjunction induces a map $\varepsilon\colon X.\alpha.\Pi_{\alpha}(\beta)\to
X.\alpha.\beta$ in $\tE/_{X.\alpha}$ which gives rise a commutative diagram

${X.\alpha.\Pi_{\alpha}(\beta)}$${E}$${X.\alpha}$${U\mathrlap{.}}$$\scriptstyle{\mathsf{app}}$$\scriptstyle{\beta}$
(1.18)

The resulting characterisation of the sections of the display map
$X.\Pi_{\alpha}(\beta)\to X$ is also essentially contained already in [42],
and will be used to show the validity of the rules for dependent product types
in 3.11.

######  Proposition 1.5.

Let $\alpha\colon X\to U$ and $\beta\colon X.\alpha\to U$. Then the following
data are in bijective correspondence:

  1. (i)

sections $b\colon X.\alpha\to X.\alpha.\beta$ over $X.\alpha$,

  2. (ii)

sections ${b}^{\sharp}\colon X\to X.\Pi_{\alpha}(\beta)$ over $X$.

The bijection is defined by pullback along $p$ and composition with the counit
$\varepsilon$, i.e. $\varepsilon\circ p^{*}b^{\sharp}=b$. ∎

As was the case for the left adjoint, there is a pullback diagram

${P(E)}$${E}$${P(U)}$${U\mathrlap{,}}$$\scriptstyle{\lambda}$$\scriptstyle{\Pi}$

(now with $P(\pi)$ on the left) such that, for every $\alpha$ and $\beta$ as
above, the diagram in (1.17) is given by a pasting of the form

${X.\Pi_{\alpha}(\beta)}$${P(E)}$${E}$${X}$${P(U)}$${U\mathrlap{.}}$$\scriptstyle{\lambda}$$\scriptstyle{(\alpha,\beta)}$$\scriptstyle{\Pi}$
(1.19)

In particular, the classifying map $\Pi_{\alpha}(\beta)\colon X\to U$ can be
taken to be the composite $\Pi(\alpha,\beta)$. Again, this is used to verify
the Beck-Chevalley condition.

### The subobject classifier

We conclude this review section by introducing some notation and recalling
some basic facts about the subobject classifier of $\tE$, written $\Omega$.
This presheaf is defined by letting, for $c\in\cC$,

$\Omega(c)=_{\mathrm{def}}\mathrm{Obj}\big{[}{(\cC/_{c})}^{\smash{\mathrm{op}}}\,,\mathbf{2}\big{]}\mathrlap{,}$
(1.20)

where $\mathbf{2}$ is the poset $\\{0\leq 1\\}$. The map $\mathsf{true}\colon
1\to\Omega$ is defined by letting its component at $c$ be the constant functor
with value $1$. This classifies subobjects in the sense that for every
subobject $S\rightarrowtail X$, there exists a unique $\sigma\colon
X\to\Omega$ such that

${S}$${1}$${X}$${\Omega}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\sigma}$
(1.21)

is a pullback diagram. In this case, we call $\sigma$ the _characteristic map_
of $S$ and say that $S$ is classified by $\sigma$. We introduce some notation
for the pullbacks of $\mathsf{true}\colon 1\to\Omega$. Given $\sigma\colon
X\to\Omega$, we write

${\\{x\mathord{\,:\,}X\mid\sigma(x)\\}}$${1}$${X}$${\Omega}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\sigma}$
(1.22)

for the subobject which is the pullback of $\mathsf{true}$ along $\sigma$.

For $X\in\tE$, we write $\mathrm{Sub}(X)$ for the poset of subobjects of $X$.
This poset has a Heyting algebra structure, which is reflected into operations
on morphisms from $X$ to $\Omega$, for which we shall use standard logical
notation. For example, if $S,T\in\mathrm{Sub}(X)$ are classified by $\sigma$
and $\tau$, respectively, so that $S=\\{x\mathord{\,:\,}X\ |\ \sigma\\}$ and
$T=\\{x\mathord{\,:\,}X\ |\ \tau\\}$, then we write $\sigma\Rightarrow\tau$
for the classifying map of the Heying implication $S\Rightarrow T$ in
$\mathrm{Sub}(X)$. Thus the subobject $\\{x\mathord{\,:\,}X\ |\
\sigma\Rightarrow\tau\\}$ has the universal property of the Heyting
implication $S\Rightarrow T$.

For our purposes, quantification along small maps will play an important role,
so we introduce some notation for it. Fix $\alpha\colon X\to U$ and let
$p\colon X.\alpha\to X$ be the associated small display map. Pullback along
$p$ restricts to a function
${p}^{*}\colon\mathrm{Sub}(X)\to\mathrm{Sub}(X.\alpha)$, which is a Heyting
algebra morphism with both left and right adjoints, written $\exists_{p}$ and
$\forall_{p}$, respectively. If $S\in\mathrm{Sub}(X.\alpha)$ is classified by
$\sigma\colon X.\alpha\to\Omega$, so that $S=\\{(x,a)\mathord{\,:\,}X.\alpha\
|\ \sigma(x,a)\\}$, then we write $\exists_{\alpha}(\sigma)\colon X\to\Omega$
for the characteristic map of $\exists_{p}(S)\in\mathrm{Sub}(X)$, so that

$\exists_{p}(S)=\exists_{p}\\{(x,a)\mathord{\,:\,}X.\alpha\ |\
\sigma(x,a)\\}=\\{x\mathord{\,:\,}X\ |\ (\exists
a\mathord{\,:\,}\alpha)\sigma(x,a)\\}\mathrlap{.}$

Since $\exists_{p}$ is calculated by taking the image factorisation of the
composite of $S\rightarrowtail X.\alpha$ and $p\colon X.\alpha\to X$, we
obtain a diagram

${S}$${\exists_{p}(S)}$${1}$${X.\alpha}$${X}$${\Omega\mathrlap{,}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{p}$$\scriptstyle{\exists_{\alpha}(\sigma)}$
(1.23)

whose right hand side is a pullback. The universal quantification
$\forall_{p}(S)\in\mathrm{Sub}(X)$ is similarly classified by a map written
$\forall_{\alpha}(\sigma)\colon X\to\Omega$, giving

$\forall_{p}(S)=\forall_{p}\\{(x,a)\mathord{\,:\,}X.\alpha\ |\
\sigma(x,a)\\}=\\{x\mathord{\,:\,}X\ |\ (\forall
a\mathord{\,:\,}\alpha)\sigma(x,a)\\}\mathrlap{.}$

##  2\. Small maps and subobjects

### Subobjects as small maps

There is an evident analogy between the small map classifier $\pi\colon E\to
U$ and the subobject classifier $\mathsf{true}\colon 1\to\Omega$. For one
thing, recall that the universe $U$ was defined in (1.3) by mapping into the
category $\mathop{\mathbf{Set}}_{\kappa}$ of small sets, while the subobject
classifer $\Omega$ was defined in (1.20) by mapping into the category
$\mathbf{2}$ of truth values. Note also the similarity between the
characteristic map of a small map in (1.5) and the characteristic map of a
subobject in (1.21), as well as between the comprehension of a map
$\alpha\colon X\to U$ with respect to $U$ in (1.8) and the comprehension of a
map $\sigma\colon X\to\Omega$ with respect to $\Omega$ in (1.22). Our aim in
this section is to make the relation between $U$ and $\Omega$ more precise.
Anticipating the use to which they will be put in the sequel, we may regard
$U$ as an object of _types_ and $\Omega$ as an object of _propositions_.
Observe first that there is an inclusion functor of truth values into sets,
$\mathbf{2}\hookrightarrow{\mathop{\mathbf{Set}}}_{\kappa}$, where, to be
specific, we take the ordinals $0=\emptyset$, $1=\\{0\\}$, $2=\\{0,1\\}$, the
later ordered by inclusion when regarded as the category $\mathbf{2}$. By the
definitions of $U$ and $\Omega$ in (1.3) and (1.20), respectively, this
functor induces by composition a natural transformation

$\\{-\\}\colon\Omega\to U\mathrlap{,}$ (2.1)

which we call the _inclusion_ of propositions into types.

######  Proposition 2.1.

The inclusion map $\\{-\\}\colon\Omega\to U$ is a monomorphism in $\tE$, and
fits into a pullback diagram of the form

${1}$${E}$${\Omega}$${U\hbox
to0.0pt{.\hss}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\pi}$$\scriptstyle{\\{-\\}}$

  * Proof.

The inclusion functor
$\mathbf{2}\hookrightarrow{\mathop{\mathbf{Set}}}_{\kappa}$ is injective on
objects, and so composing with it is pointwise monic. Similarly, the pullback
is induced via composition by the evident pullback of categories and functors

${\mathbf{1}}$${{\mathop{\mathbf{Set}}}^{\bullet}_{\kappa}}$${\mathbf{2}}$${{\mathop{\mathbf{Set}}}_{\kappa}\mathrlap{.}}$

∎

######  Corollary 2.2.

Let $\sigma\colon X\to\Omega$. Then $X.\\{\sigma\\}=\\{x\colon
X\mid\sigma(x)\\}$, i.e. the comprehension of $\sigma$ with respect to
$\Omega$ is equal, as a subobject of $X$, to the comprehension of its
inclusion $\\{\sigma\\}$ with respect to $U$.

  * Proof.

The display map $p_{\\{\sigma\\}}\colon X.\\{\sigma\\}\to X$ fits into the
diagram

${X.\\{\sigma\\}}$${1}$${E}$${X}$${\Omega}$${U\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\pi}$$\scriptstyle{\sigma}$$\scriptstyle{\\{-\\}}$

Since the outer rectangle is a pullback by definition and the right hand
square is a pullback by 2.1, the left hand square is also a pullback. Thus the
mono $p_{\\{\sigma\\}}\colon X.\\{\sigma\\}\to X$ represents the subobject
$\\{x\colon X\mid\sigma(x)\\}$ classified by $\sigma\colon X\to\Omega$. ∎

######  Remark 2.3.

Propositional comprehension of a subobject $S\rightarrowtail X$ from a map
$\sigma\colon X\to\Omega$ is determined only up to equivalence of the
representing monomorphisms $s\colon S\rightarrowtail X$, whereas for a type
$\alpha\colon X\to U$, we have made a canonical choice $p_{\alpha}\colon
X.\alpha\to X$, which however is only one among many isomorphic small maps
$p\colon A\to X$ classified by $\alpha$. 2.2 says that we can use these
canonical small maps as canonical representatives of subobjects when
convenient. See Section 2 for a warning about this use.

### Propositional truncation

Consider universal small map $\pi\colon E\to U$ and its image factorisation
$E\twoheadrightarrow\mathsf{im}(\pi)\rightarrowtail U$ and let
$\mathsf{supp}\colon U\to\Omega$ be the characteristic map of the subobject
$\mathsf{im}(\pi)\rightarrowtail{U}$, fitting into the pullback diagram

${\mathsf{im}(\pi)}$${1}$${U}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\mathsf{supp}}$

Note that $\mathsf{supp}$ is induced by composition with the functor
${\mathop{\mathbf{Set}}}_{\kappa}\to\mathbf{2}$ mapping every non-empty set to
$1$ and the empty set to $0$. For $\alpha\colon X\to U$, we write
$\mathsf{supp}(\alpha)\colon X\to\Omega$ and call it the support of $\alpha$.
Pasting the factorisation on the left and the pullback diagram of 2.1 on the
right, we obtain

${{E}}$${\mathsf{im}(\pi)}$${1}$${{E}}$${U}$${U}$${\Omega}$${U.}$$\scriptstyle{\pi}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\pi}$$\scriptstyle{\mathsf{supp}}$$\scriptstyle{\\{-\\}}$
(2.2)

Define the truncation operation $\mathsf{tr}\colon U\to U$ to be the composite
of $\mathsf{supp}\colon U\to\Omega$ and $\\{-\\}\colon\Omega\rightarrowtail
U$. For $\alpha\colon X\to U$, we write $\mathsf{tr}(\alpha)\colon X\to U$ for
the composite of $\alpha$ and $\mathsf{tr}$, so that

$\mathsf{tr}(\alpha)=_{\mathrm{def}}\\{\mathsf{supp}(\alpha)\\}\mathrlap{.}$
(2.3)

This operation of propositional truncation behaves like the bracket types of
[4], as stated in the following proposition

######  Proposition 2.4.

Let $p\colon A\to X$ be a small map with characteristic map $\alpha\colon X\to
U$. Then $\mathsf{tr}(\alpha)\colon X\to~{}U$ is a characteristic map for the
image factorisation of $p$, in the sense that there is a pullback diagram

${\mathsf{im}(p)}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{\pi}$$\scriptstyle{\mathsf{tr}(\alpha)}$

Moreover, the composite $\mathsf{supp}\circ\\{-\\}\colon\Omega\to\Omega$ is
the identity map.

  * Proof.

Consider the image factorisation on the left face below, which is a pullback
of the right face, since image factorisations are stable under pullback:

${A}$${\,\,\,{E}\,\,\,}$${{\mathsf{im}(p)}}$${\mathsf{im}(\pi)}$${X}$${U}$${X}$${U\mathrlap{.}}$$\scriptstyle{p}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$
(2.4)

Adjoining diagram (2.2) on the right, we obtain

${{A}}$${\,\,\,{E}\,\,\,}$${{\mathsf{im}(p)}}$${\mathsf{im}(\pi)}$${1}$${{E}}$${X}$${U}$${X}$${U}$${\Omega}$${U\mathrlap{,}}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{\mathsf{supp}}$$\scriptstyle{\\{-\\}}$

which shows that the three-fold composite across the front face below is also
a pullback. Thus

$\mathsf{im}(p)\cong
X.\\{\mathsf{supp}(\alpha)\\}=X.\mathsf{tr}(\alpha)\mathrlap{.}$

Finally, the left hand square in

${1}$${\mathsf{im}(\pi)}$${1}$${\Omega}$${U}$${\Omega}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\\{-\\}}$$\scriptstyle{\mathsf{supp}}$

is a pullback, as can be seen by putting $\\{-\\}$ for $\alpha$ in (2.4) and
using $\mathsf{im}(\Omega.\\{-\\})=\mathsf{im}(\mathsf{true})=\mathsf{true}$,
since $\mathsf{true}\colon 1\to\Omega$ is monic. The right hand square is a
pullback by definition. Thus the outer rectangle is a pullback, and so the
composite $\mathsf{supp}\circ\\{-\\}$ must be the identity, since it is the
characteristic map of $\mathsf{true}\colon 1\rightarrowtail\Omega$. ∎

### Propositions and types

Subobjects and small maps can be combined, but some care is required in
working with their respective characteristic maps. For example, fix
$\alpha\colon X\to U$ and let $p\colon X.\alpha\to X$ be the associated
display map. Then consider $\sigma\colon X.\alpha\to\Omega$ and let
$S=\\{(x,a)\mathord{\,:\,}X.\alpha\mid\sigma(x,a)\\}$ be the associated
subobject,

${S}$${X.\alpha}$${X\mathrlap{.}}$$\scriptstyle{p}$ (2.5)

By Corollary 2.2, $S=X.\alpha.\\{\sigma\\}$ as subobjects, and so the
composite $S\to X$ is classified as a small map by
$\Sigma_{\alpha}\\{\sigma\\}\colon X\to U$. Thus $S\to X$ is isomorphic over
$X$ to the asssociated display map,

${S}$${X.\Sigma_{\alpha}\\{\sigma\\}}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{\cong}$$\scriptstyle{\pi}$$\scriptstyle{\Sigma_{\alpha}\\{\sigma\\}}$

Now consider the image factorisation
$S\twoheadrightarrow\exists_{p}(S)\rightarrowtail X$ and the classifier
${\exists_{\alpha}(\sigma)}\colon X\to\Omega$ of the subobject
$\exists_{p}(S)\rightarrowtail X$, as in (1.23). Composing with the inclusion
$\\{-\\}\colon\Omega\rightarrowtail U$, we can compare the map
$\\{\exists_{\alpha}(\sigma)\\}\colon X\to U$ to the propositional truncation
$\mathsf{tr}(\Sigma_{\alpha}\\{\sigma\\})\colon X\to U$, which also classifies
the image $\exists_{p}(S)\rightarrowtail X$ (as a small map), by Proposition
2.4. Indeed, since $\mathsf{tr}=\\{-\\}\circ\mathsf{supp}$, and $\\{-\\}$ is
monic, it suffices to compare the maps $\exists_{\alpha}(\sigma)\colon
X\to\Omega$ and $\mathsf{supp}(\Sigma_{\alpha}\\{\sigma\\})\colon X\to\Omega$.
Since these are characteristic maps into $\Omega$, they are equal if and only
if the associated subobjects of $X$ are the same, which is true since both are
$\mathsf{im}(S)\rightarrowtail X$. Thus we have
$\\{\exists_{\alpha}(\sigma)\\}=\mathsf{tr}(\Sigma_{\alpha}\\{\sigma\\})$ as
maps from $X$ to $U$.

Now consider the universal quantification, and compare
$\\{\forall_{\alpha}(\sigma)\\}$ with $\Pi_{\alpha}\\{\sigma\\}$. Again we
have the subobject $S\rightarrowtail X.\alpha$ of (2.5) classified by
$\sigma\colon X.\alpha\to\Omega$, as well as its classifier as a small map
$\\{\sigma\\}\colon X.\alpha\to U$. Applying $\Pi_{p}$ along $X.\alpha\to X$
gives a small map $q\colon X.\Pi_{\alpha}\\{\sigma\\}\to X$ classified by
$\Pi_{\alpha}\\{\sigma\\}\colon X\to U$. Since $\Pi_{p}$ preserves
monomorphisms, $q\colon X.\Pi_{\alpha}\\{\sigma\\}\to X$ is monic and so
determines a subobject of $X$, which by definition is
$\forall_{p}(S)\rightarrowtail X$. The classifying map of this subobject is
then $\forall_{\alpha}(\sigma)\colon X\to\Omega$. Finally, composing again
with the inclusion $\\{-\\}\colon\Omega\rightarrowtail U$ we can compare the
maps

$\\{\forall_{\alpha}(\sigma)\\}\colon X\to
U\mathrlap{,}\qquad\Pi_{\alpha}\\{\sigma\\}\colon X\to U\mathrlap{.}$ (2.6)

But now there is no reason why these maps should be equal. What we can say is
that their supports agree, because they classify the same subobject of $X$,
and therefore

$\forall_{\alpha}(\sigma)=\mathsf{supp}\\{\forall_{\alpha}(\sigma)\\}=\mathsf{supp}(\Pi_{\alpha}\\{\sigma\\}).$

Bearing this lesson in mind, we have the following relationship between the
operations on propositions $\sigma\colon X\to\Omega$ and on types
$\alpha\colon X\to U$, stated in terms of equations between maps into
$\Omega$. This is one variant of the usual propositions-as-types translation
(see 2.7 below for another).

######  Proposition 2.5.

The following equalities hold for maps into $\Omega$, where
$\sigma\,,\tau\colon X\to\Omega$.

  1. (i)

$\mathsf{true}=\mathsf{supp}(\mathsf{1})$,

  2. (ii)

$\mathsf{false}=\mathsf{supp}(\mathsf{0})$,

  3. (iii)

$\sigma\land\tau=\mathsf{supp}(\\{\sigma\\}\times\\{\tau\\})$,

  4. (iv)

$\sigma\lor\tau=\mathsf{supp}(\\{\sigma\\}+\\{\tau\\})$,

  5. (v)

$\sigma\Rightarrow\tau=\mathsf{supp}(\\{\sigma\\}\to\\{\tau\\})$.

For $\alpha\colon X\to U$ and $\sigma\colon X.\alpha\to\Omega$,

  1. (vi)

${\forall_{\alpha}(\sigma)}=\mathsf{supp}(\Pi_{\alpha}\\{\sigma\\})$,

  2. (vii)

${\exists_{\alpha}(\sigma)}=\mathsf{supp}(\Sigma_{\alpha}\\{\sigma\\})$.

######  Remark 2.6.

The equations of 2.5 can be expressed as diagrams in $\tE$ by representing the
operations on subobjects and on small maps internally as maps involving
$\Omega$ and $U$ (as shown in [2]). We illustrate this only for the
quantifiers. Let $P\colon\tE\to\tE$ be the polynomial functor associated to
the map $\pi\colon E\to U$, as defined in (1.16). Dependent sums and
existential quantifiers then give rise to maps $\Sigma\colon P(U)\to U$ and
$\exists\colon P(\Omega)\to\Omega$, respectively. The following square

${P(\Omega)}$${\Omega}$${P(U)}$${U}$$\scriptstyle{\exists}$$\scriptstyle{P\\{-\\}}$$\scriptstyle{\Sigma}$$\scriptstyle{\mathsf{supp}}$

then commutes, since the equation (vii) holds for all $\alpha\colon X\to U$
and $\sigma\colon X.\alpha\mathbin{\shortrightarrow}\Omega$. The direct
analogue for the universal quantifier also holds, of course, by (vi); but
consider instead the following diagram, corresponding to the two maps in
(2.6):

${{P(\Omega)}}$${\Omega}$${{P(U)}}$${U\mathrlap{.}}$$\scriptstyle{\forall}$$\scriptstyle{P\\{-\\}}$$\scriptstyle{\\{-\\}}$$\scriptstyle{\Pi}$
(2.7)

Since the maps in this diagram land in $U$, rather than $\Omega$, we cannot
use the universal property of $\Omega$ to conclude that it commutes.
Nonetheless, it can be shown to commute “up to isomorphism”, which we make
precise next.

### The internal category of types

We have emphasized the analogy between the small map classifier $U$ and the
subobject classifier $\Omega$. There are, of course, also some important
differences; in particular, the universal property of $\Omega$ is stronger
than that of $U$, in that a subobject $S\rightarrowtail X$ has a unique
characteristic map from $X$ to $\Omega$, while for a small map $p\colon A\to
X$, a characteristic map from $X$ to $U$ will usually not be unique. As was
shown in (1.6), however, there is a canonical choice of the characteristic map
of a given small map; moreover, this map is in fact _unique up to isomorphism_
, in a sense that we now make precise.

As was noted in (1), for each $X\in\tE$, the poset of subobjects
$\mathrm{Sub}(X)$ has a stable Heyting algebra structure, which is mirrored by
operations on morphisms from $X$ to $\Omega$. Since the isomorphism
$\mathrm{Sub}(X)\ \cong\ \tE(X,\Omega)$ is natural in $X$, by the Yoneda lemma
there are associated operations on $\Omega$ making it an internal Heyting
algebra in $\tE$. In particular, $\Omega$ is an internal poset, with an
ordering relation $\\{(x,y)\mathord{\,:\,}\Omega\times\Omega\ |\ x\leq
y\\}\rightarrowtail\Omega\times\Omega$, satisfying the condition that for
subobjects $S,T\rightarrowtail X$ with characteristic maps $\sigma,\tau\colon
X\to\Omega$, one has $S\leq T$ if and only if there is a (necessarily unique)
lift as indicated in the following diagram.

${\\{(x,y)\ |\ x\leq y\\}}$${X}$${\Omega\times\Omega\hbox
to0.0pt{.\hss}}$$\scriptstyle{(\sigma,\tau)}$

In much the same way, there is an internal _category_ structure on the object
$U$,

$U_{1}\to U\times U,$

such that for any small maps $A\to X$ and $B\to X$, with characteristic maps
$\alpha,\beta\colon X\to U$, the maps $f\colon A\to B$ in the slice category
over $X$ correspond (uniquely!) to lifts $\vartheta$ of $(\alpha,\beta)\colon
X\to U\times U$, as indicated in the following diagram.

${U_{1}}$${X}$${U\times U\hbox
to0.0pt{.\hss}}$$\scriptstyle{(\alpha,\beta)}$$\scriptstyle{\vartheta}$

Moreover, since by (1.9) the assignment of $p_{\alpha}\colon X.\alpha\to X$ to
$\alpha\colon X\to U$ is essentially surjective onto the objects in the
category $\tS/_{X}$ of small maps, we therefore have an equivalence of
categories,

$\tS/_{X}\ \simeq\ \underline{\tE}(X,\mathbb{U}),$ (2.8)

where $\mathbb{U}=(U,U_{1})$ may be called the _internal category of types_ ,
and the category $\underline{\tE}(X,\mathbb{U})$ consists of objects
$\tE(X,U)$ and morphisms $\tE(X,U_{1})$. Since we shall make no essential use
of (2.8), we only sketch the proof.

First recall the definition (1.3) of the set $U(c)$, for $c\in\cC$, and
consider the corresponding set of morphisms,

$U_{1}(c)=_{\mathrm{def}}\mathrm{Mor}\big{[}{(\cC/_{c})}^{\smash{\mathrm{op}}}\,,{\mathop{\mathbf{Set}}}_{\kappa}\big{]}\,.$
(2.9)

Explicitly, an element $\vartheta\in U_{1}(c)$ is a natural transformation
$\vartheta\colon\alpha\to\beta$ of presheaves $\alpha,\beta\in U(c)$ on the
slice category $\cC/_{c}$ whose values are small sets. The domain and codomain
maps are just those of the functor category
$\big{[}{(\cC/_{c})}^{\smash{\mathrm{op}}}\,,{\mathop{\mathbf{Set}}}_{\kappa}\big{]}$,
as are the identities and composition. Naturality with respect to $d\to c$ in
$\cC$ is given by “whiskering” (i.e. precomposition) with the composition
functor $\cC/d\to\cC/c$.

Now let $c\in\cC$ and assume $\alpha,\beta\colon\mathsf{y}c\to U$, with
associated display maps $p_{\alpha}\colon\mathsf{y}c.\alpha\to\mathsf{y}c$ and
$p_{\beta}\colon\mathsf{y}c.\beta\to\mathsf{y}c$. A map $h\colon p_{\alpha}\to
p_{\beta}$ in $\tS/_{\mathsf{y}c}$ is a morphism in

$\big{(}{{\mathop{\mathbf{Set}}}_{\kappa}}^{{\cC}^{\smash{\mathrm{op}}}}\big{)}{/\mathsf{y}c}\
\simeq\
{{\mathop{\mathbf{Set}}}_{\kappa}}^{{(\cC{/c})}^{\smash{\mathrm{op}}}},$
(2.10)

and therefore corresponds to a unique element $\vartheta$ of $U_{1}(c)$ by
(2.9). One then checks that the equivalence of categories (2.10) indeed
relates $\alpha\colon\mathsf{y}c\to U$ to the display map
$p_{\alpha}\colon\mathsf{y}c.\alpha\to\mathsf{y}c$ in a functorial way (see
(1.7)).

Finally, two maps $\alpha,\beta\colon X\to U$ are said to be _isomorphic_ if
they are so as objects in the category $\underline{\tE}(X,\mathbb{U})$ of
types over $X$ (2.8). In particular, it is in this sense that the diagram
(2.7) commutes up to isomorphism. Indeed, using this notion, we can give a
more precise statement than Proposition 2.5 of the relationship between
propositions $\sigma\colon X\to\Omega$ and types $\alpha\colon X\to U$.

######  Proposition 2.7.

The following isomorphisms hold for maps into $U$.

  1. (i)

$\\{\mathsf{true}\\}\cong\mathsf{1}$,

  2. (ii)

$\\{\mathsf{false}\\}\cong\mathsf{0}$,

  3. (iii)

$\\{\sigma\land\tau\\}\cong\\{\sigma\\}\times\\{\tau\\}$,

  4. (iv)

$\\{\sigma\lor\tau\\}\cong\mathsf{tr}\big{(}\\{\sigma\\}+\\{\tau\\}\big{)}$,

  5. (v)

$\\{\sigma\Rightarrow\tau\\}\cong\\{\sigma\\}\to\\{\tau\\}$.

For $\alpha\colon X\to U$ and $\sigma\colon X.\alpha\to\Omega$,

  1. (vi)

$\\{\forall_{\alpha}(\sigma)\\}\cong\Pi_{\alpha}\\{\sigma\\}$,

  2. (vii)

$\\{\exists_{\alpha}(\sigma)\\}\cong\mathsf{tr}(\Sigma_{\alpha}\\{\sigma\\})$.

  * Proof.

We have an adjunction $\mathsf{supp}\dashv\\{-\\}$, so that for all
$\sigma\colon X\to\Omega$ and $\alpha\colon X\to U$, there is a natural
isomorphism $\Omega^{X}(\mathsf{supp}(\alpha),\sigma)\ \cong\
\mathbb{U}^{X}(\alpha,\\{\sigma\\})$. Now use the fact that
$\mathsf{supp}(\\{\sigma\\})=\sigma$ and
$\\{\mathsf{supp}(\alpha)\\}=\mathsf{tr}(\alpha)$. ∎

##  3\. The type theory of a presheaf category

### The category with families

The aim of this section is to introduce precisely a dependent type theory
associated to the presheaf category $\tE$. In order to do so, we begin by
saying how $\tE$ determines a category with families via the universe
$\pi\colon E\to U$ (as in [2]). We then consider what forms of type are
supported by this category with families. We will not specify all the
deduction rules that are valid in $\tE$, but rather focus on those that will
be most important for our applications, namely those concerning dependent
sums, dependent products and the subobject classifier.

In Sections 5 and 8, we will extend this type theory with additional forms of
type, corresponding to additional structure that may be assumed on $\tE$. We
begin by introducing some terminology.

######  Definition 3.1 (The category with families $\mathcal{T}_{\tE}$).

  * •

A context is an object of $\tE$. We use letters $\Gamma,\Delta,\ldots$ to
denote contexts.

  * •

For a context $\Gamma$, a type in context $\Gamma$ is a morphism
$\alpha\colon\Gamma\to U$ in $\tE$. In this case, we write
$\Gamma\vdash\alpha\colon U$.

  * •

Given two types $\alpha_{1}$ and $\alpha_{2}$ in context $\Gamma$, we say that
$\alpha_{1}$ and $\alpha_{2}$ are _judgementally equal_ if they are equal as
morphisms from $\Gamma$ to $U$. In this case, we write
$\Gamma\vdash\alpha_{1}=\alpha_{2}\colon U$.

  * •

For a context $\Gamma$ and a type $\alpha$ in context $\Gamma$, an element of
$\alpha$ in context $\Gamma$ is a map $a\colon\Gamma\to E$ such that

${\Gamma}$${E}$${\Gamma}$${U\mathrlap{.}}$$\scriptstyle{a}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(3.1)

commutes. In this case, we write $\Gamma\vdash a\colon\alpha$.

  * •

For two terms $a_{1}$ and $a_{2}$ of type $\alpha$ in context $\Gamma$, we say
that $a_{1}$ and $a_{2}$ are _judgementally equal_ elements of $\alpha$ if
they are equal as morphisms from $\Gamma$ to $E$. We then write $\Gamma\vdash
a_{1}=a_{2}\colon\alpha$.

For a context $\Gamma$ and a type $\alpha$ in context $\Gamma$, we have a new
context $\Gamma.\alpha$, obtained by the pullback in (1.8). This is the
operation of context extension. We sometimes refer to a map $a$ with codomain
$E$ simply as an _element_ , leaving implicit that it is an element of the
type $\pi\circ a$.

######  Remark 3.2.

Thus elements of a type $\alpha$ in context $\Gamma$ are in bijective
correspondence with sections of its display map $\Gamma.\alpha\to\Gamma$.
Indeed, an element $a$ of $\alpha$ in context $\Gamma$, as defined above,
determines the diagram

${\Gamma}$${\Gamma.\alpha}$${E}$${\Gamma}$${U\mathrlap{.}}$$\scriptstyle{a}$$\scriptstyle{\operatorname{id}_{\Gamma}}$$\scriptstyle{(\operatorname{id}_{\Gamma},a)}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$

The empty context is the terminal object $1$ of $\tE$. A type in the empty
context, which is just a map $\alpha\colon 1\to U$ is called a closed type. In
this case, we simply write $\vdash\alpha\colon U$. As a special case of (1.8),
for a closed type $\alpha$, we obtain

${1.\alpha}$${E}$${1}$${U\mathrlap{.}}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$

Such closed types correspond up to isomorphism to small presheaves
$A\colon{\cC}^{\smash{\mathrm{op}}}\to\mathop{\mathbf{Set}}_{\kappa}$.

######  Definition 3.3.

Let $\Gamma$ and $\Delta$ be contexts. A context morphism from $\Delta$ to
$\Gamma$ is a map $t\colon\Delta\to\Gamma$ in $\tE$.

Context morphisms, which may be regarded as (tuples of) _terms_ , act on types
and elements via the operation of substitution, which we now define.

######  Notation 3.4 (Substitution).

Fix a context morphism $t\colon\Delta\to\Gamma$. For a type $\alpha$ in
context $\Gamma$, we define a type $\alpha(t)$ in context $\Delta$, obtained
by substitution of $t$ in $\alpha$, by letting

$\alpha(t)=_{\mathrm{def}}\alpha\circ t\mathrlap{.}$ (3.2)

We then have the following diagram of the associated context extensions, in
which the left square is also a pullback.

${{\Delta.\alpha(t)}}$${\Gamma.\alpha}$${E}$${\Delta}$${\Gamma}$${U\mathrlap{.}}$$\scriptstyle{\pi}$$\scriptstyle{t}$$\scriptstyle{\alpha}$

If $a$ is term of type $\alpha$ in context $\Gamma$, we define the
substitution of $t$ in $a$ to be the element $a(t)$ of type $\alpha(t)$ in
context $\Delta$ defined by letting $a(t)=_{\mathrm{def}}a\circ t$. Note that
$a(t)$ is indeed an element of $\alpha(t)$ since

${\Delta}$${\Gamma}$${E}$${\Delta}$${\Gamma}$${U}$$\scriptstyle{t}$$\scriptstyle{a}$$\scriptstyle{\pi}$$\scriptstyle{t}$$\scriptstyle{\alpha}$

commutes if the right hand square does. Note that substitution satisfies the
expected laws $\alpha(t)(s)=\alpha(ts)$, etc.

We introduce some auxiliary notation for substitutions of a context morphism
of the form $(\operatorname{id}_{\Gamma},a)\colon\Gamma\to\Gamma.\alpha$ as in
3.2. In this case, given a type $\beta$ in context $\Gamma.\alpha$, we write
the substitution of $(\operatorname{id}_{\Gamma},a)$ in $\beta$ as $\beta(a)$,
rather than the more precise $\beta(\operatorname{id}_{\Gamma},a)$. Similarly,
if $b$ is a term of type $\beta$ in context $\Gamma.\alpha$, we write $b(a)$
instead of $b(\operatorname{id}_{\Gamma},a)$. The interpretation of these
terms and types is displayed in the diagram

${\Gamma}$${\Gamma.\alpha}$${E}$${\Gamma}$${\Gamma.\alpha}$${U\mathrlap{.}}$$\scriptstyle{(\operatorname{id}_{\Gamma},a)}$$\scriptstyle{(\operatorname{id}_{\Gamma},a)}$$\scriptstyle{\pi}$$\scriptstyle{(\operatorname{id}_{\Gamma},a)}$$\scriptstyle{\beta}$

This notation allows us to derive the substitution rule

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
a\mathord{\,:\,}\alpha\qquad\Gamma,\alpha\vdash b\mathord{\,:\,}\beta$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=110.52718pt\hbox{}}}\hbox{\kern
22.43443pt\hbox{$\displaystyle\Gamma\vdash
b(a)\mathord{\,:\,}\beta(a)\mathrlap{.}$}}}}$

######  Notation 3.5 (Weakening).

When we perform a substitution along a map of the form
${p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\beta$}}{\raisebox{-2.0pt}{$\textstyle\beta$}}{\raisebox{-2.0pt}{$\scriptstyle\beta$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\beta$}}}\colon\Gamma.\beta\to\Gamma$
for some $\beta\colon\Gamma\to U$, we obtain the diagram

${\Gamma.\beta.\alpha}$${\Gamma.\alpha}$${E}$${\Gamma.\beta}$${\Gamma}$${U\mathrlap{.}}$$\scriptstyle{\pi}$$\scriptstyle{{p}_{\mathchoice{\raisebox{-2.0pt}{$\scriptstyle\displaystyle\beta$}}{\raisebox{-2.0pt}{$\scriptstyle\textstyle\beta$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptstyle\beta$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptscriptstyle\beta$}}}}$$\scriptstyle{\alpha}$

This corresponds to the rule of weakening, which we write as

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\alpha\colon
U\qquad\Gamma\vdash\beta\colon U$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=100.38887pt\hbox{}}}\hbox{\kern
13.281pt\hbox{$\displaystyle\Gamma.\alpha\vdash\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})\colon
U\mathrlap{.}$}}}}$

Note that we write
$\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})$
rather than the more familiar $\beta$ in the conclusion, as this will help us
keep track of the context in which we are working. Analogously, we have
weakening for elements of types, which we write as

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\alpha\colon
U\qquad\Gamma\vdash b\colon\beta$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=96.7625pt\hbox{}}}\hbox{\kern
1.14476pt\hbox{$\displaystyle\Gamma.\alpha\vdash
b({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})\colon\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})\mathrlap{.}$}}}}$

######  Notation 3.6.

Observe that in the context extension diagram (1.8), viz.

${\Gamma.\alpha}$${E}$${\Gamma}$${U\mathrlap{,}}$$\scriptstyle{q_{\alpha}}$$\scriptstyle{{p}_{\mathchoice{\raisebox{-2.0pt}{$\scriptstyle\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\scriptscriptstyle\alpha$}}}}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$
(3.3)

the top arrow $q_{\alpha}\colon\Gamma.\alpha\to E$ gives a canonical element
$q_{\alpha}\colon\alpha$ in the weakened context $\Gamma.\alpha$. This
corresponds to the syntactic rule of introducing a variable, usually expressed
by the judgement $\Gamma,x\colon\alpha\vdash x\colon\alpha$.

We recall a fundamental fact from [2].

######  Theorem 3.7.

Contexts, context morphisms, types, elements, and the context extension
operation, as defined above, form a category with families, denoted
$\mathcal{T}_{\tE}$. ∎

######  Remark 3.8.

By 1.2, the slice category $\tE/_{X}\cong\mathrm{Psh}(\int\\!X)$ also has a
universal small map $\pi_{X}\colon E_{X}\to U_{X}$, and so we can apply the
foregoing construction to obtain a category with families
$\mathcal{T}_{\tE/_{\\!X}}$. Using (1.11), and similar reasoning, one sees
that the contexts, types, elements, etc., of $\mathcal{T}_{\tE/_{\\!X}}$
correspond to those of $\mathcal{T}_{\tE}$ in which the context has the form
$X.(-)$, as in e.g. $X.\Gamma\vdash a\colon\alpha$. We shall not distinguish
between these isomorphic type theories.

### Dependent sum and dependent product types

The category-theoretic structure of $\tE$ and the closure properties of the
class $\tE$ of small maps discussed in Section 1 correspond to well-known
type-theoretic constructions. In particular, the type theory of $\tE$ has
empty type $\mathsf{0}$, a unit type $\mathsf{1}$, sum types $\alpha+\beta$,
dependent sum types $\Sigma_{\alpha}(\beta)$, dependent product types
$\Pi_{\alpha}(\beta)$, a type of propositions $\Omega$ and subset types
$\\{x\mathord{\,:\,}\alpha\mid\sigma\\}$. With these product types
$\alpha\times\beta$ and function types $\alpha\rightarrow\beta$ can be
defined, as explained in 3.12 below. It also has a type of natural numbers
$\mathsf{N}$, as well as many other inductively defined types. We shall not
list the rules for all these types, limiting ourselves to those that will be
most relevant and illustrative, namely dependent sums, dependent products and
propositions.

The statement of the next proposition and its proof make use of the convention
introduced in 3.4. For the proof, see [2].

######  Proposition 3.9 (Rules for dependent sum types).

The following rules are valid in $\tE$.

  * •

Formation: if $\Gamma\vdash\alpha\mathord{\,:\,}U$ and
$\Gamma.\alpha\vdash\beta\mathord{\,:\,}U$, then
$\Gamma\vdash\Sigma_{\alpha}(\beta)\mathord{\,:\,}U$.

  * •

Introduction: if $\Gamma\vdash a\mathord{\,:\,}\alpha$ and $\Gamma\vdash
b\mathord{\,:\,}\beta(a)$ then
$\Gamma\vdash\mathsf{pair}(a,b)\mathord{\,:\,}\Sigma_{\alpha}(\beta)$.

  * •

Elimination: if $\Gamma\vdash t\colon\Sigma_{\alpha}(\beta)$ then
$\Gamma\vdash\mathsf{p}_{1}(t)\colon\alpha$ and
$\Gamma\vdash\mathsf{p}_{2}(t)\colon\beta(\mathsf{p}_{1}(t))$.

  * •

Computation: if $\Gamma\vdash a\mathord{\,:\,}\alpha$ and $\Gamma\vdash
b\mathord{\,:\,}\beta(a)$ then
$\Gamma\vdash\mathsf{p}_{1}(\mathsf{pair}(a,b))=a\mathord{\,:\,}\alpha$ and
$\Gamma\vdash\mathsf{p}_{2}(\mathsf{pair}(a,b))=b\mathord{\,:\,}\beta(a)$.

  * •

Expansion: if $\Gamma\vdash t\colon\Sigma_{\alpha}(\beta)$ then $\Gamma\vdash
t=\mathsf{pair}(\mathsf{p}_{1}(t),\mathsf{p}_{2}(t))\colon\Sigma_{\alpha}(\beta)$.
∎

######  Notation 3.10.

In the statement of the next proposition and below we make use not only of the
convention introduced in 3.4, but also write $\lambda(b)$ instead of
$\lambda((\operatorname{id}_{\Gamma},b^{\sharp}))$ for simplicity.

For the proof of the next statement, see [2].

######  Proposition 3.11 (Rules for dependent product types).

The following rules are valid in $\tE$.

  * •

Formation: if $\Gamma\vdash\alpha\mathord{\,:\,}U$ and
$\Gamma.\alpha\vdash\beta\mathord{\,:\,}U$ then
$\Gamma\vdash\Pi_{\alpha}\beta\mathord{\,:\,}U$.

  * •

Introduction: if $\Gamma.\alpha\vdash b\colon\beta$ then
$\Gamma\vdash\lambda(b)\colon\Pi_{\alpha}(\beta)$.

  * •

Elimination: if $\Gamma\vdash t\mathord{\,:\,}\Pi_{\alpha}(\beta)$ and
$\Gamma\vdash a\mathord{\,:\,}\alpha$ then
$\Gamma\vdash\mathsf{app}(t,a)\colon\beta(a)$.

  * •

Computation: if $\Gamma.\alpha\vdash b\colon\beta$ and $\Gamma\vdash
a\mathord{\,:\,}\alpha$ then
$\Gamma\vdash\mathsf{app}\big{(}\lambda(b),a\big{)}=b(a)\colon\beta(a)$.

  * •

Expansion: if $\Gamma\vdash t\mathord{\,:\,}\Pi_{\alpha}(\beta)$ then
$\Gamma\vdash\lambda(\mathsf{app}(t,q_{\alpha}))=t\colon\Pi_{\alpha}(\beta)$.
∎

######  Notation 3.12 (Product and function types).

The rules for dependent sum and dependent product types of 3.9 and 3.11, in
combination with the weakening operation of 3.5, allow us to define product
and function types and derive deduction rules for them. For
$\alpha\colon\Gamma\to U$ and $\beta\colon\Gamma\to U$, we define the product
type $\alpha\times\beta\colon\Gamma\to U$ and the function type
$\alpha\to\beta\colon\Gamma\to U$ by letting

$\alpha\times\beta=_{\mathrm{def}}\Sigma_{\alpha}\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})\mathrlap{,}\qquad\alpha\to\beta=_{\mathrm{def}}\Pi_{\alpha}\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})\mathrlap{,}$

where we used the notation for weakening introduced in (3.5). We can then
derive the deduction rules

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\alpha\colon
U\quad\Gamma\vdash\beta\colon U$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=90.38885pt\hbox{}}}\hbox{\kern
15.97284pt\hbox{$\displaystyle\Gamma\vdash\alpha\times\beta\colon
U\mathrlap{,}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 1.33345pt\hbox{$\displaystyle\penalty 1\Gamma\vdash
a\colon\alpha\quad\Gamma\vdash b\colon\beta$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=86.79724pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\mathsf{pair}(a,b)\colon\alpha\times\beta$}}}}$

for product types, and the rules

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash\alpha\colon
U\quad\Gamma\vdash\beta\colon U$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=90.38885pt\hbox{}}}\hbox{\kern
16.80618pt\hbox{$\displaystyle\Gamma\vdash\alpha\rightarrow\beta\colon
U\mathrlap{,}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma.\alpha\vdash
b\colon\beta({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}})$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=70.20047pt\hbox{}}}\hbox{\kern
1.7196pt\hbox{$\displaystyle\Gamma\vdash\lambda(b)\colon\alpha\rightarrow\beta$}}}}$

for function types, where we made use of the simplification introduced in
3.10.

######  Notation 3.13 (Constant functions).

In order to be able to manipulate constant functions conveniently, we
introduce a further abuse of notation on top of the one discussed in 3.10. If
$\Gamma\vdash b\colon\beta$, we write
$\Gamma\vdash\lambda(b)\colon\alpha\to\beta$ instead of
$\Gamma\vdash\lambda(b({p}_{\mathchoice{\raisebox{-2.0pt}{$\displaystyle\alpha$}}{\raisebox{-2.0pt}{$\textstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptstyle\alpha$}}{\raisebox{-2.0pt}{$\scriptscriptstyle\alpha$}}}))\colon\alpha\to\beta$,
thereby omitting mention of the weakening in this particular case. This
convention will be used frequently in Section 5.

######  Remark 3.14.

The rules for dependent sum and dependent product types stated in 3.9 and 3.11
imply also many familiar properties of these types. In particular, if
$\Gamma\vdash\alpha\colon U$ and $\Gamma.\alpha\vdash\beta\colon U$ and
$\Gamma.\alpha.\beta\vdash\rho\colon U$, we can prove that there are
isomorphisms of types,

$\displaystyle\textstyle\sum_{x\colon\alpha}\,\sum_{y\mathord{\,:\,}\beta}\,\rho$
$\displaystyle\textstyle\ \cong\
\sum_{z\colon\sum_{x\mathord{\,:\,}\alpha}\,\beta}\,\rho(\mathsf{p}_{1}(z),\mathsf{p}_{2}(z))\mathrlap{,}$
(3.4)
$\displaystyle\textstyle\prod_{x\mathord{\,:\,}\alpha}\,\sum_{y\mathord{\,:\,}\beta}\,\rho$
$\displaystyle\textstyle\ \cong\
\sum_{u\mathord{\,:\,}\prod_{x\mathord{\,:\,}\alpha}\,\beta}\,\prod_{x\mathord{\,:\,}\alpha}\,\rho(x,\mathsf{app}(u,x))\mathrlap{.}$
(3.5)

Also, if $\Gamma\vdash\alpha\colon U$ and $\Gamma.\alpha\vdash\beta\colon U$,
then there is an isomorphism,

$\textstyle\big{(}\sum_{x\mathord{\,:\,}\alpha}\,\beta\big{)}\mathbin{\shortrightarrow}\rho\
\cong\
\prod_{x\mathord{\,:\,}\alpha}\,\big{(}\beta\mathbin{\shortrightarrow}\rho\big{)}\mathrlap{.}$
(3.6)

The soundness of the rules in $\tE$, 3.9 and 3.11, then implies that there are
corresponding isomorphisms in the category of types over $\Gamma$,

$\tS/_{\Gamma}\ \simeq\ \underline{\tE}(\Gamma,\mathbb{U}),$

introduced in (2.8) of section 2. In particular, it follows that the internal
category of types $\mathbb{U}$ is locally cartesian closed, much as the
subobject classifier $\Omega$ is an internal Heyting algebra.

### The type of propositions

We conclude this section by fixing some notation for the closed type
associated to the subobject classifier of $\tE$, which we shall also write
$\Omega$. The elements of this type, to be regarded as propositions, will be
written using the standard logical notation,

$\mathsf{true}\mathrlap{,}\quad\mathsf{false}\mathrlap{,}\quad
a=_{\alpha}b\mathrlap{,}\quad\sigma\land\tau\mathrlap{,}\quad\sigma\lor\tau\mathrlap{,}\quad\sigma\Rightarrow\tau\mathrlap{,}\quad(\forall
x\colon\alpha)\tau(x)\mathrlap{,}\quad(\exists
x\colon\alpha)\tau(x)\mathrlap{.}$

Note that the proposition $a=_{\alpha}b$ is a well-formed element of type
$\Omega$ in context $\Gamma$ when $a$ and $b$ are well-formed elements of type
$\alpha$ in context $\Gamma$. We refer to this as propositional equality; it
is to be distinguished from judgemental equality $a=b\colon\alpha$, relating
two elements of type $\alpha$ (and from $p=q\colon\Omega$, relating two
elements of type $\Omega$). In spite of this, we will sometimes drop the
subscript from propositional equality, when this does not create confusion
(see also 3.16 below).

######  Definition 3.15.

We say that a proposition $\sigma$ in context $\Gamma$ is valid if
$\sigma\colon\Gamma\to\Omega$ factors through $\mathsf{true}\colon
1\to\Omega$. In that case, we write $\Gamma\vdash\sigma$. Similarly, we say
that $\Gamma,\varphi_{1},\ldots,\varphi_{n}$ _implies_ $\varphi$, if the
subobject $\\{\Gamma\mid\varphi_{1}\land\ldots\land\varphi_{n}\\}$ factors
through $\\{\Gamma\mid\varphi\\}$. In this case, we write
$\Gamma,\varphi_{1},\ldots,\varphi_{n}\vdash\varphi$.

Note that $\sigma$ is valid exactly when the associated subobject
$\\{\Gamma\mid\sigma\\}\rightarrowtail\Gamma$ admits a section, and hence is
isomorphic to $\Gamma$.

######  Remark 3.16.

Propositional equality $a=_{\alpha}b\colon\Omega$ serves the purpose of the
_equality types_ $\mathsf{Eq}_{\alpha}(a,b)$ sometimes used in a system of
type theory without a type of propositions. Here judgemental and propositional
equality are equivalent, in the sense that the inference rules

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
a_{1}\colon\alpha\quad\Gamma\vdash a_{2}\colon\alpha\quad\Gamma\vdash
a_{1}=_{\alpha}a_{2}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=141.3584pt\hbox{}}}\hbox{\kern
42.38103pt\hbox{$\displaystyle\Gamma\vdash
a_{1}=a_{2}\colon\alpha$}}}}\qquad\qquad{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
a_{1}\colon\alpha\quad\Gamma\vdash a_{2}\colon\alpha\quad\Gamma\vdash
a_{1}=a_{2}\colon\alpha$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=152.5063pt\hbox{}}}\hbox{\kern
53.52892pt\hbox{$\displaystyle\Gamma\vdash a_{1}=_{\alpha}a_{2}$}}}}$

are derivable. This is sometimes expressed by saying that the type theory of
$\tE$ is extensional, in contrast with recent formulations of Martin-Löf type
theories that are intensional.

##  4\. Kripke-Joyal forcing

### Definition and basic properties

The aim of this section is to give the definition of the Kripke-Joyal
semantics for the type theory $\mathcal{T}_{\tE}$ of the category $\tE$ of
presheaves, introduced in Section 3, and establish some of its key properties.
In particular, we unfold the general definition for each of the main type
forming operations, so as to facilitate the work of subsequent sections.

######  Definition 4.1.

Let $\alpha\colon X\to U$ and $x\colon\mathsf{y}{c}\to X$.

  1. (i)

For $a\colon\mathsf{y}{c}\to E$, we say that $c$ forces $a\colon\alpha(x)$,
written

$c\Vdash a\colon\alpha(x)\,,$

if the following diagram commutes:

${\mathsf{y}{c}}$${E}$${X}$${U\mathrlap{.}}$$\scriptstyle{a}$$\scriptstyle{x}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$

  2. (ii)

For $a,b\colon\mathsf{y}{c}\to E$ such that $c\Vdash a\colon\alpha(x)$ and
$c\Vdash b\colon\alpha(x)$, we say that $c$ forces $a=b\colon\alpha(x)$,
written

$c\Vdash a=b\colon\alpha(x)\,,$

if $a$ and $b$ are equal maps in $\tE$.

######  Remark 4.2.

We provide some equivalent ways of regarding the forcing condition.

  1. (i)

A map $a\colon\mathsf{y}{c}\to E$ such that $c\Vdash a\colon\alpha(x)$ is the
same thing as an element of $\alpha(x)$ in context $\mathsf{y}{c}$. Indeed, we
can rewrite the diagram in 4.1 as

${\mathsf{y}{c}}$${E}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{a}$$\scriptstyle{\pi}$$\scriptstyle{x}$$\scriptstyle{\alpha}$

Consulting (3.1), we see that $c\Vdash a\colon\alpha(x)$ is therefore simply
another notation for $\mathsf{y}{c}\vdash a\colon\alpha(x)$. Even if it is
just an abbreviation, the forcing notation provides an alternate tool for
working with the type theory of $\tE$, when unfolded for the various type
formers, as we shall see later.

  2. (ii)

A map $a\colon\mathsf{y}{c}\to E$ such that $c\Vdash a\colon\alpha(x)$ is the
same thing as a dotted map making the following diagram commute:

${X.\alpha}$${E}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{x}$$\scriptstyle{\alpha}$

As we will see in 4.19, our definition subsumes the Kripke-Joyal forcing for
propositions, which defines $c\Vdash\sigma(x)$ to mean that there is a (now
necessarily unique) map in

${\\{X\mid\sigma\\}}$${1}$${\mathsf{y}{c}}$${X}$${\Omega\mathrlap{.}}$$\scriptstyle{x}$$\scriptstyle{\sigma}$

One of the key differences between forcing for types and forcing for
propositions is that in the forcing condition for types we need to record the
map $a$, as it is not unique in general.

  3. (iii)

A map $a\colon\mathsf{y}{c}\to E$ such that $c\Vdash a\colon\alpha(x)$ also
corresponds uniquely to a section of the display map of
${\alpha(x)}\colon\mathsf{y}{c}\to U$,

${\mathsf{y}{c}.\alpha(x)}$${E}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{x}$$\scriptstyle{\alpha}$

The following statements gather some immediate consequences of 4.1.

######  Lemma 4.3.

Let $\alpha,\beta\colon X\to U$. Then $\alpha=\beta$ if and only if
$c\Vdash\alpha(x)=\beta(x)$ for every $c\in\cC$ and $x\colon\mathsf{y}c\to X$.
∎

For the next lemma, recall that the monotonicity of conventional Kripke
semantics states that if $k\Vdash p$ and $j>k$ then $j\Vdash p$. Something
similar holds in our setting as well.

######  Lemma 4.4 (Monotonicity).

Let $\alpha\colon X\to U$, $x\colon\mathsf{y}{c}\to X$ and
$a\colon\mathsf{y}{c}\to E$. If $c\Vdash a\mathord{\,:\,}\alpha(x)$ then
$d\Vdash a(f)\mathord{\,:\,}\alpha(xf)$ for every $f\colon d\to c$.

  * Proof.

Just precompose the diagram 4.1 with $f\colon d\to c$. ∎

A converse to monotonicity might be stated as follows. Suppose that for every
$f\colon d\to c$, we have $a_{f}\colon\mathsf{y}{d}\to E$ with $d\Vdash
a_{f}\mathord{\,:\,}\alpha(xf)$, and moreover the uniformity condition
$e\Vdash a_{f}(g)=a_{fg}\mathord{\,:\,}\alpha(xfg)$ holds for all $g\colon
e\to d$. Then there is $a\colon\mathsf{y}{c}\to E$ with $c\Vdash
a\mathord{\,:\,}\alpha(x)$, and moreover $d\Vdash
a(f)=a_{f}\mathord{\,:\,}\alpha(xf)$ for all $f\colon d\to c$. This is
trivial, however, because for $a$ we can just take
$a_{\operatorname{id}_{c}}$. What is not so trivial is the analogous statement
for a judgement of the form $X\vdash a\colon\alpha$ when $X$ is not
representable. Since the presheaf $X$ is a colimit of representables, the
validity of such judgements in the internal type theory $\mathcal{T}_{\tE}$
can be related to forcing semantics as follows.

######  Proposition 4.5.

Let $X\vdash\alpha\colon U$. Suppose that for each ${x\colon\mathsf{y}{c}\to
X}$ there is a given element $a_{x}\colon\mathsf{y}{c}\to E$ such that

$c\Vdash a_{x}\mathord{\,:\,}\alpha(x),$ (4.1)

and moreover, the following uniformity condition holds for all $f\colon d\to
c$,

$d\Vdash a_{x}(f)=a_{xf}\mathord{\,:\,}\alpha(xf)\,.$

Then there is a unique element $a\colon X\to E$ such that

$X\vdash a\colon\alpha$ (4.2)

and, for all ${x\colon\mathsf{y}{c}\to X}$,

$c\Vdash a(x)=a_{x}\mathord{\,:\,}\alpha(x)\,.$

  * Proof.

Given any $X\vdash a\colon\alpha$ we can set $a_{x}=_{\mathrm{def}}ax$ for
each ${x\colon\mathsf{y}{c}\to X}$, and we then have $c\Vdash
a_{x}\mathord{\,:\,}\alpha(x)$ by precomposing (3.1) with
${x\colon\mathsf{y}{c}\to X}$. The uniformity condition $d\Vdash
a_{x}(f)=a_{xf}\mathord{\,:\,}\alpha(xf)$ holds because
$a_{x}(f)=(ax)f=a(xf)=a_{xf}$.

To see that any uniform family of elements $(a_{x}\colon\mathsf{y}{c}\to
E)_{x\colon\mathsf{y}{c}\to X}$ arises in this way from a unique $X\vdash
a\colon\alpha$, note that, for each $c$, the family
$(a_{x}\colon\mathsf{y}{c}\to E)_{x\colon\mathsf{y}{c}\to X}$ determines a
function $\mathbf{a}_{c}\colon X(c)\to E(c)$, while the uniformity condition
means that the various functions $\mathbf{a}_{c}$ are natural in $c$, so we
indeed have a natural transformation $a\colon X\to E$. Recall that $X\vdash
a\colon\alpha$ means that this $a\colon X\to E$ makes the diagram (3.1)
commute. This follows from the individual conditions (4.1). ∎

We can summarise 4.5 as follows.

######  Corollary 4.6.

Let $\alpha\colon X\to U$. Then the following data are in bijective
correspondence:

  1. (i)

elements $a\colon X\to E$ such that $X\vdash a\colon\alpha$,

  2. (ii)

uniform families of elements $a_{x}\colon\mathsf{y}{c}\to E$ such that
$c\Vdash a_{x}\colon\alpha(x)$.

Specifically, the bijection is defined by letting
$a_{x}=_{\mathrm{def}}a(x)\colon\alpha(x)$. ∎

######  Proposition 4.7.

Let $\alpha\colon 1\to U$ be a closed type. Then the following data are in
bijective correspondence:

  1. (i)

elements $a\colon 1\to E$ such that $\vdash a\colon\alpha$,

  2. (ii)

uniform families of elements $(a_{c})_{c\in\cC}$, where $c\Vdash
a_{c}\mathord{\,:\,}\alpha$, i.e. such that
$d\Vdash{a_{c}}(f)=a_{d}\mathord{\,:\,}\alpha$, for all $f\colon d\to c$.

  * Proof.

Immediate from 4.6. ∎

When the equivalent conditions of 4.7 hold, we may write $\tE\Vdash
a\colon\alpha$ and say that _$\tE$ forces $a\colon\alpha$_ (or even just that
_$\tE$ forces $\alpha$_). In these terms 4.6 implies the following soundness
and completeness theorem for the $\vdash$ relation of the internal type theory
$\mathcal{T}_{\tE}$ with respect to the Kripke-Joyal forcing relation $\Vdash$
(but also see 4.26).

######  Theorem 4.8 (Soundness and completeness of forcing).

Let $\alpha\colon 1\to U$ be a closed type and $a\colon 1\to E$. Then
$\mathcal{T}_{\tE}\vdash a\colon\alpha$ if and only if $\tE\Vdash
a\colon\alpha$. ∎

### Forcing in slice categories

Since any slice category of a presheaf topos is also a presheaf topos, as
$\mathrm{Psh}(\cC)/_{X}\cong\mathrm{Psh}(\int\\!X)$, 4.1 also determines a
notion of forcing there (for the type theory $\mathcal{T}_{\tE/_{\\!X}}$, see
3.8), which is related to forcing in $\tE$ by the following.

######  Lemma 4.9.

Let $\alpha\colon X\to U$ and $x\colon\mathsf{y}c\to X$. For any
$a\colon\mathsf{y}c\to E$, the following conditions are equivalent.

  1. (i)

$c\Vdash a\mathord{\,:\,}\alpha(x)$ in $\mathrm{Psh}(\cC)$.

  2. (ii)

$(c,x)\Vdash a\mathord{\,:\,}\alpha$ in $\mathrm{Psh}(\int\\!X)$.

  * Proof.

Under the identification of (1.11) (and observing 3.8), the forcing condition
$(c,x)\Vdash a\mathord{\,:\,}\alpha$ states that the diagram on the left below
commutes in $\mathrm{Psh}(\int\\!X)$, where $\pi_{X}$ is the small map
classifier of $\mathrm{Psh}(\int\\!X)$, as in 1.2. But by the specification of
$\pi_{X}$, this is equivalent to the commutativity in $\mathrm{Psh}(\cC)$ of
the diagram on the right, which is what the condition $c\Vdash
a\mathord{\,:\,}\alpha(x)$ means.

${\mathsf{y}(c,x)}$${E_{X}}$${1}$${U_{X}}$$\scriptstyle{a}$$\scriptstyle{\pi_{X}}$$\scriptstyle{\alpha}$
${\mathsf{y}(c)}$${E}$${X}$${U}$$\scriptstyle{a}$$\scriptstyle{x}$$\scriptstyle{\pi}$$\scriptstyle{\alpha}$

∎

######  Remark 4.10.

Let $\alpha\colon X\to U$ and reconsider the bijection of 4.6 between

>   1. (i)
>
> elements $X\vdash a\colon\alpha$,
>
>   2. (ii)
>
> uniform families of elements $c\Vdash a_{x}\colon\alpha(x)$, for all
> $x\colon\mathsf{y}{c}\to X$.
>
>

In light of Lemma 4.9, when we move to the slice category $\tE/_{X}$ where
$\alpha\colon X\to U$ is a _closed type_ , the bijection is then between:

>   1. (i)
>
> elements $\vdash a\colon\alpha$,
>
>   2. (ii)
>
> uniform families of elements $(c,x)\Vdash a_{(c,x)}\colon\alpha$, for all
> $(c,x)\in\int{X}$.
>
>

The latter statement is 4.7.

In conclusion, forcing a _type in context_ $X\vdash a\colon\alpha$ in
$\mathcal{T}_{\tE}$ is equivalent to forcing the corresponding _closed type_
$\vdash a\colon\alpha$ in $\mathcal{T}_{\tE/_{X}}$. Indeed, there is a
bijection between the witnessing elements $a$. We can summarise this as
follows.

######  Proposition 4.11.

Let $\alpha\colon X\to U$ be a type. Then the following data are in bijective
correspondence:

  1. (i)

elements $a\colon X\to E$ such that $\tE/_{X}\Vdash a\colon\alpha$,

  2. (ii)

uniform families of elements $(a_{x})_{(c,x)\in\int X}$, where $c\Vdash
a_{x}\colon\alpha(x)$. ∎

### Forcing for types

We now unfold the definition of forcing with respect to each of the main type-
forming operations of $\mathcal{T}_{\tE}$. We make use thereby of the term
constructors $\mathsf{pair}$, $\mathsf{app}$, etc., of $\mathcal{T}_{\tE}$
that were introduced in Section 3.

######  Proposition 4.12 (Forcing for empty and unit type).

Let $c\in\mathbb{C}$.

  1. (i)

$c\not\Vdash a\colon\mathsf{0}$ for all $a\colon\mathsf{y}{c}\to E$.

  2. (ii)

$c\Vdash a\colon\mathsf{1}$ for a unique $a=*\colon\mathsf{y}{c}\to E$.

  * Proof.

For item (i), if $c\Vdash a\colon\mathsf{0}$, then by item (iii) of 4.2 we
would have a section of the display map
$\mathsf{y}{c}.\mathsf{0}\to\mathsf{y}{c}$, but
$\mathsf{y}{c}.\mathsf{0}=\\{\mathsf{y}{c}\ |\
\bot\\}\rightarrowtail\mathsf{y}{c}$ is the initial object of $\tE$, so this
is impossible, since $\mathsf{y}{c}$ always has at least the element
$\operatorname{id}\colon\mathsf{y}{c}\to\mathsf{y}{c}$.

For item (ii), $c\Vdash a\colon\mathsf{1}$ for every section $a$ of the
display map $\mathsf{y}{c}.\mathsf{1}\to\mathsf{y}{c}$, but
$\mathsf{y}{c}.\mathsf{1}=\\{\mathsf{y}{c}\ |\
\top\\}\rightarrowtail\mathsf{y}{c}$ is the total subobject, so there is
always exactly one such section. ∎

######  Proposition 4.13 (Forcing for sum types).

Let $\alpha,\beta\mathord{\,:\,}X\to U$. For every $x\colon\mathsf{y}{c}\to
X$, the following conditions hold.

  1. (i)

If $c\Vdash a\colon\alpha(x)$ then
$c\Vdash\mathsf{inl}(a)\colon\alpha(x)+\beta(x)$, and if $c\Vdash
b\colon\beta(x)$ then $c\Vdash\mathsf{inr}(b)\colon\alpha(x)+\beta(x)$.

  2. (ii)

If $c\Vdash t\colon\alpha(x)+\beta(x)$ then either $c\Vdash
t=\mathsf{inl}(a)\colon\alpha(x)\mathsf{+}\beta(x)$ for $c\Vdash
a\colon\alpha(x)$ or $c\Vdash
t=\mathsf{inr}(b)\colon\alpha(x)\mathsf{+}\beta(x)$ for $c\Vdash
b\colon\beta(x)$.

  * Proof.

The sum $\alpha+\beta\colon X\to U$ classifies the canonical map from the
coproduct

$[p_{\alpha},p_{\beta}]\colon X.\alpha+X.\beta\to X.$

Now if $c\Vdash a\colon\alpha(x)$ then we have a lift $a\colon\mathsf{y}{c}\to
X.\alpha$ of $x\colon\mathsf{y}{c}\to X$ across the display map
$p_{\alpha}\colon X.\alpha\to X$. Composing with the coproduct inclusion
$\mathsf{inl}\colon X.\alpha\to X.\alpha+X.\beta$ we obtain
$c\Vdash\mathsf{inl}(a)\colon\alpha(x)+\beta(x)$. If instead $c\Vdash
b\colon\beta(x)$ then in the same way we obtain
$c\Vdash\mathsf{inr}(b)\colon\alpha(x)+\beta(x)$. Thus (i).

For (ii), if $c\Vdash t\colon\alpha(x)+\beta(x)$, then there is a lift
$t\colon\mathsf{y}{c}\to X.\alpha+X.\beta$ of $x\colon\mathsf{y}{c}\to X$
across $[p_{\alpha},p_{\beta}]$. Since the representable $\mathsf{y}{c}$ is
indecomposable, the map $t$ must factor through one of the coproduct
inclusions. Thus we either have $c\Vdash
t=\mathsf{inl}(a)\colon\alpha(x)+\beta(x)$ where $c\Vdash a\colon\alpha(x)$ or
we have $c\Vdash t=\mathsf{inr}(b)\colon\alpha(x)+\beta(x)$ where $c\Vdash
b\colon\beta(x)$, as required. ∎

######  Proposition 4.14 (Forcing for dependent sum types).

Let $\alpha\colon X\to U$ and $\beta\colon X.\alpha\to U$. For every
$x\colon\mathsf{y}{c}\to X$, the following conditions hold.

  1. (i)

If $c\Vdash a\colon\alpha(x)$ and $c\Vdash b\colon\beta(a)$, then
$c\Vdash\mathsf{pair}(a,b)\colon(\Sigma_{\alpha}\beta)(x)$.

  2. (ii)

If $c\Vdash t\mathord{\,:\,}(\Sigma_{\alpha}\beta)(x)$, then
$c\Vdash\mathsf{p}_{1}(t)\colon\alpha(x)$ and
$c\Vdash\mathsf{p}_{2}(t)\colon\beta(\mathsf{p}_{1}(t))$.

  * Proof.

The statements (i) and (ii) follow from 3.9 (introduction and elimination) and
item (i) of 4.2. ∎

######  Corollary 4.15 (Forcing for product types).

For $\alpha,\beta\colon X\to U$, the following hold.

  1. (i)

If $c\Vdash a\colon\alpha(x)$ and $c\Vdash b\colon\beta(x)$, then
$c\Vdash\mathsf{pair}(a,b)\colon(\alpha\times\beta)(x)$.

  2. (ii)

If $c\Vdash t\mathord{\,:\,}(\alpha\times\beta)(x)$, then
$c\Vdash\mathsf{p}_{1}(t)\colon\alpha(x)$ and
$c\Vdash\mathsf{p}_{2}(t)\colon\beta(x)$.

  * Proof.

Special case of 4.14 since product types are defined as dependent sum types
(see 3.12). ∎

The next proposition unfolds the forcing condition for elements of the
dependent product type. We see another appearance of the uniformity condition,
which will play a role in our study of uniform fibrations in Section 7. As the
proof shows, this condition arises from the non-pointwise character of
dependent products in presheaves, much like the consideration of “future
possible worlds” in the familiar Kripke semantics of implication $p\Rightarrow
q$.

######  Proposition 4.16 (Forcing for dependent product types).

Let $\alpha\colon X\to U$ and $\beta\colon X.\alpha\to U$. Then for every
$x\colon\mathsf{y}{c}\to X$ we have the following.

  1. (i)

Suppose for every $f\colon d\to c$ and every $d\Vdash
a\mathord{\,:\,}\alpha(xf)$ we are given ${d\Vdash
b_{(f,a)}\mathord{\,:\,}\beta(xf,a)}$, satisfying the following uniformity
condition for all $g\colon e\to d$,

$e\Vdash b_{(f,a)}(g)=b_{(fg,ag)}\colon\beta(xfg,ag).$

Then there is a map $b\colon\mathsf{y}{c}.\alpha\to E$ for which

$c\Vdash\lambda b\mathord{\,:\,}(\Pi_{\alpha}\beta)(x)\mathrlap{,}$

and for all $f\colon d\to c$ and $d\Vdash a\mathord{\,:\,}\alpha(xf)$ we have

${d\Vdash\mathsf{app}((\lambda
b)(f),a)=b_{(f,a)}\mathord{\,:\,}\beta(xf,a)}\mathrlap{.}$

  2. (ii)

Suppose that $c\Vdash t\colon(\Pi_{\alpha}\beta)(x)$. Then for every $f\colon
d\to c$ and every $d\Vdash a\colon\alpha(xf)$, we have

$d\Vdash\mathsf{app}(t(f),a)\colon\beta(xf,a)\,,$

and moreover the following uniformity condition holds for every $g\colon e\to
d$,

$e\Vdash\mathsf{app}(t(f),a)(g)=\mathsf{app}(t(fg),a(g))\colon\beta(xfg,a).$

  * Proof.

We work in the slice category $\tE/{\mathsf{y}{c}.\alpha}$ where the
representables are pairs of the form $(f,a)$ with $f\colon d\to c$ and
$d\Vdash a\colon\alpha(xf)$. Applying 4.11 to the condition in (i) we obtain
$\tE/{\mathsf{y}{c}.\alpha}\Vdash b\colon\beta(x)$, which by 4.8 implies
$\mathcal{T}_{\tE/{\mathsf{y}{c}.\alpha}}\vdash b\colon\beta(x)$. Thus in
$\mathcal{T}$ we have $\mathsf{y}{c}.\alpha\vdash b\colon\beta(x)$ for some
$b\colon\mathsf{y}{c}.\alpha\to E$. By 3.11, therefore,
$\mathsf{y}{c}\vdash\lambda b\colon\Pi_{\alpha}(\beta)(x)$, and hence
$c\Vdash\lambda b\colon\Pi_{\alpha}(\beta)(x)$ by 4.2(i). Then for all
$f\colon d\to c$ and $d\Vdash a\mathord{\,:\,}\alpha(xf)$ we indeed have

$\mathsf{app}((\lambda b)(f),a)=b(f,a)=b_{(f,a)}\mathord{\,:\,}\beta(xf,a)$

by the computation rule of 3.11 and 4.6. Thus (i), as required.

For (ii), take $c\Vdash t\colon(\Pi_{\alpha}\beta)(x)$ and $f\colon d\to c$ so
that $d\Vdash t(f)\colon(\Pi_{\alpha}\beta)(xf)$ by Lemma 4.4. We then have
$\mathsf{y}{d}\vdash t(f)\colon(\Pi_{\alpha}\beta)(xf)$, again by (i) of 4.2.
And similarly for $d\Vdash a\colon\alpha(xf)$, we have $\mathsf{y}{d}\vdash
a\colon\alpha(xf)$. Applying the elimination rule from 3.11 then gives
$\mathsf{y}{d}\vdash\mathsf{app}(t(f),a)\colon\beta(xf,a)$, whence
$d\Vdash\mathsf{app}(t(f),a)\colon\beta(xf,a)$. The uniformity with respect to
$g\colon e\to d$ follows from the corresponding statement in the type theory,
which is proved as usual from the Computation, Expansion, and Substitution
rules. ∎

######  Corollary 4.17 (Forcing for function types).

Let $\alpha\colon X\to U$ and $\beta\colon X\to U$. Then for every
$x\colon\mathsf{y}{c}\to X$ we have the following.

  1. (i)

Suppose for every $f\colon d\to c$ and every $d\Vdash
a\mathord{\,:\,}\alpha(xf)$ we are given $d\Vdash
b_{(f,a)}\mathord{\,:\,}\beta(xf)$, satisfying the following uniformity
condition for all $g\colon e\to d$,

$e\Vdash b_{(f,a)}(g)=b_{(fg,a(g))}\colon\beta(xfg).$

Then there is a map $b\colon\mathsf{y}{c}.\alpha\to E$ for which

$c\Vdash\lambda(b)\mathord{\,:\,}(\alpha\to\beta)(x)\mathrlap{,}$

and for all $f\colon d\to c$ and $d\Vdash a\mathord{\,:\,}\alpha(xf)$ we have

${d\Vdash\mathsf{app}((\lambda
b)(f),a)=b_{(f,a)}\mathord{\,:\,}\beta(xf)}\mathrlap{.}$

  2. (ii)

Suppose that $c\Vdash t\colon(\alpha\to\beta)(x)$. Then for every $f\colon
d\to c$, and every $d\Vdash a\colon\alpha(xf)$, we have

$d\Vdash\mathsf{app}(t(f),a)\colon\beta(xf)\,,$

and moreover the following uniformity condition holds for every $g\colon e\to
d$,

$\mathsf{app}(t(f),a)(g)=\mathsf{app}(t(fg),a(g))\colon\beta(xfg).$

  * Proof.

This is the special case of 4.16 since function types are defined as dependent
product types (see 3.12). ∎

The foregoing forcing statements included detailed information about which
specific terms are forced, on the basis of those assumed as given. While this
information is sometimes useful, it can also be convenient to use the
following simplified _forcing conditions_ which elide this information (to the
extent possible). Except where otherwise indicated, the individual forcing
statements of the form $c\Vdash t\colon\alpha$ then assert that _there merely
exists_ a term $t$ such that $c\Vdash t\colon\alpha$.

######  Corollary 4.18 (Forcing conditions).

Let the types $\alpha$, $\beta$, etc., be as in the corresponding propositions
above. Then for every $x\colon\mathsf{y}{c}\to X$ we have the following
equivalences.

  1. (i)

$c\Vdash a\colon\mathsf{0}$ if and only if $a\neq a$.

  2. (ii)

$c\Vdash a\colon\mathsf{1}$ if and only if $a=*$.

  3. (iii)

$c\Vdash t\colon(\alpha+\beta)(x)$ if and only if $c\Vdash a\colon\alpha(x)$
or $c\Vdash b\colon\beta(x)$,

  4. (iv)

$c\Vdash t\colon(\alpha\times\beta)(x)$ if and only if $c\Vdash
a\colon\alpha(x)$ and $c\Vdash b\colon\beta(x)$.

  5. (v)

$c\Vdash t\colon(\Sigma_{\alpha}\beta)(x)$ if and only if $c\Vdash
a\colon\alpha(x)$ and $c\Vdash b\colon\beta(a)$.

  6. (vi)

$c\Vdash t\colon({\alpha}\to{\beta})(x)$ if and only if $d\Vdash
b_{(f,a)}\mathord{\,:\,}\beta(xf)$ for all $f\colon d\to c$ and $d\Vdash
a\mathord{\,:\,}\alpha(xf)$, and $e\Vdash
b_{(f,a)}(g)=b_{(fg,ag)}\colon\beta(xfg)$ for all $g\colon e\to d$.

  7. (vii)

$c\Vdash t\colon(\Pi_{\alpha}\beta)(x)$ if and only if $d\Vdash
b_{(f,a)}\mathord{\,:\,}\beta(xf,a)$ for all $f\colon d\to c$ and $d\Vdash
a\mathord{\,:\,}\alpha(xf)$, and $e\Vdash
b_{(f,a)}(g)=b_{(fg,ag)}\colon\beta(xfg,ag)$ for all $g\colon e\to d$. ∎

### Kripke-Joyal forcing for propositions

We conclude this section by specialising our Kripke-Joyal forcing for type
theory to propositions in $\tE$ and relating it to the standard Kripke-Joyal
forcing for first-order logic. For this, we make use of the relation between
the small map classifier $U$ and the subobject classifier $\Omega$ described
in Section 2. Recall that the standard Kripke-Joyal semantics is given by the
specification, for $\sigma\colon X\to\Omega$ and $x\colon\mathsf{y}{c}\to X$,
that $c\Vdash\sigma(x)$ if there is a (necessarily unique) dotted map fitting
in the diagram

${\\{x\mathord{\,:\,}X\mid\sigma(x)\\}}$${1}$${\mathsf{y}{c}}$${X}$${\Omega\,.}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{x}$$\scriptstyle{\sigma}$
(4.3)

The following shows that our Kripke-Joyal semantics for type theory coincides
with the standard one when restricted to propositions.

######  Theorem 4.19.

Let $\sigma\colon X\to\Omega$ and $x\colon\mathsf{y}{c}\to X$. Then the
following conditions are equivalent.

  1. (i)

$c\Vdash\sigma(x)$.

  2. (ii)

There exists a (necessarily unique) $s\colon\mathsf{y}{c}\to E$ such that
$c\Vdash s\colon\\{\sigma(x)\\}$.

  * Proof.

Immediate from the definitions, observing that we have the two-pullback
diagram

$\begin{gathered}\leavevmode\hbox to200.61pt{\vbox
to63.42pt{\pgfpicture\makeatletter\hbox{\hskip
100.3061pt\lower-37.71385pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-100.3061pt}{-25.70831pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 23.99997pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 41.80841pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.5029pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${X.\\{\sigma\\}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
17.80844pt\hfil&\hfil\hskip 30.80551pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.5pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${1}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.80554pt\hfil&\hfil\hskip 32.28467pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.97916pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${E}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.2847pt\hfil\cr\vskip 18.00005pt\cr\hfil\hskip
9.10822pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.80267pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\mathsf{y}{c}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
9.10822pt\hfil&\hfil\hskip 32.84023pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.53471pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${X}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.84026pt\hfil&\hfil\hskip 31.91663pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.61111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\Omega}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
7.91666pt\hfil&\hfil\hskip 32.26453pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.95901pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${U\mathrlap{.}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.26456pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{19.40765pt}{11.44447pt}\pgfsys@lineto{44.06668pt}{11.44447pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{44.26666pt}{11.44447pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{1.39922pt}{0.50488pt}\pgfsys@lineto{1.39922pt}{-14.61533pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{1.39922pt}{0.3049pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{1.39922pt}{-14.8153pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{51.47218pt}{3.00488pt}\pgfsys@lineto{51.47218pt}{-14.61533pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{51.47218pt}{2.8049pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{51.47218pt}{-14.8153pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{53.82495pt}{-7.11803pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\mathsf{true}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{58.47772pt}{11.44447pt}\pgfsys@lineto{83.13675pt}{11.44447pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{83.33673pt}{11.44447pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{ {}{}{}}{} {}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{83.53671pt}{10.38959pt}\pgfsys@lineto{0.3969pt}{0.04935pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.99236}{-0.12341}{0.12341}{-0.99236}{0.19846pt}{0.02467pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{44.12112pt}{-0.17186pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{\pi}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-81.88968pt}{-23.20831pt}\pgfsys@lineto{-58.68967pt}{-23.20831pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-58.48969pt}{-23.20831pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-72.09003pt}{-28.57497pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{
{}{}{}}{{{{}}{{}}{{}}{{}}}{{{{}}{ {}{}}{}{}{{}{}}}} }{{}{}}{{}}
{}{}{}{{{}}{{}}{{}}} {{{}}{{}}{{}}}
{}{{}}{}{{}}{}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{0.39998pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-82.88951pt}{-17.54306pt}\pgfsys@curveto{-54.80605pt}{-0.02838pt}{-32.77136pt}{4.63492pt}{-0.39601pt}{0.056pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.99014}{-0.14005}{0.14005}{0.99014}{-0.19801pt}{0.02802pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-40.2092pt}{-23.20831pt}\pgfsys@lineto{-7.1174pt}{-23.20831pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.91742pt}{-23.20831pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.46326pt}{-28.57497pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{\sigma}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{9.51587pt}{-23.20831pt}\pgfsys@lineto{42.60767pt}{-23.20831pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{42.80765pt}{-23.20831pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.09508pt}{-33.06108pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\\{-\\}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\end{gathered}\vspace{-2em}$

∎

######  Notation 4.20.

In light of 4.19, we shall often write $c\Vdash\sigma(x)$ to mean that there
exists an $s$ such that $c\Vdash s\colon\\{\sigma(x)\\}$.

By 4.19, we obtain forcing conditions for all types $\sigma\colon\Gamma\to U$
that factor through the monomorphism $\\{-\\}\colon\Omega\to U$ of (2.1). For
such types, the uniformity conditions required for function types and
$\Pi$-types become vacuous and indeed give back the standard Kripke-Joyal
conditions. We illustrate this in a few cases.

######  Proposition 4.21 (Forcing for propositional equality).

Let $\alpha\colon X\to U$ and suppose that $X\vdash a\colon\alpha$ and
$X\vdash b\colon\alpha$. Then for any $x\colon\mathsf{y}{c}\to X$, the
following conditions are equivalent.

  1. (i)

$c\Vdash a(x)=b(x)$.

  2. (ii)

$a(x)$ and $b(x)$ are equal as maps $\mathsf{y}{c}\to E$.

  * Proof.

For each $x\colon\mathsf{y}{c}\to X$, the element $a\colon\alpha$ determines a
map $(x,a(x))$ as follows (and similarly for $b\colon\alpha$).

${X.\alpha}$${E}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{x}$$\scriptstyle{(x,a(x))}$$\scriptstyle{a}$$\scriptstyle{\alpha}$

Now consider the following diagram, in which both squares are pullbacks.

${X.\alpha}$${1}$${E}$${\mathsf{y}{c}}$${X.\alpha\times\alpha}$${\Omega}$${U\mathrlap{.}}$$\scriptstyle{\delta_{\alpha}}$$\scriptstyle{(x,a(x),b(x))}$$\scriptstyle{=_{\alpha}}$

By definition, we have $c\Vdash a(x)=b(x)$ if and only if there is a dotted
map as indicated. But this holds if and only if $(x,a(x))=(x,b(x))$, which in
turn is equivalent to $a(x)=b(x)$ as maps $\mathsf{y}{c}\to E$. ∎

For disjunction, even though $\\{\sigma\lor\tau\\}$ is not the same as
$\\{\sigma\\}+\\{\tau\\}$, we still have the following equivalence due to
special properties of presheaf categories.

######  Proposition 4.22 (Forcing for disjunction).

Let $\sigma,\tau\mathord{\,:\,}X\to\Omega$. For $x\colon\mathsf{y}{c}\to X$,
the following conditions are equivalent.

  1. (i)

$c\Vdash\sigma(x)\lor\tau(x)$.

  2. (ii)

$c\Vdash\sigma(x)$ or $c\Vdash\tau(x)$.

  * Proof.

As stated in 2.5, the disjunction $\sigma\lor\tau\colon X\to\Omega$ classifies
the subobject $\\{\sigma\\}\cup\\{\tau\\}\rightarrowtail X$, which is the
image of the canonical map $\\{\sigma\\}+\\{\tau\\}\to X$. So if
$c\Vdash\sigma(x)\lor\tau(x)$, then there is a map
$v\colon\mathsf{y}{c}\to\\{\sigma\\}\cup\\{\tau\\}$ lifting $x$. Since the
representable $\mathsf{y}{c}$ is projective, there is then a further lift
$u\colon\mathsf{y}{c}\to\\{\sigma\\}+\\{\tau\\}$, and so $c\Vdash
u\colon\\{\sigma(x)\\}+\\{\tau(x)\\}$. Applying 4.13 we obtain either $c\Vdash
a\colon\\{\sigma(x)\\}$ or $c\Vdash b\colon\\{\tau(x)\\}$, whence either
$c\Vdash\sigma(x)$ or $c\Vdash\tau(x)$. The converse is even more direct,
using the factorisations

${\\{\sigma\\}}$${\\{\sigma\\}\cup\\{\tau\\}}$${\\{\tau\\}}$${X\mathrlap{.}}$

∎

A similar fact also holds for existential quantifiers.

######  Proposition 4.23.

Let $\alpha\colon X\to U$ and $\sigma\colon X.\alpha\to\Omega$. For
$x\colon\mathsf{y}{c}\to X$, the following conditions are equivalent.

  1. (i)

$c\Vdash(\exists_{\alpha}\sigma)(x)$.

  2. (ii)

There exists $a\colon\mathsf{y}{c}\to E$ such that $c\Vdash
a\mathord{\,:\,}\alpha(x)$, and $c\Vdash\sigma(x,a)$.

  * Proof.

First assume that $c\Vdash(\exists_{\alpha}\sigma)(x)$, which means that we
have a lift

${\\{x\mathord{\,:\,}X\mid\exists_{\alpha}\sigma(x)\\}}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{x}$

Since $\mathsf{y}{c}$ is projective, there is then a further lift as indicated
in the diagram below, which also recalls the construction of
$\\{X\mid\exists_{\alpha}\sigma\\}$.

${X.\alpha.\\{\sigma\\}}$${X.\alpha}$${E}$${\mathsf{y}{c}}$${\\{X\mid\exists_{\alpha}\sigma\\}}$${X}$${U}$$\scriptstyle{p_{\sigma}}$$\scriptstyle{q_{\alpha}}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{\pi}$$\scriptstyle{v}$$\scriptstyle{u}$$\scriptstyle{\alpha}$

Let $a=_{\mathrm{def}}q_{\alpha}\circ p_{\sigma}\circ v$, so that $c\Vdash
a\mathord{\,:\,}\alpha(x)$, and $c\Vdash\sigma(x,a)$, by construction. The
converse is direct, using the above diagram. ∎

The general charaterisation of forcing for subset types follows the same
pattern. The proof is left to the reader.

######  Proposition 4.24 (Forcing for subset types).

Let $\alpha\colon X\to U$ and $\sigma\colon X.\alpha\to\Omega$. For
$x\colon\mathsf{y}{c}\to X$, the following conditions are equivalent.

  1. (i)

There exists $s$ such that $c\Vdash
s\mathord{\,:\,}\\{y\mathord{\,:\,}\alpha(x)\mid\sigma(x,y)\\}$

  2. (ii)

There exists $a$ such that $c\Vdash a\mathord{\,:\,}\alpha(x)$ and
$c\Vdash\sigma(x,a)$. ∎

######  Proposition 4.25 (Forcing for propositional truncation).

Let $\alpha\colon X\to U$. For $x\colon\mathsf{y}{c}\to X$, the following
conditions are equivalent.

  1. (i)

$c\Vdash\mathsf{supp}(\alpha)(x)$.

  2. (ii)

There exists $a$ such that $c\Vdash a\colon\alpha(x)$.

  * Proof.

Recall from 2.4 that the propositional truncation $\mathsf{supp}(\alpha)\colon
X\to\Omega$ is the pullback along $\alpha$ of the image factorisation of
$\pi\colon E\to U$,

${X.\alpha}$${E}$${X.\\{\mathsf{supp}(\alpha)\\}}$${\operatorname{im}(\pi)}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{q_{\alpha}}$$\scriptstyle{x}$$\scriptstyle{u}$$\scriptstyle{\alpha}$

By definition, $c\Vdash\mathsf{supp}(\alpha)(x)$ if and only if there is a
factorisation of $x\colon\mathsf{y}{c}\to X$ through the subobject
$X.\\{\mathsf{supp}(\alpha)\\}\rightarrowtail X$. But since the representable
$\mathsf{y}{c}$ is projective, this is the case if and only if there is a
further lift $u\colon\mathsf{y}{c}\to X.\alpha$ as indicated. Composing to get
$a=q_{\alpha}\circ u$ gives $c\Vdash a\colon\alpha(x)$. The converse is
immediate. ∎

######  Remark 4.26.

Our Kripke-Joyal forcing semantics can be specialised to the system of
dependent type theory without a type $\Omega$ of propositions, but with the
type formers

$0\mathrlap{,}\quad
1\mathrlap{,}\quad\alpha+\beta\mathrlap{,}\quad\alpha\times\beta\mathrlap{,}\quad\alpha\to\beta\mathrlap{,}\quad\Sigma_{x\colon\alpha}\beta(x)\mathrlap{,}\quad\Pi_{x\colon\alpha}\beta(x)\mathrlap{,}\quad
a=_{\alpha}b\mathrlap{,}$ (4.4)

by treating propositional equality $a=_{\alpha}b$ equivalently as an
(extensional) equality type $\mathsf{Eq}_{\alpha}(a,b)$, as mentioned in 3.16.
This can then be seen as a proof-relevant version of the standard Kripke
semantics for intuitionistic first-order logic [48]. The standard deduction
relation $\vdash_{\mathsf{IFOL}}$ for that system can be shown to be _sound
and complete_ with respect to standard Kripke semantics, in the sense that for
any closed formula $\sigma$, one has $\vdash_{\mathsf{IFOL}}\sigma$ if and
only if $K\Vdash\sigma$ for all Kripke frames $K$, which are essentially
interpretations of the signature of $\sigma$ into categories of the form
$\mathsf{Set}^{K}$ for arbitrary posets $K$.

Similarly, one can infer from the results in [5] that the system of type
theory specified by (4.4), with the customary inference rules, as stated e.g.
in _ibid._ , is deductively complete with respect to our Kripke-Joyal forcing
semantics, in the following sense. Given a closed type $\alpha$ (over a basic
signature of closed and dependent types and terms), one can construct a closed
term $\vdash a\colon\alpha$ if and only if, for every interpretation of the
signature of $\alpha$ into a category of the form $\mathsf{Set}^{P}$ for an
arbitrary _poset_ $P$, one has $\mathsf{Set}^{P}\Vdash a\colon\alpha$ in the
sense of 4.7. Briefly, extensional dependent type theory is complete with
respect to Kripke-Joyal forcing semantics, something that is not true for the
system of higher-order logic, with a type of propositions. We leave to the
reader the pleasant task of simplifying the forcing conditions given in this
section for the special case where the index category $\cC$ is a poset.

##  5\. Cofibrations

### Basic definitions

This section starts the second part of the paper, in which we use our forcing
semantics to describe models of homotopy type theory. In order to do so, we
assume certain auxiliary structures on our fixed presheaf category, as in
[15], which give rise to (algebraic) weak factorisation systems [6, 8, 18]. As
we shall see, forcing allows us to relate precisely category-theoretic
concepts, as defined in [15, 21, 22], with their type-theoretic counterparts,
as defined in [35]. Below, we shall take the categorical point of view as our
starting point.

######  Definition 5.1.

A class of cofibrations in $\tE=\mathrm{Psh}(\cC)$ is a class of maps
$\mathsf{Cof}$ that satisfies the following conditions:

  1. (C1)

The elements of $\mathsf{Cof}$ are monomorphisms.

  2. (C2)

For every $X\in\tE$, the unique map $0\to 1$ is in $\mathsf{Cof}$.

  3. (C3)

For every $X\in\tE$, the identity $\operatorname{id}_{1}\colon 1\to 1$ is in
$\mathsf{Cof}$.

  4. (C4)

Cofibrations are stable under pullback along all maps.

  5. (C5)

Cofibrations are closed under composition.

  6. (C6)

The full subcategory of $\tE^{\to}_{\mathrm{cart}}$ spanned by $\mathsf{Cof}$
has a terminal object.

Let us now assume that $\mathsf{Cof}$ is a class of cofibrations in $\tE$. We
say that an object $X\in\tE$ is cofibrant if the unique map $!_{X}\colon 0\to
X$ is a cofibration.

######  Remark 5.2.

We note without proof a few elementary consequences of these axioms.

  1. (i)

In light of (C4), axioms (C2) and (C3) imply that, for every $X\in\tE$, the
unique map $!_{X}\colon 0\to X$ and the identity $\operatorname{id}_{X}\colon
X\to X$ are cofibrations . Thus, every object is cofibrant. See [19, 25] for a
context where this is not the case.

  2. (ii)

The terminal cofibration posited in (C6) will be denoted $\mathsf{t}\colon
1\rightarrowtail\Phi$, note that its domain can be shown to be $1$. In the
pullback square

${1}$${1}$${\Phi}$${\Omega\mathrlap{,}}$$\scriptstyle{\mathsf{t}}$$\scriptstyle{\mathsf{true}}$
(5.1)

the lower horizontal classifying map can be shown to be monic. The map
$\mathsf{t}\colon 1\rightarrowtail\Phi$ classifies cofibrations, in the sense
that a monomorphism $S\rightarrowtail X$ is in $\mathsf{Cof}$ if and only if
its classifying map $\sigma\colon X\to\Omega$ factors through
$\Phi\rightarrowtail\Omega$, and thus if and only if it is a pullback of
$\mathsf{t}$ along a (necessarily unique) classifying map.

  3. (iii)

The full subcategory of $\tE^{\to}_{\mathrm{cart}}$ spanned by $\mathsf{Cof}$
has all colimits, and these are preserved by the inclusion into
$\tE^{\to}_{\mathrm{cart}}$. In particular, cofibrations are closed under
coproducts $A+B\rightarrowtail X+Y$, descent along epimorphisms, and joins of
cofibrant subobjects $S\vee T\rightarrowtail X$.

  4. (iv)

The cofibrations with representable codomain $S\rightarrowtail\mathsf{y}c$ are
called generating cofibrations. Note that these form a small set. Every
cofibration is a colimit in $\tE^{\to}_{\mathrm{cart}}$ of generating
cofibrations in a canonical way (determined by the category of elements of its
codomain). As shown in [22, Theorem 9.1] using Garner’s small object argument
[23], the subcategory of generating cofibrations determines an algebraic weak
factorisation system $(\mathsf{Cof},\mathsf{TrivFib})$, with right class the
uniform trivial fibrations to be considered in Section 7.

Since $\Phi$ is a subobject of $\Omega$, it admits a classifier
$\operatorname{\mathsf{cof}}\colon\Omega\to\Omega$,

${\Phi}$${1}$${\Omega}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\operatorname{\mathsf{cof}}}$

In the internal type theory, we thus have

$\Phi=\\{\varphi\colon\Omega\mid\operatorname{\mathsf{cof}}{\varphi}\\}\mathrlap{.}$
(5.2)

We will call a proposition $\varphi\colon X\to\Omega$ cofibrant if it factors
through $\Phi\rightarrowtail\Omega$, for which we also write $\varphi\colon
X\to\Phi$.

Let $\varphi\colon X\to\Phi$ be a cofibrant proposition. The comprehension of
$\varphi$ with respect to $\Phi$ is defined as the pullback of $\mathsf{t}$
along $\varphi$. Thus the cofibrant comprehension agrees with the usual
(subobject) comprehension,

${\\{X\,|\,\varphi\\}}$${1}$${1}$${X}$${\Phi}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{t}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\varphi}$

Thus in particular, every generating cofibration is of the form
$\\{\mathsf{y}c\,|\,\varphi\\}\rightarrowtail\mathsf{y}c$ for a unique
$\varphi\colon\mathsf{y}c\to\Phi$.

The next series of propositions shows some of the consequences of our axioms
for cofibrations in the internal type theory of $\tE$, thus relating them to
those in [35, Figure 1]. In particular, 5.8 below is [35, Lemma 5.4 (i)], but
we give a forcing proof.

######  Lemma 5.3.

Let $\varphi\colon X\to\Omega$ be a proposition. For every
$x\colon\mathsf{y}c\to X$, the following conditions are equivalent.

  1. (i)

$c\Vdash\operatorname{\mathsf{cof}}\varphi(x)$.

  2. (ii)

$\varphi(x)\colon\mathsf{y}c\to\Omega$ factors through
$\Phi\rightarrowtail\Omega$.

  * Proof.

Consider the diagram

${\\{X\,|\,\operatorname{\mathsf{cof}}\varphi\\}}$${\Phi}$${1}$${\mathsf{y}c}$${X}$${\Omega}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{x}$$\scriptstyle{\varphi}$$\scriptstyle{\operatorname{\mathsf{cof}}}$

∎

######  Lemma 5.4.

Let $\varphi\colon X\to\Omega$. Then
$\tE\Vdash\varphi\Rightarrow\operatorname{\mathsf{cof}}\varphi$.

  * Proof.

We show that
$c\Vdash\varphi(x)\Rightarrow\operatorname{\mathsf{cof}}\varphi(x)$ for every
$x\colon\mathsf{y}c\to X$. So let $f\colon d\to c$ and assume
$d\Vdash\varphi(xf)$. Then there is a dotted map in

${\\{\varphi\\}}$${1}$${\mathsf{y}d}$${\mathsf{y}c}$${X}$${\Omega\mathrlap{.}}$${\lrcorner}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{f}$$\scriptstyle{x}$$\scriptstyle{\varphi}$

We then obtain the diagram

${\\{\varphi\\}}$${1}$${{\\{\operatorname{\mathsf{cof}}\varphi\\}}}$${\Phi}$${1}$${\mathsf{y}d}$${\mathsf{y}c}$${X}$${\Omega}$${\Omega\mathrlap{,}}$${\lrcorner}$$\scriptstyle{\mathsf{t}}$${\lrcorner}$${\lrcorner}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{f}$$\scriptstyle{x}$$\scriptstyle{\varphi}$$\scriptstyle{\operatorname{\mathsf{cof}}}$

which shows $d\Vdash\operatorname{\mathsf{cof}}\varphi(xf)$, as required. ∎

######  Corollary 5.5.

Let $\varphi\colon X\to\Omega$.

  1. (i)

The map $\\{\varphi\\}\rightarrowtail\\{\operatorname{\mathsf{cof}}\varphi\\}$
is a cofibration.

  2. (ii)

$\operatorname{\mathsf{cof}}\varphi=_{\Omega}\mathsf{true}$ if and only if
$\\{\varphi\\}\rightarrowtail X$ is a cofibration if and only if
$\\{\operatorname{\mathsf{cof}}\varphi\\}\rightarrowtail X$ is an isomorphism.
∎

######  Proposition 5.6 (Forcing characterisation of cofibrations).

Let $m\colon S\rightarrowtail X$ be a monomorphism. Then the following
conditions are equivalent.

  1. (i)

The map $m$ is a cofibration.

  2. (ii)

$\tE\Vdash(\forall x\colon X)\operatorname{\mathsf{cof}}\\!\big{(}(\exists
s\colon S)(m(s)=x)\big{)}$.

  * Proof.

We first show that, for $\varphi\colon X\to\Omega$, $\tE\Vdash(\forall x\colon
X)\operatorname{\mathsf{cof}}\varphi(x)$ if and only if $\varphi$ is
cofibrant. Indeed, $\tE\Vdash(\forall x\colon
X)\operatorname{\mathsf{cof}}\varphi(x)$ if and only if
$d\Vdash\operatorname{\mathsf{cof}}\varphi(xf)$ for all $x\colon\mathsf{y}c\to
X$ and $f\colon d\to c$. This holds if and only if there is a dotted map in

${{\\{\operatorname{\mathsf{cof}}\varphi\\}}}$${\mathsf{y}d}$${\mathsf{y}c}$${X\mathrlap{.}}$$\scriptstyle{f}$$\scriptstyle{x}$

By the Yoneda lemma, this means there is a factorisation of $\varphi\colon
X\to\Omega$ through $\Phi$,

${{\\{\operatorname{\mathsf{cof}}\varphi\\}}}$${\Phi}$${1}$${\mathsf{y}d}$${\mathsf{y}c}$${X}$${\Omega}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{f}$$\scriptstyle{x}$$\scriptstyle{\varphi}$$\scriptstyle{\operatorname{\mathsf{cof}}}$

To prove the required claim, it suffices to define $\varphi\colon X\to\Omega$
to be the classifying map of $m\colon S\rightarrowtail X$, i.e.
$\varphi(x)=_{\mathrm{def}}(\exists s\colon S)(m(s)=x)$. ∎

### Dominance

We show that Axiom (C5) corresponds to the basic law of a dominance,
introduced in [40].

######  Lemma 5.7.

Suppose $\varphi\colon X\to\Omega$ and $\psi\colon X\to\Omega$, and consider
the pullback squares

${\\{\varphi\wedge\psi\\}}$${\\{\psi\\}}$${1}$${\\{\varphi\\}}$${X}$${\Omega\mathrlap{.}}$$\scriptstyle{\mathsf{true}}$$\scriptstyle{\psi}$

The following conditions are equivalent.

  1. (i)

$\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ is a cofibration.

  2. (ii)

$\tE\Vdash\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi$.

  * Proof.

Assume first that $\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ is a
cofibration. Let $c\in\cC$ and $x\colon\mathsf{y}c\to X$. We want to show
$c\Vdash\varphi(x)\Rightarrow\operatorname{\mathsf{cof}}\psi(x)$, so let
$f\colon d\to c$ and assume that $d\Vdash\varphi(xf)$, i.e. that we have a
factorisation

${\\{\varphi\\}}$${\mathsf{y}d}$${\mathsf{y}c}$${X\mathrlap{,}}$$\scriptstyle{f}$$\scriptstyle{x}$

and we claim that $d\Vdash\operatorname{\mathsf{cof}}\psi(xf)$. That holds if
and only if $\psi(xf)\colon\mathsf{y}d\to\Omega$ factors through $\Phi$ or,
equivalently, just if $\\{\psi(xf)\\}\rightarrowtail\mathsf{y}d$ is a
cofibration. But $\\{\psi(xf)\\}\rightarrowtail\mathsf{y}d$ is also the
pullback of $\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ along the
dotted arrow above. The claim follows by the closure of cofibrations under
pullback, Axiom (C4).

Conversely, as we just saw,
$\tE\Vdash\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi$ if and only if
the pullback of $\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ along any
map $\mathsf{y}c\to\\{\varphi\\}$ is a cofibration. But this implies that
$\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ itself is a cofibration.
∎

######  Proposition 5.8.

Assuming only axioms (C1–4) and (C6), axiom (C5) can be expressed equivalently
as follows.

  1. (i)

Cofibrations are closed under composition.

  2. (ii)

$\tE\Vdash(\forall\varphi,\psi\colon\Omega)\operatorname{\mathsf{cof}}\varphi\Rightarrow\big{(}(\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi)\Rightarrow\operatorname{\mathsf{cof}}(\varphi\land\psi)\big{)}$.

  * Proof.

Suppose that item (i) holds. We need to show that for every $c\in\cC$, we have
$c\Vdash(\forall\varphi,\psi\colon\Omega)\operatorname{\mathsf{cof}}\varphi\Rightarrow\big{(}(\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi)\Rightarrow\operatorname{\mathsf{cof}}(\varphi\land\psi)\big{)}$
. Thus take any $x:d\to c$ and $\varphi,\psi:\mathsf{y}{d}\to\Omega$ and any
$y\colon e\to d$ such that $e\Vdash\operatorname{\mathsf{cof}}\varphi(xy)$,
and let furthermore $z\colon f\to e$ with
$f\Vdash\varphi(xyz)\Rightarrow\operatorname{\mathsf{cof}}(\psi(xyz))$. Then
$\\{\varphi(xy)\\}\rightarrowtail\mathsf{y}e$ is a cofibration and therefore
so is $\\{\varphi(xyz)\\}\rightarrowtail\mathsf{y}f$ and, by Lemma 5.7,
$\\{\varphi(xyz)\land\psi(xyz)\\}\rightarrowtail\\{\varphi(xyz)\\}$ is a
cofibration as well. By the assumption, the composite
$\\{\varphi(xyz)\land\psi(xyz)\\}\rightarrowtail\mathsf{y}f$ is then a
cofibration, and hence
$f\Vdash\operatorname{\mathsf{cof}}(\varphi(xyz)\land\psi(xyz))$, as required.

To see that (ii) implies (i), note first that arbitrary cofibrations compose
just if the same is true of cofibrations of the form
$\\{\varphi\\}\rightarrowtail\mathsf{y}c$ and
$\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$, where
$\varphi,\psi\colon\mathsf{y}c\to\Omega$. (Indeed, given arbitrary
cofibrations $\\{\varphi\\}\rightarrow X$ and
$\\{\vartheta\\}\rightarrowtail\\{\varphi\\}$, the composite is a cofibration
just if its pullback along every $\mathsf{y}c\to X$ is one; then take
$\\{\psi\\}\rightarrowtail\mathsf{y}c$ to be the composite
$\\{\vartheta\\}\rightarrowtail\\{\varphi\\}\rightarrowtail\mathsf{y}c$.) So
let $\\{\varphi\\}\rightarrowtail\mathsf{y}c$ and
$\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ be cofibrations, and
assume item (ii), so that for all $d\to c$ and all $\varphi,\psi:d\to\Omega$,
we have

$d\Vdash\operatorname{\mathsf{cof}}\varphi\Rightarrow((\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi)\Rightarrow\operatorname{\mathsf{cof}}(\varphi\land\psi))\mathrlap{.}$