Thus, in particular, if $c\Vdash\operatorname{\mathsf{cof}}\varphi$ and
$c\Vdash\varphi\Rightarrow\operatorname{\mathsf{cof}}\psi$ then
$c\Vdash\operatorname{\mathsf{cof}}(\varphi\land\psi)$. But the first premise
holds since $\\{\varphi\\}\rightarrowtail\mathsf{y}c$ is assumed to be a
cofibration, and the second premise holds by Lemma 5.7, since
$\\{\varphi\land\psi\\}\rightarrowtail\\{\varphi\\}$ is also assumed to be a
cofibration. Thus we have
$c\Vdash\operatorname{\mathsf{cof}}(\varphi\land\psi)$, and so
$\\{\varphi\land\psi\\}\rightarrowtail\mathsf{y}c$ is a cofibration, as
required.

∎

######  Remark 5.9.

Let $\varphi\colon X\to\Phi$ and $\psi\colon\\{\varphi\\}\to\Phi$, and
consider the pullback squares

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

We write $\Sigma_{\varphi}\psi\colon X\to\Phi$ for the classifer of the
composite cofibration
$\\{\varphi\,|\,\psi\\}\rightarrowtail\\{\varphi\\}\rightarrowtail X$. Thus,
$\\{\varphi\,|\,\psi\\}=\\{\Sigma_{\varphi}\psi\\}$ as subobjects of $X$.

##  6\. Partial elements

Uniform trivial fibrations will be defined in Section 7 as maps equipped with
a lifting structure against cofibrations. In the type theory of $\tE$, this is
expressed in terms of the notion of a cofibrant partial element of a type [35,
Section 5.1]. In preparation for the material on uniform fibrations, we
discuss cofibrant partial elements, leading up to 6.5, which provides the
equivalence between the categorical and type-theoretical definitions. As
before, we start with a diagrammatic definition. We consider a fixed class of
cofibrations as in 5.1.

######  Definition 6.1.

Let $p\colon A\to X$ be a map in $\tE$.

  1. (i)

A (cofibrant) partial element of $p\colon A\to X$ is a pair $(m,u)$, where
$m\colon S\rightarrowtail X$ is a cofibration and $u\colon S\to A$ makes the
following diagram commute:

${S}$${A}$${X}$${X\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{m}$$\scriptstyle{p}$
(6.1)

We call $S$ the extent of the partial element $(m,u)$.

  2. (ii)

A partial element $(m,u)$ of $A\to X$ is extensible if there exists $a\colon
X\to A$ such that the following diagram commutes:

${S}$${A}$${X}$${X\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{m}$$\scriptstyle{a}$

Regarding $A$ as an object in $\tE/_{\\!X}$, we wish to define the object
$P_{X}(A)\in\tE/_{\\!X}$ of all such partial elements of $A$, or as we shall
say, the _classifying type_ for partial elements. Consider the case $X=1$. A
partial element can then be described equivalently as a pair $(\varphi,u)$
where $\varphi\colon 1\to\Phi$, and $u\colon\\{\varphi\\}\to A$. We can
therefore define the object $P(A)$ as follows. Let $P\colon\tE\to\tE$ be the
polynomial endofunctor associated to the map $\mathsf{t}\colon 1\to\Phi$,
namely the composite

${\tE}$${\tE/_{\Phi}}$${\tE\mathrlap{.}}$$\scriptstyle{\Pi_{\mathsf{t}}}$$\scriptstyle{\Sigma_{\Phi}}$
(6.2)

The global elements $t\colon 1\to P(A)$ are pairs $t=(\varphi,v)$ with
$\varphi\mathord{\,:\,}1\to\Phi$ and $v\colon 1\to A^{\\{\varphi\\}}$. This
data determines a unique span

${\\{\varphi\\}}$${A}$${1}$${1\mathrlap{,}}$$\scriptstyle{u}$ (6.3)

with $\lambda u=v$, which is exactly a partial element of $A$ in the sense of
6.1. For example, since
$\operatorname{\mathsf{cof}}(\mathsf{t})=\mathsf{true}$ by axiom (C3), for any
$a\colon 1\to A$ there is the totally defined partial element
$(\mathsf{t},a)\colon 1\to P(A)$. Similarly, since
$\operatorname{\mathsf{cof}}(\mathsf{f})=\mathsf{true}$ by axiom (C2), we have
the totally undefined partial element $(\mathsf{f},0_{A})\colon 1\to P(A)$.

Finally, if $p\colon A\to X$, then let $P_{X}(A)\to X$ be the result of
applying the corresponding endofunctor $P_{X}\colon\tE/_{\\!X}\to\tE/_{\\!X}$,
where in place of $\mathsf{t}\colon 1\to\Phi$ we use the cofibration
classifier for $\tE/_{\\!X}$, namely $X^{*}\mathsf{t}\colon X^{*}1\to
X^{*}\Phi$, as in [22, Section 9]. We then recover the description in [35,
Definition 5.1] using the internal type theory of $\tE$, as follows. If
$p\colon A\to X$ is classified by $\alpha\colon X\to U$, then $P_{X}(A)\to X$
is classified by the type

$\textstyle P(\alpha)=_{\mathrm{def}}\
\sum_{\varphi\mathord{\,:\,}\Phi}\,\alpha^{\\{\varphi\\}}\mathrlap{,}$ (6.4)

in the sense that $P_{X}(A)\cong X.P(\alpha)$ over $X$. Hereafter, we will use
the type-theoretic description (6.4) interchangeably with the relative point
of view, keeping in mind that the function type $\alpha^{\\{\varphi\\}}$
refers to the relative exponential over $X$. Sections $t\colon X\to
X.P(\alpha)$ over $X$ then correspond in exactly the same way to diagrams

${\\{\varphi\\}}$${X.\alpha}$${X}$${X\mathrlap{,}}$$\scriptstyle{u}$$\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$}}}}$
(6.5)

i.e. partial elements of
${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$, with $t=(\varphi,\lambda u)$ for $\varphi\colon X\to\Phi$ and
$u\colon\\{\varphi\\}\to X.\alpha$ over $X$.

The functor $P\colon\tE\to\tE$ defined in (6.2), as well as its relative
versions $P_{X}\colon\tE/_{\\!X}\to\tE/_{\\!X}$, has a canonical pointing
$\eta\colon\operatorname{id}_{\tE}\to P$, given by the composite

${1}$${\Sigma_{{\Phi}}\circ\Sigma_{\mathsf{t}}}$${\Sigma_{{\Phi}}\circ\Pi_{\mathsf{t}}\circ{\mathsf{t}}^{*}\circ\Sigma_{\mathsf{t}}}$${\Sigma_{{\Phi}}\circ\Pi_{\mathsf{t}}}$${P\mathrlap{,}}$$\scriptstyle{\cong}$

where the second map uses the unit of the adjunction
${\mathsf{t}}^{*}\dashv\Pi_{\mathsf{t}}$, and the third map uses that the unit
of the adjunction $\Sigma_{\mathsf{t}}\dashv{\mathsf{t}}^{*}$ is an
isomorphism
$\operatorname{id}_{\tE}\cong{\mathsf{t}}^{*}\circ\Sigma_{\mathsf{t}}$ since
$\mathsf{t}$ is monic. Observe that $\eta_{A}\colon A\to P(A)$ can be defined
in the type theory of $\tE$ as the function taking $a\colon A$ to the totally
defined partial element $(\mathsf{t},a)\colon T(A)$. 6.4 below gives the sense
in which $P(A)$ classifies cofibrant partial elements of $A$. For this, we
require a lemma.

######  Lemma 6.2.

For every $A\in\tE$, the commutative diagram

${A}$${P(A)}$${1}$${\Phi}$$\scriptstyle{\eta_{A}}$$\scriptstyle{!_{A}}$$\scriptstyle{\operatorname{\pi_{1}}}$$\scriptstyle{\mathsf{t}}$

is a pullback. Thus $\eta_{A}\colon A\to P(A)$ is a cofibration.

  * Proof.

As already noted, since $\mathsf{t}$ is monic the unit of
$\Sigma_{\mathsf{t}}\dashv{\mathsf{t}}^{*}$ is an isomorphism
$\operatorname{id}_{\tE}\cong{\mathsf{t}}^{*}\circ\Sigma_{\mathsf{t}}$. It
follows by a standard argument that the counit of
${\mathsf{t}}^{*}\dashv\Pi_{\mathsf{t}}$ is also an isomorphism
${\mathsf{t}}^{*}\circ\Pi_{\mathsf{t}}\cong\operatorname{id}_{\tE}$. Since
$T(A)=\Pi_{\mathsf{t}}(A)$, we therefore have $\mathsf{t}^{*}(TA)\cong A$. ∎

######  Corollary 6.3.

The natural transformation $\eta\colon\operatorname{id}_{\tE}\to P$ is
cartesian.

  * Proof.

Let $f\colon A\to B$ be a morphism in $\tE$ and consider the naturality
diagram

${A}$${P(A)}$${B}$${P(B)}$${1}$${\Phi\mathrlap{.}}$$\scriptstyle{\eta_{A}}$$\scriptstyle{f}$$\scriptstyle{P{f}}$$\scriptstyle{\eta_{B}}$$\scriptstyle{\mathsf{t}}$

The bottom square and the outer rectangle are cartesian by the previous lemma,
so the top square is also cartesian. ∎

The next proposition gives the universal property of $\eta_{A}\colon A\to
P(A)$.

######  Proposition 6.4.

For every $A\in\tE$, the map $\eta_{A}\colon A\rightarrowtail P(A)$ classifies
cofibrant partial maps to $A$ in the following sense: for any $T\in\tE$ and
cofibration $m\colon S\rightarrowtail T$ and map $u\colon S\to A$ as indicated
below, the span $(m,u)$ can be uniquely completed to a pullback square as
follows.

${S}$${A}$${T}$${P(A)\mathrlap{.}}$$\scriptstyle{m}$$\scriptstyle{u}$$\scriptstyle{\eta_{A}}$
(6.6)

  * Proof.

The cofibration $m\colon S\rightarrowtail T$ has a unique classifying map
$\varphi\colon T\to\Phi$. Using 6.2, we can complete (6.6) to form the solid
part of the following diagram, in which the outer (distorted) rectangle is a
pullback.

${S}$${A}$${1}$${T}$${P(A)}$${\Phi\mathrlap{.}}$$\scriptstyle{m}$$\scriptstyle{u}$$\scriptstyle{\mathsf{t}}$$\scriptstyle{\varphi}$$\scriptstyle{\operatorname{\pi_{1}}}$
(6.7)

Recalling that $\operatorname{\pi_{1}}\colon P(A)\to\Phi$ is
$\Pi_{\mathsf{t}}(A)$, we have the indicated dotted map as $u^{\sharp}\colon
T\to P(A)$ over $\Phi$, the adjoint transpose of $u\colon
T\cong{\mathsf{t}}^{*}(T)\to A$ under the adjunction
$\mathsf{t}^{*}\dashv\Pi_{\mathsf{t}}$. The left hand square then commutes,
and is a pullback, because $\mathsf{t}^{*}(u^{\sharp})=u$. ∎

Letting $T=1$ in the foregoing shows that $P(A)$ classifies partial elements
of $A$ in $\tE$, and doing the same for $p\colon A\to X$ in the slice category
$\tE/_{\\!X}$ shows that $P_{X}(A)$ classifies partial elements in the sense
of 6.1. In light of 6.4, we call $\eta_{A}\mathord{\,:\,}A\to P(A)$ the
cofibrant partial map classifier of $A$ (cf. [3, Proposition 4]), generalising
the usual partial map classifier from topos theory [29, Proposition A.2.4.7],
which occurs when $\operatorname{\mathsf{cof}}=\mathsf{true}\circ{!_{\Omega}}$
and so $\Phi=\Omega$.

We now unfold explicitly the forcing conditions for $P(A)$, which are
determined by those for dependent sums and dependent products.

######  Proposition 6.5 (Forcing for partial elements).

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

  1. (i)

There is a cofibration $m\colon\\{\varphi\\}\rightarrowtail\mathsf{y}c$ and a
map $u\colon\\{\varphi\\}\to E$ such that the following diagram commutes:

${\\{\varphi\\}}$${X.\alpha}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{m}$$\scriptstyle{(xm,u)}$$\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{x}$

  2. (ii)

$c\Vdash\varphi\mathord{\,:\,}\Phi$ and there is a map
$u\colon\\{\varphi\\}\to E$ for which $c\Vdash\lambda
u\mathord{\,:\,}\\{\varphi\\}\to\alpha(x)$.

  3. (iii)

There is a map $t\colon\mathsf{y}c\to E$ such that $c\Vdash
t\mathord{\,:\,}P(\alpha)(x)$.

  * Proof.

For the equivalence between item (i) and item (ii), a map
$u\colon\\{\varphi\\}\to E$ determines a unique map
$(xm,u)\colon\\{\varphi\\}\to X.\alpha$ making the diagram in item (i) commute
if and only if the judgement $\mathsf{y}{c},\\{\varphi\\}\vdash
u\colon\alpha(xm)$ holds. But the latter is equivalent to $c\Vdash\lambda
u\colon\\{\varphi\\}\to\alpha(x)$.

For the equivalence between item (ii) and item (iii), recall the definition of
$P(\alpha)$ from from (6.4). So by 4.14, $c\Vdash
t\mathord{\,:\,}P(\alpha)(x)$ if and only if $t=(\varphi,v)$ with
$c\Vdash\varphi\mathord{\,:\,}\Phi$ and $c\Vdash
v\mathord{\,:\,}(\\{\varphi\\}\to\alpha)(x)$. We might as well assume without
loss of generality that $v=\lambda u$ for suitable $u\colon\\{\varphi\\}\to
E$, as required. ∎

######  Remark 6.6.

The forcing conditions in 6.5 may be unfolded even further using 4.17. Indeed,
if $t=(\varphi,v)$ then $c\Vdash\varphi\mathord{\,:\,}\Phi$ and $c\Vdash
v\mathord{\,:\,}(\\{\varphi\\}\to\alpha)(x)$ if and only if for all $f\colon
d\to c$ and $d\Vdash p\mathord{\,:\,}\\{\varphi(f)\\}$ we have
$d\Vdash\mathsf{app}(v(f),p)\mathord{\,:\,}\alpha(xf)$, and for all $g\colon
e\to d$, we have
$e\Vdash\mathsf{app}(v(f),p)(g)=\mathsf{app}(v({fg}),p(g))\colon\alpha(xfg)$.
In particular, for $v=\lambda{u}$, the computation rule for function types
reduces the above to

$d\Vdash p\mathord{\,:\,}\\{\varphi(f)\\}\,,\qquad d\Vdash
u(f)p\mathord{\,:\,}\alpha(xf)$

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

$e\Vdash(u(f)p)(g)=u({fg})p(g)\colon\alpha(xfg)$

for all $g\colon e\to d$.

The next result also admits both diagrammatic and internal type-theoretic
proofs (cf. [3, Proposition 5]). The proof via forcing given here serves
mainly to illustrate the method.

######  Theorem 6.7.

Let $\alpha\colon 1\to U$. Then there is a map $\mu_{\alpha}\colon
P^{2}(\alpha)\to P(\alpha)$, natural in $\alpha$, making the pointed
endofunctor $(P,\eta)$ into a monad on $\tE$. Moreover, the monad
$(P,\eta,\mu)$ extends to the slice categories $\tE/_{X}$ making it an
$\tE$-indexed monad.

  * Proof.

We will force an element $\mu_{\alpha}$ of the closed function type
$P^{2}(\alpha)\to P(\alpha)$. Thus we need to show:

    1. (i)

for all $c\in\cC$, there is given $\mu_{\alpha}c$ such that
$c\Vdash\mu_{\alpha}c\mathord{\,:\,}P^{2}(\alpha)\to P(\alpha)$,

    2. (ii)

for all $f\colon d\to c$,

$d\Vdash{\mu_{\alpha}c}\circ
f\,=\,\mu_{\alpha}d\mathord{\,:\,}P^{2}(\alpha)\to P(\alpha)\,.$ (6.8)

By 4.17, the forcing condition (1) for $\mu_{\alpha}c$ of function type
$P^{2}(\alpha)\to P(\alpha)$ at $c$ requires that for every $f\colon d\to c$
and for all $a$ such that $d\Vdash a\mathord{\,:\,}P^{2}(\alpha)(f)$, there is
given $\mu_{\alpha}c_{(f,a)}$ such that
$d\Vdash\mu_{\alpha}c_{(f,a)}\mathord{\,:\,}P(\alpha)(f)$, and moreover
$\mu_{\alpha}c_{(f,a)}\circ g=\mu_{\alpha}c_{(fg,ag)}$ for every $g\colon e\to
d$.

Since the types are closed, the indicated substitution of $f$ is trivial, and
so the requirements (1) and (2) simplify to the following (with some
relettering):

    * (1’)

for all $f\colon d\to c$, and for all $a$ such that $d\Vdash
a\mathord{\,:\,}P^{2}(\alpha)$, there is given $\mu_{\alpha}c_{(f,a)}$ such
that $d\Vdash\mu_{\alpha}c_{(f,a)}\mathord{\,:\,}P(\alpha)$, and

    * (2’)

for all $g\colon e\to d$, we have $\mu_{\alpha}c_{(f,a)}\circ
g=\mu_{\alpha}c_{(fg,ag)}$, and

    * (3)

for all $a$ such that $e\Vdash a\mathord{\,:\,}P^{2}(\alpha)$, we have

$e\Vdash\mu_{\alpha}c_{(fg,a)}\,=\,\mu_{\alpha}d_{(g,a)}\mathord{\,:\,}P(\alpha).$

Note that this also gives the uniformity in $c$ required in (2).

Thus let $f\colon d\to c$, and suppose that $d\Vdash
a\mathord{\,:\,}P^{2}\alpha$. By 6.5, for the type of partial elements
$P(P\alpha)=\sum_{\varphi\mathord{\,:\,}\Phi}\,(P\alpha)^{\\{\varphi\\}}$, we
have $a=(\varphi,\lambda u)$ with:

    1. (a)

$d\Vdash\varphi\mathord{\,:\,}\Phi$ and $d\Vdash\lambda
u\mathord{\,:\,}\\{\varphi\\}\to P\alpha$, the latter meaning that:

    2. (a1)

for all $g\colon e\to d$ and all $e\Vdash p\mathord{\,:\,}\\{\varphi g\\}$, we
have $e\Vdash u(g)p\mathord{\,:\,}P\alpha$, and

    3. (a2)

for all $h\colon e^{\prime}\to e$, we have $(u(g)p)h=u(gh)p(h)$.

Unfolding the clause $e\Vdash u(g)p\mathord{\,:\,}P\alpha$ in (a1) yields
$u(g)p=(\psi,\lambda v)$ with:

    1. (b)

$e\Vdash\psi\mathord{\,:\,}\Phi$ and $e\Vdash\lambda
v\mathord{\,:\,}\\{\psi\\}\to\alpha$, the latter meaning that:

    2. (b1)

for all $h\colon e^{\prime}\to e$ and all $e^{\prime}\Vdash
q\mathord{\,:\,}\\{\psi h\\}$, we have $e^{\prime}\Vdash
v(h)q\mathord{\,:\,}\alpha$, and

    3. (b2)

for all $i\colon e^{\prime\prime}\to e^{\prime}$, we have
$(v(h)q)i=v(hi)q(i)$.

To satisfy (1’), we need to construct an element
$\mu_{\alpha}c_{(f,a)}=(\vartheta,\lambda w)\mathord{\,:\,}P\alpha$ (based at
$\mathsf{y}{d}$) such that, among other things,

$d\Vdash\vartheta\mathord{\,:\,}\Phi\quad\text{and}\quad d\Vdash\lambda
w\mathord{\,:\,}\\{\vartheta\\}\to\alpha\,.$

From (a) above, we have a span,

${\\{\varphi\\}}$${P\alpha}$${\mathsf{y}{d}\mathrlap{.}}$$\scriptstyle{u}$
(6.9)

To see this, take any $p\colon\mathsf{y}{e}\to\\{\varphi\\}$ and compose with
$\\{\varphi\\}\rightarrowtail\mathsf{y}{d}$ to get a map $g\colon e\to d$ with
$e\Vdash p\mathord{\,:\,}\\{\varphi g\\}$. By (a1) we then get
$u(g)p\colon\mathsf{y}{e}\to P\alpha$. Since the assignment $p\mapsto u(g)p$
is natural in $e$ by (a2), by Yoneda there is indeed a map
$u\colon\\{\varphi\\}\to P\alpha$, as claimed.

Now let $u=(\psi,\lambda v)$, where $\psi\colon\\{\varphi\\}\to\Phi$, and
there is another span

${\\{\psi\\}}$${\alpha}$${\\{\varphi\\}\mathrlap{,}}$$\scriptstyle{v}$ (6.10)

as can be deduced from (b) in the same way that $(\varphi,\lambda u)$ followed
from (a).

Let $\vartheta\colon\mathsf{y}{d}\to\Phi$ classify the composite
$\\{\psi\\}\rightarrowtail\\{\varphi\\}\rightarrowtail\mathsf{y}{d}$, which is
a cofibration since each factor is one. We can then take $w=v$ to get the
desired pair $(\vartheta,\lambda w)$ with $d\Vdash(\vartheta,\lambda
w)\mathord{\,:\,}P(\alpha)$. Thus with
$\mu_{\alpha}c_{(f,a)}=(\vartheta,\lambda w)$ we have (1’). The uniformity
conditions (2’) and (3) then follow from the uniformity conditions in (a) and
(b).

Thus we have shown (6.8), and so there is a closed term $\mu_{\alpha}\colon
P^{2}\alpha\to P\alpha$. That $\mu_{\alpha}$ is natural in $\alpha$ can be
seen to follow from the universal property of $(P,\eta)$ given in 6.4. The
monad laws for $(P,\eta,\mu)$ can be seen to follow from the unit and
associativity laws for composition of (general maps and) cofibrations.
Finally, the entire monad $(P,\eta,\mu)$ is indexed over $\tE$, because all of
the type-theoretic constructions involved are stable under pullback, as is
forcing, by 4.11. ∎

##  7\. Uniform trivial fibrations

We again assume a fixed class $\mathsf{Cof}$ of cofibrations in $\tE$, as in
5.1. The subcategory of $\tE^{\rightarrow}$ consisting of cofibrations and
cartesian squares between them determines an algebraic weak factorisation
system $(\mathsf{Cof},\mathsf{TrivFib})$ on $\tE$ [22, Theorem 9.1]. The maps
in the right class $\mathsf{TrivFib}$ are the uniform trivial fibrations which
appear in the semantics of Homotopy Type Theory (see [15, Section 5.1], [3],
and [21]). In this section, we show how these structured maps can be described
equivalently in the internal type theory of $\tE$. In particular, we see how
the uniformity condition arises naturally from Kripke-Joyal forcing.

######  Definition 7.1.

Let $p\colon A\to X$ be a map in $\tE$. A _uniform trivial fibration
structure_ on $p$ consists of a function $j$ that assigns a diagonal filler
$j(m,u,v)$ to every commutative diagram of solid arrows of the form

${S}$${A}$${T}$${X\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{m}$$\scriptstyle{p}$$\scriptstyle{v}$

where $m$ is a cofibration, subject to the following _uniformity_ condition:
for every $t\colon T^{\prime}\to T$, giving rise to the following diagram with
a pullback square on the left,

${{t}^{*}(S)}$${S}$${A}$${T^{\prime}}$${T}$${X\mathrlap{,}}$$\scriptstyle{s}$$\scriptstyle{{t}^{*}(m)}$$\scriptstyle{u}$$\scriptstyle{m}$$\scriptstyle{p}$$\scriptstyle{t}$$\scriptstyle{v}$
(7.1)

we have $j({t}^{*}(m),us,vt)=j(m,u,v)\circ t$.

The next result recalls from [22, Theorem 9.1] that a trivial fibration
structure is determined by its values for the generating cofibrations, i.e.
those with representable codomains since a general diagonal filling problem
can be expressed as a colimit of filling problems for generating cofibrations.

######  Lemma 7.2.

Let $p\colon A\to X$ be a map in $\tE$. Then $p$ admits a uniform trivial
fibration structure if and only if there is a function $j$ that assigns a
diagonal filler $a=j(m,u,x)$ to every commutative diagram of solid arrows

${S}$${A}$${\mathsf{y}{c}}$${X\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{m}$$\scriptstyle{p}$$\scriptstyle{x}$$\scriptstyle{a}$
(7.2)

where $m$ is a generating cofibration, subject to the uniformity condition
indicated in the following diagram:

${{f}^{*}(S)}$${{S}}$${A}$${\mathsf{y}{d}}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{p}$$\scriptstyle{f}$$\scriptstyle{x}$

∎

We now wish to express the diagonal filling property in the internal type
theory. So let $p\colon A\to X$ be a small map, $m\colon
S\rightarrowtail\mathsf{y}{c}$ be a cofibration and consider their classifying
maps $\alpha\colon X\to U$ and $\varphi\colon\mathsf{y}{c}\to\Phi$,
respectively. The outer diagram in (7.2) can then be expressed equivalently in
the form,

${\\{\varphi\\}}$${X.\alpha}$${{\mathsf{y}{c}}}$${X\mathrlap{,}}$$\scriptstyle{(xi,u)}$$\scriptstyle{i}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{x}$
(7.3)

for a suitable $u\colon\\{\varphi\\}\to E$ with
$\mathsf{y}{c}.\\{\varphi\\}\vdash u\colon\alpha(xi)$. Recall thereby that
$i\colon\\{\varphi\\}\rightarrowtail\mathsf{y}{c}$ abbreviates the
comprehension,

${\\{\varphi\\}}$${\mathsf{y}{c}.\\{\varphi\\}}$${{\mathsf{y}{c}}}$${{\mathsf{y}{c}}\,\mathrlap{.}}$$\scriptstyle{i}$$\scriptstyle{=}$$\scriptstyle{p_{\\{\varphi\\}}}$$\scriptstyle{=}$
(7.4)

The commutative square (7.3) represents a partial element
$(\varphi,\lambda{u})$ of $\alpha$ at $x\colon\mathsf{y}{c}\to X$, in the
sense of 6.1, where $c\Vdash\varphi\colon\Phi$ and
$c\Vdash\lambda{u}\colon\\{\varphi\\}\to\alpha(x)$. We show that also the
existence of a diagonal filler for (7.3) can be written as a forcing
condition. First recall that for any $x\colon\mathsf{y}{c}\to X$ and
$a\colon\mathsf{y}{c}\to E$, the condition $c\Vdash a\mathord{\,:\,}\alpha(x)$
means that there is a (necessarily unique) lift of the form,

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

Then for maps $\varphi\colon\mathsf{y}{c}\to\Phi$ and $u\colon\\{\varphi\\}\to
E$ as in (7.3) above, we construct the type

$(u=^{\varphi}\\!a)\colon\mathsf{y}{c}\overset{}{\longrightarrow}U$

as follows. The maps $\varphi$ and $\alpha$ give rise to types over
$\mathsf{y}{c}$ as indicated below.

${E}$${\mathsf{y}{c}.\\{\varphi\\}}$${\mathsf{y}{c}.\alpha(x)}$${E}$${U}$${\Phi}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{i}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{\\{-\\}}$$\scriptstyle{\varphi}$$\scriptstyle{x}$$\scriptstyle{\alpha}$
(7.6)

The pullback of these two display maps may be regarded as weakenings of each
context by the other; we choose the one indicated in the following diagram:

${\mathsf{y}{c}.\\{\varphi\\}.\alpha(xi)}$${E}$${\mathsf{y}{c}.\\{\varphi\\}}$${\mathsf{y}{c}.\alpha(x)}$${E}$${U}$${\Phi}$${\mathsf{y}{c}}$${X}$${U\mathrlap{.}}$$\scriptstyle{p_{\alpha(xi)}}$$\scriptstyle{i}$$\scriptstyle{p_{\alpha(x)}}$$\scriptstyle{\\{-\\}}$$\scriptstyle{\varphi}$$\scriptstyle{x}$$\scriptstyle{\alpha}$
(7.7)

Maps $(xi,u)\colon\\{\varphi\\}\to X.\alpha$ and $(x,a)\colon\mathsf{y}{c}\to
X.\alpha$ as in (7.3) and (7.5) then determine two sections of the indicated
display map $p_{\alpha(xi)}$. Expressing the same thing in the type theory of
$\tE$, we have $\mathsf{y}{c}.\\{\varphi\\}\vdash u\colon\alpha(xi)$ and
$\mathsf{y}{c}.\\{\varphi\\}\vdash a(i)\colon\alpha(xi)$. Note that the
weakened term and type $\mathsf{y}{c}.\\{\varphi\\}\vdash
a(i)\colon\alpha(xi)$ do not depend on $\\{\varphi\\}$. Over $\mathsf{y}{c}$
we can then define the type

$\textstyle(u=^{\varphi}\\!a)\ =_{\mathrm{def}}\
\prod_{\\{\varphi\\}}\,u=_{\alpha(xi)}a(i)\mathrlap{.}$ (7.8)

The proposition $u=^{\varphi}\\!a$ expresses the condition that “$u$ is the
restriction to $\\{\varphi\\}$ of $a$” or, equivalently, “$u$ extends along
$\\{\varphi\\}\rightarrowtail\mathsf{y}{c}$ to $a$”, as in [35, Definition
5.1]. Diagonal filling of (7.3) can now be expressed in terms of forcing as
follows.

######  Lemma 7.3.

Let $\alpha\colon X\to U$, $x\colon\mathsf{y}{c}\to X$,
$\varphi\colon\mathsf{y}{c}\to\Phi$ and $u^{\prime}\colon\\{\varphi\\}\to
X.\alpha$ such that the diagram of solid arrows

${{\\{\varphi\\}}}$${X.\alpha}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{i}$$\scriptstyle{u^{\prime}}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{x}$$\scriptstyle{a^{\prime}}$

commutes. Then the following conditions are equivalent.

  1. (i)

There is a diagonal filler $a^{\prime}\colon\mathsf{y}c\to X.\alpha$ as
indicated in the diagram.

  2. (ii)

There are maps $u\colon\\{\varphi\\}\to E$ and $a\colon\mathsf{y}{c}\to E$
such that

$c\Vdash a\colon\alpha(x)\mathrlap{,}\quad c\Vdash\lambda
u\colon\\{\varphi\\}\to\alpha(x)\mathrlap{,}\quad c\Vdash
u=^{\varphi}\\!a\mathrlap{,}$

and $u^{\prime}=(xi,u)$, $a^{\prime}=(x,a)$.

  * Proof.

We have already observed that maps $a\colon\mathsf{y}{c}\to E$ such that
$c\Vdash a\colon\alpha(x)$ correspond uniquely to maps
$(x,a)\colon\mathsf{y}{c}\to X.\alpha$ making the bottom triangle in the
diagram commute. While item (i) states that the condition $c\Vdash\lambda
u\colon\\{\varphi\\}\to\alpha(x)$ is equivalent to having a map
$(xi,u)\colon\\{\varphi\\}\to X.\alpha$ making the outer square in the diagram
commute.

It therefore suffices to show that $c\Vdash u=^{\varphi}\\!a$ just if the top
triangle also commutes, for such $u$ and $a$. Unfolding the definition of
$u=^{\varphi}\\!a$, assume that

$\textstyle c\Vdash\prod_{\\{\varphi\\}}\,u=_{\alpha(xi)}a(i)\,.$

Although the type $\prod_{\\{\varphi\\}}\,u=_{\alpha(xi)}a(i)$ is a
proposition and therefore requires no explicit forcing term, let us assume one
in order to apply the rule of forcing for dependent products (4.16) literally.
Thus suppose we have

$\textstyle c\Vdash t\colon\prod_{\\{\varphi\\}}\,u=_{\alpha(xi)}a(i)\,.$

Then by 4.16, for every $f\colon d\to c$ and every $d\Vdash
e\colon\\{\varphi(f)\\}$, we have

$d\Vdash\mathsf{app}(t(f),e)\colon(u=_{\alpha(xi)}a(i))(f,e)\,,$ (7.9)

where we applied part (ii) of 4.16.222We applied it with $\\{\varphi\\}$ for
$\alpha$, $u=_{\alpha(xi)}a(i)$ for $\beta$ and $\mathsf{y}{c}$ for $X$; and
$\operatorname{id}_{\mathsf{y}{c}}$ for $x\colon\mathsf{y}{c}\to X$. The
substitution in the type in (7.9) can be calculated as follows:

$\big{(}u=_{\alpha(xi)}a(i)\big{)}(f,e)\ =\
\big{(}u(f,e)=_{\alpha(xi(f,e))}a(i(f,e))\big{)}\,.$

Thus, equivalently, for every $f\colon d\to c$ and every lift
$(f,e)\colon\mathsf{y}{d}\to\\{\varphi\\}$, we have

$d\Vdash u(f,e)=_{\alpha(xi(f,e))}a(i(f,e))\,,$ (7.10)

as indicated in the following diagram:

${{\\{\varphi\\}}}$${X.\alpha}$${\mathsf{y}{d}}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{i}$$\scriptstyle{u^{\prime}}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{(f,e)}$$\scriptstyle{f}$$\scriptstyle{x}$$\scriptstyle{a^{\prime}}$
(7.11)

But $a(i(f,e))=a(f)$ and $\alpha(xi(f,e))=\alpha(xf)$, so from (7.10) we have

$d\Vdash u(f,e)=_{\alpha(xf)}a(f)\,.$

Thus

$u^{\prime}(f,e)=(xi,u)(f,e)=(xi(f,e),u(f,e))=(xf,u(f,e))\\\
=(xf,af)=(x,a)f=a^{\prime}f=a^{\prime}i(f,e).$ (7.12)

Since this holds for all $(f,e)$, we have $u^{\prime}=a^{\prime}i$, as
required, by Lemma 4.3.

Note that the uniformity condition for forcing the dependent product is
trivial because we are forcing a proposition. ∎

######  Remark 7.4.

Observe that by function extensionality the type $(u=^{\varphi}\\!a)$ defined
in (7.8) is equivalent to the type $\lambda u=\lambda a$, where the equality
is on the function type
$\alpha(x)^{\\{\varphi\\}}=(\\{\varphi\\}\to\alpha(x))$ over $\mathsf{y}{c}$
(making use of item (i)). The term $\lambda{a}$ here (see 3.13) therefore
represents the restriction to $\\{\varphi\\}$ of the constant $a$-valued
function and we have $(u=^{\varphi}\\!a)\ =\ (\lambda u=\lambda a)$.

We can now construct a classifying type $\mathsf{TFib}(\alpha)$ for trivial
fibration structures on $\alpha$ (cf. [3, Section 6.2]).

$\textstyle\mathsf{TFib}(\alpha)\ =_{\mathrm{def}}\
\prod_{\varphi\mathord{\,:\,}\Phi}\,\prod_{v\mathord{\,:\,}\alpha^{\\{\varphi\\}}}\,\sum_{a\mathord{\,:\,}\alpha}\,v=\lambda
a\mathrlap{.}$ (7.13)

Note that under the propositions as types reading, this type expresses that
every partial element of $\alpha$ extends to a total one. Indeed, using the
partial elements endofunctor $T$ from (6.2), we can write this in the form

$\textstyle\mathsf{TFib}(\alpha)=\prod_{(\varphi,v)\mathord{\,:\,}P\alpha}\,\sum_{a\mathord{\,:\,}\alpha}\,v=\lambda
a\mathrlap{.}$ (7.14)

The notion of a uniform trivial fibration structure now arises inexorably from
forcing of the type $\mathsf{TFib}(\alpha)$ of trivial fibration structures on
$\alpha$.

######  Theorem 7.5.

Let $\alpha\colon X\to U$. The following conditions are equivalent.

  1. (i)

There is a term $t$ such that $X\vdash t\mathord{\,:\,}\mathsf{TFib}(\alpha)$.

  2. (ii)

For each $x\colon\mathsf{y}{c}\to X$ we have $c\Vdash
t_{x}\mathord{\,:\,}\mathsf{TFib}(\alpha)(x)$, uniformly in $x$.

  3. (iii)

There is a uniform trivial fibration structure on
${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$.

  * Proof.

Observe that (i) and (ii) are equivalent by 4.5.

Now suppose (ii). For each $x\colon\mathsf{y}{c}\to X$, we have $c\Vdash
t_{x}\mathord{\,:\,}\mathsf{TFib}(\alpha)(x)$, uniformly in $x$. By definition
(7.14) this means

$\textstyle c\Vdash
t_{x}\colon\prod_{(\varphi,v)\mathord{\,:\,}P\alpha(x)}\,\sum_{a\mathord{\,:\,}\alpha(x)}\,v=\lambda
a\mathrlap{.}$

Unwinding the forcing conditions using 4.16 and 4.14, we see that for every
$f\colon d\to c$ and every

$\textstyle
d\Vdash(\varphi,v)\colon\sum_{\varphi\mathord{\,:\,}\Phi}\,\alpha(xf)^{\\{\varphi\\}},$
(7.15)

we have
$t_{xf}(\varphi,v)=\big{(}t_{xf}(\varphi,v)_{1},t_{xf}(\varphi,v)_{2}\big{)}$
with

$\displaystyle d$ $\displaystyle\Vdash t_{xf}(\varphi,v)_{1}\colon\alpha(xf)$
(7.16) $\displaystyle d$ $\displaystyle\Vdash t_{xf}(\varphi,v)_{2}\colon
v=\lambda(t_{xf}(\varphi,v)_{1}).$ (7.17)

Without loss of generality, we may assume that $v=\lambda u$, so that by (7.4)
the second condition becomes

$d\Vdash t_{xf}(\varphi,\lambda u)_{2}\colon
u=^{\varphi}\\!t_{xf}(\varphi,\lambda u)_{1}.$ (7.18)

Moreover, for any $g\colon e\to d$, we have

$(t_{xf}(\varphi,\lambda u))g=t_{xfg}(\varphi g,\lambda ug)\,.$ (7.19)

Unfolding the condition (7.15) using 6.5 yields a commutative diagram

${{\\{\varphi\\}}}$${X.\alpha}$${\mathsf{y}{d}}$${X\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{xf}$
(7.20)

and the uniformity condition yields, for any $g\colon e\to d$, a further
pullback diagram on the left,

${{\\{\varphi
g\\}}}$${{\\{\varphi\\}}}$${X.\alpha}$${\mathsf{y}{e}}$${\mathsf{y}{d}}$${X\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{g}$$\scriptstyle{xf}$
(7.21)

Now we can apply Lemma 7.3 to (7.16) and (7.18) to conclude that
$t_{xf}(\varphi,\lambda u)_{1}$ is a diagonal filler in

${{\\{\varphi\\}}}$${X.\alpha}$${{\mathsf{y}{d}}}$${X\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{xf}$

while $t_{xfg}(\varphi g,\lambda ug)_{1}$ is similarly a diagonal filler for
the outer rectangle in (7.21).

In this way, forcing $\mathsf{TFib}(\alpha)$ produces diagonal fillers

$j(\varphi,xf,u)\ =_{\mathrm{def}}\ t_{xf}(\varphi,u)_{1}$ (7.22)

against all generating cofibrations
$\\{\varphi\\}\rightarrowtail\mathsf{y}{d}$. Finally, the uniformity of these
fillers $j(\varphi,xf,u)$ with respect to all $g\colon e\to d$ is provided by
the uniformity condition (7.19).

The inference from (iii) to (ii) is essentially the same argument backwards. ∎

######  Corollary 7.6.

Let $\alpha\colon X\to U$. The display map $p_{\alpha}\colon X.\alpha\to X$ is
a uniform trivial fibration if and only if $\tE\Vdash
t\colon\mathsf{TFib}(\alpha)$ for some $t$. Indeed, $t$ itself may be regarded
as a trivial fibration structure on $p_{\alpha}$ in virtue of the
specification in (7.22). ∎

### Uniform trivial fibrations as algebras

For $X\in\tE$, we defined the pointed endofunctor
$P_{X}\colon\tE/_{X}\to\tE/_{X}$ on the slice topos $\tE/_{X}$ in (6.2). An
algebra for $P_{X}$ consists of an object $p\colon A\to X$ of $\tE/_{X}$ and a
retraction of $\eta_{A}\colon A\to P_{X}(A)$ over $X$, i.e. a map $s\colon
P_{X}(A)\to A$ over $X$ such that

${A}$${P_{X}(A)}$${A}$$\scriptstyle{\eta_{A}}$$\scriptstyle{\operatorname{id}_{A}}$$\scriptstyle{s}$

commutes. Such an algebra is the same thing as a uniform fibration structure
on $p\colon A\to X$ ([22, Theorem 9.8]). We give a new simple proof of this
fact using forcing, which in particular avoids any reference to Garner’s small
object argument [23] and left Kan extensions (cf. [3, Proposition 8]).

For this, let us first consider the object $P\text{-}\mathsf{alg}(A)$ of
algebra structures on $p$ by taking the following pullback in $\tE/_{X}$,
where we write $A$ for $p\colon A\to X$ as an object in $\tE/_{X}$ and $P$ for
$P_{X}$:

${P\text{-}\mathsf{alg}(A)}$${{A^{P(A)}}}$${1}$${{A^{A}}\mathrlap{.}}$$\scriptstyle{A^{\eta_{A}}}$$\scriptstyle{\operatorname{id}_{A}^{\sharp}}$
(7.23)

If $p\colon A\to X$ is classified by $\alpha\colon X\to U$, then
$P\text{-}\mathsf{alg}(A)\to X$ is classified by the map
$P\text{-}\mathsf{alg}(\alpha)\colon X\to U$ defined by setting

$\textstyle
P\text{-}\mathsf{alg}(\alpha)=\sum_{s\mathord{\,:\,}\alpha^{P\alpha}}\,s\circ\eta=\operatorname{id}_{A}\mathrlap{.}$
(7.24)

We can then strengthen 7.5 to the following isomorphism.

######  Theorem 7.7.

Let $\alpha\colon X\to U$. Then there is an isomorphism
$P\text{-}\mathsf{alg}(\alpha)\cong\mathsf{TFib}(\alpha)$.

  * Proof.

Recall the description of $\mathsf{TFib}(\alpha)$ in (7.14). Applying to it
the type-theoretic axiom of choice (3.5) yields a natural isomorphism

$\textstyle\left(\prod_{(\varphi,v)\mathord{\,:\,}P\alpha}\,\sum_{a\mathord{\,:\,}\alpha}\,v=\lambda
a\right)\cong\left(\sum_{s\mathord{\,:\,}\alpha^{P\alpha}}\,\prod_{(\varphi,v)\mathord{\,:\,}P\alpha}\,v=\lambda\,\mathsf{app}(s,(\varphi,v))\right).$
(7.25)

We claim that, up to natural isomorphism, the right hand side is the object
$P\text{-}\mathsf{alg}(\alpha)$ of algebra structures on $\alpha$ from (7.24).
It suffices to show that (in the context extended by
$s\colon\alpha^{P\alpha}$) there is a natural isomorphism

$\textstyle\prod_{(\varphi,v)\mathord{\,:\,}P\alpha}\,\big{(}v=\lambda\,\mathsf{app}(s,(\varphi,v))\big{)}\
\cong\ \prod_{a\mathord{\,:\,}\alpha}\,\mathsf{app}(s\circ\eta,a)=a)\,.$
(7.26)

Moreover, since both sides are now propositions, it suffices to show that they
are logically equivalent, which we will do by forcing.

Thus take any $x\colon\mathsf{y}{c}\to X$ and any $s\colon\mathsf{y}{c}\to E$
with $c\Vdash s\colon({{P\alpha}\to\alpha})(x)$ and suppose that

$\textstyle
c\Vdash\prod_{(\varphi,v)\mathord{\,:\,}P\alpha(x)}\,v=\lambda\,\mathsf{app}(s,(\varphi,v))\mathrlap{.}$
(7.27)

Then for all $f\colon d\to c$ and all $(\varphi,v)$ such that

$d\Vdash(\varphi,v)\mathord{\,:\,}P\alpha(xf)\mathrlap{,}$ (7.28)

we have

$d\Vdash v=\lambda\,\mathsf{app}(s(f),(\varphi,v))\mathrlap{.}$ (7.29)

To see what this means, consider the diagram on the left in (7.30) below:

${\\{\varphi\\}}$${{\alpha(x)}}$${\mathsf{y}{d}}$${{P\alpha(x)}\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{i}$$\scriptstyle{\eta}$$\scriptstyle{(\varphi,\lambda
u)}$$\scriptstyle{j}$$\scriptstyle{\sigma_{f}}$
${\\{\mathsf{t}\\}}$${\alpha(x)}$${\mathsf{y}{d}}$${P\alpha(x)\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{\eta}$$\scriptstyle{(\mathsf{t},a(f))}$$\scriptstyle{a(f)}$$\scriptstyle{\sigma_{f}}$
(7.30)

The solid part is the pullback in $\tE/\mathsf{y}{c}$ arising from (7.28) and
the forcing rules for $P\alpha(x)$ in 6.5, with $\lambda u=v$, and we have
written $\mathsf{y}{d}$ for the map
$\mathsf{y}{f}\colon\mathsf{y}{d}\to\mathsf{y}{c}$ and $\alpha(x)$ for the
projection $p_{\alpha(x)}\colon\mathsf{y}{c}.\alpha(x)\to\mathsf{y}{c}$ and
similarly for $P\alpha(x)$.

By 7.4, the condition (7.29) thus becomes

$\textstyle d\Vdash u=^{\varphi}\mathsf{app}(s(f),(\varphi,\lambda u)).$

By Lemma 7.3, the map $j=\mathsf{app}(s(f),(\varphi,\lambda u))$ therefore
fits on the diagonal in the lefthand diagram of (7.30) and makes the top
triangle commute.

Take $\sigma_{f}$ with $\lambda\sigma_{f}=s(f)$, so that

$j=\mathsf{app}(s(f),(\varphi,\lambda
u))=\mathsf{app}(\lambda\sigma_{f},(\varphi,\lambda
u))=\sigma_{f}(\varphi,\lambda u).$

Then we claim that $\sigma_{f}\,\eta=\operatorname{id}$, which will give the
required righthand side of (7.26).

To prove the claim, recall that (7.29) holds for all $f\colon d\to c$ and all
$(\varphi,\lambda u)$ with

$d\Vdash(\varphi,\lambda u)\mathord{\,:\,}P\alpha(xf)\mathrlap{.}$

Since for any $c\Vdash a\mathord{\,:\,}\alpha(x)$, we can take
$c\Vdash(\mathsf{t},\lambda a)\mathord{\,:\,}P\alpha(x)$ to get
$d\Vdash(\mathsf{t},\lambda a(f))\mathord{\,:\,}P\alpha(xf)$, we will then
have $a(f)=\sigma_{f}\,(\mathsf{t},a(f))$. Indeed, in this case we have
$i=\operatorname{id}\colon\\{\mathsf{t}\\}\rightarrowtail\mathsf{y}{d}$ and so
$u=a(f)$ as on the right in (7.30) above, so the (partial) commutativity of
the diagram on the left specialises on the right to give
$a(f)=\sigma_{f}\,(\mathsf{t},a(f))$.

Since this holds for all $f\colon d\to c$ and is uniform with respect to all
$g\colon e\to d$, and since $(\mathsf{t},a_{f})=\eta(a_{f})$, we conclude that

$\textstyle
c\Vdash\prod_{a\mathord{\,:\,}\alpha(x)}\,(\sigma\,\eta(a)=a\big{)}\mathrlap{.}$

Conversely, $\operatorname{id}=s\circ\eta$ implies $u=s\circ\eta\circ u$, and
since $\eta\circ u=(\varphi,\lambda u)\circ i$, it follows that
$u=s\circ(\varphi,u)\circ i$, and thus
$u=^{\varphi}\mathsf{app}(s,(\varphi,u))$. ∎

######  Corollary 7.8 (Pullback stability of $\mathsf{TFib}$).

Let $\alpha\colon X\to U$. Then the object $\mathsf{TFib}(\alpha)$ over $X$ is
stable under pullback along any map $t\colon Y\to X$, in the sense that the
right hand square below is a pullback whenever the left hand one is:

${Y.\beta}$${X.\alpha}$${Y}$${X\mathrlap{,}}$$\scriptstyle{t}$
${\mathsf{TFib}(\beta)}$${\mathsf{TFib}(\alpha)}$${Y}$${X\mathrlap{.}}$$\scriptstyle{t}$

In other words, ${t}^{*}\mathsf{TFib}(\alpha)\cong\mathsf{TFib}(\alpha(t))$.

  * Proof.

Note that we have simplified the notation $X.\mathsf{TFib}(\alpha)\to X$ to
$\mathsf{TFib}(\alpha)\to X$. The description in (7.23) involves only
$P$-algebras, exponentials, and pullbacks, all of which are stable under all
pullbacks (as is $P$ itself). ∎

It also follows from 7.7 that, for every small $A\in\tE$, the unique map
$P{A}\to 1$ is a uniform trivial fibration, as it can be equipped with the
$(P,\eta)$-algebra structure $\mu_{A}\colon P{P{A}}\to P{A}$. Thus, we have
the following result.

######  Corollary 7.9.

Every small map can be factored as a cofibration followed by a uniform trivial
fibration.

  * Proof.

Consider $p\colon A\to X$ as an object of the slice category $\tE/_{{X}}$ and
apply the functor $P_{X}\colon\tE/_{X}\to\tE/_{X}$ to form the object
$P_{X}(p)\colon\operatorname{dom}({P_{X}(p)})\to X$ in $\tE/_{X}$. The map
$\eta_{p}\colon p\to P_{X}(p)$ is a cofibration in $\tE/_{X}$, hence in $\tE$,
while $P_{X}(p)$ is a uniform trivial fibration, as was just observed. ∎

We conclude the section by constructing a universal uniform trivial fibration,
using the method of [3, Proposition 63]. For $\alpha\colon X\to U$, applying
7.8 to the pullback in (1.8) we obtain a pullback diagram as the outside
square below, where $\operatorname{id}\colon U\to U$ of course classifies
$\pi\colon E\to U$.

${\mathsf{TFib}(\alpha)}$${\mathsf{TFib}(\operatorname{id})}$${X}$${U\mathrlap{.}}$$\scriptstyle{\alpha}$$\scriptstyle{\bar{\alpha}}$
(7.31)

Trivial fibration structures on $\alpha$, i.e. sections of
$\mathsf{TFib}(\alpha)$, then correspond uniquely to factorisations
$\bar{\alpha}$, as indicated.

######  Theorem 7.10 (Universal trivial fibration).

There exists a universal small uniform trivial fibration
${\mathsf{TFib}_{\bullet}}\to\mathsf{TFib}$, in the sense that every small
uniform trivial fibration $p\colon A\to X$ is a pullback of
${\mathsf{TFib}_{\bullet}}\to\mathsf{TFib}$ along a canonically determined
classifying map $\bar{\alpha}\colon X\to\mathsf{TFib}$.

${A}$${{\mathsf{TFib}_{\bullet}}}$${X}$${\mathsf{TFib}\mathrlap{.}}$$\scriptstyle{p}$$\scriptstyle{\bar{\alpha}}$
(7.32)

  * Proof.

Define $\mathsf{TFib}=\mathsf{TFib}(\operatorname{id})$ and
${\mathsf{TFib}_{\bullet}}\to\mathsf{TFib}$ by the pullback indicated on the
right below.

${A}$${E}$${{\mathsf{TFib}_{\bullet}}\mathrlap{.}}$${X}$${U}$${\mathsf{TFib}}$$\scriptstyle{\pi}$$\scriptstyle{\bar{\alpha}}$$\scriptstyle{\alpha}$

As was just shown (7.31), a trivial fibration structure on $A\to X$
corresponds to a factorisation $\bar{\alpha}$ of $\alpha$, thus making a
pullback square as indicated on the left above. In particular, taking
$X=\mathsf{TFib}$ and $\alpha$ the projection $\mathsf{TFib}\to U$ and
$\bar{\alpha}=\operatorname{id}$, we see that
${\mathsf{TFib}_{\bullet}}\to\mathsf{TFib}$ is itself a trivial fibration, and
thus it is a universal one. ∎

######  Remark 7.11.

Using variables, the identity map $\operatorname{id}\colon U\to U$ is the
interpretation of the judgement $\alpha\colon U\vdash\alpha\colon U$, from
which we also have $\alpha\colon U\vdash\mathsf{TFib}(\alpha)\colon U$. Thus
for the type $\mathsf{TFib}=U.\mathsf{TFib}(\operatorname{id})$ we have
$\mathsf{TFib}=\sum_{\alpha\colon U}\,\\!\mathsf{TFib}(\alpha)$ and then
${\mathsf{TFib}_{\bullet}}=\sum_{(\alpha,t)\colon\mathsf{TFib}}\,\alpha$.

##  8\. Uniform fibrations

The definition of a uniform fibration was originally introduced in the setting
of categories of cubical sets in [9, 15] to provide a constructive model of
the Univalence Axiom. The notion was analysed in terms of algebraic weak
factorisation systems in [45] and generalised to the setting of presheaf
categories equipped with a class of cofibrations and a suitable interval
object in [22, 3]. The definition of [15, Section 8.2] was rephrased in the
internal type theory of such a category in [35, Definition 5.6]. Here, we
relate precisely the category-theoretic and the type-theoretic formulations of
this notion. In particular, we show how this notion arises naturally from our
Kripke-Joyal forcing for the internal type theory of a presheaf category
$\tE=\mathrm{Psh}(\cC)$.

We assume a class of cofibrations as in 5.1, classified by
$\Phi\rightarrowtail\Omega$. The next definition introduces the notion of an
interval object in $\tE$ with which we shall work.

######  Definition 8.1.

An interval with connections is an object $\mathrm{I}$ in $\tE$ equipped with
endpoints $\delta^{k}\colon 1\to\mathrm{I}$ and connections
$c_{k}\colon\mathrm{I}\times\mathrm{I}\to\mathrm{I}$, for $k=0,1$, satisfying
the following axioms.

  1. (i)

$\delta^{0}\neq\delta^{1}$

  2. (ii)

$\delta^{k}\colon 1\to\mathrm{I}$ is a cofibration, for $k=0,1$.

  3. (iii)

The diagrams

${\mathrm{I}}$${\mathrm{I}\times\mathrm{I}}$${\mathrm{I}}$${1}$${\mathrm{I}}$${1\mathrlap{,}}$$\scriptstyle{(\delta^{k},1)}$$\scriptstyle{c_{k}}$$\scriptstyle{(1,\delta^{k})}$$\scriptstyle{\delta^{k}}$$\scriptstyle{\delta^{k}}$
${\mathrm{I}}$${\mathrm{I}\times\mathrm{I}}$${\mathrm{I}}$${\mathrm{I}}$$\scriptstyle{(\delta^{1-k},1)}$$\scriptstyle{c_{1-k}}$$\scriptstyle{(1,{\delta^{1-k}})}$

commute, for $k=0,1$.

In order to recall the definition of a uniform fibration from [22, Section 7],
we define the naive trivial cofibrations to be pushout-products of the form

$c\otimes\delta_{k}\colon T+_{S}(S\times\mathrm{I})\rightarrowtail
T\times\mathrm{I}\mathrlap{,}$

for an arbitrary cofibration $m\colon S\rightarrowtail T$ and an endpoint
$\delta_{k}\colon 1\rightarrowtail\mathrm{I}$, for $k=0,1$ (see [22, Section
3] for the definition of this pushout-product). This construction is not
stable under pullback in general, but it is so for maps $t\colon T^{\prime}\to
T$, for which one has a pullback square

${T^{\prime}+_{S^{\prime}}(S^{\prime}\times\mathrm{I})}$${T+_{S}(S\times\mathrm{I})}$${T^{\prime}\times\mathrm{I}}$${T\times\mathrm{I}\mathrlap{,}}$$\scriptstyle{m^{\prime}\otimes\delta_{k}}$$\scriptstyle{m\otimes\delta_{k}}$$\scriptstyle{t\times\mathrm{I}}$
(8.1)

where $m^{\prime}\colon S^{\prime}\to T^{\prime}$ is the pullback of $m$ along
$t$.

######  Definition 8.2.

Let $p\colon A\to X$ be a small map. A _uniform fibration structure_ on $p$
consists of a function $j$ that assigns a dotted filler $j(m,u,v)\colon
T\times\mathrm{I}\to A$ to every diagram of solid arrows

${T+_{S}(S\times\mathrm{I})}$${A}$${T\times\mathrm{I}}$${X\mathrlap{,}}$$\scriptstyle{u}$$\scriptstyle{m\otimes\delta_{k}}$$\scriptstyle{v}$

where $m$ is a cofibration, and $k=0,1$, subject to the following uniformity
condition: for any map $t\colon T^{\prime}\to T$ and induced pullback square
on the left,

${T^{\prime}+_{S^{\prime}}(S^{\prime}\times\mathrm{I})}$${T+_{S}(S\times\mathrm{I})}$${A}$${T^{\prime}\times\mathrm{I}}$${T\times\mathrm{I}}$${X\mathrlap{,}}$$\scriptstyle{m^{\prime}\otimes\delta_{k}}$$\scriptstyle{u}$$\scriptstyle{t\times\mathrm{I}}$$\scriptstyle{v}$
(8.2)

we have

$j(m^{\prime},u(t\times i)^{\prime},v(t\times
i))=j(m,u,v)\circ(t\times\mathrm{I})\,,$

where $(t\times\mathrm{I})^{\prime}$ is the evident pullback of
$(t\times\mathrm{I})$.

As a functor on the arrow category $\tE^{\rightarrow}$, the pushout-product
$(-)\otimes\delta_{k}$ has a right adjoint $\delta_{k}\Rightarrow(-)$, the
pullback-hom, taking $p\colon A\to X$ to the map $\delta_{k}\Rightarrow p$
indicated in the following diagram.

${A^{\mathrm{I}}}$${X^{\mathrm{I}}\times_{X}A}$${A}$${X^{\mathrm{I}}}$${X\mathrlap{.}}$$\scriptstyle{p^{\mathrm{I}}}$$\scriptstyle{\delta_{k}\Rightarrow{p}}$$\scriptstyle{A^{\delta_{k}}}$$\scriptstyle{p}$$\scriptstyle{X^{\delta_{k}}}$
(8.3)

By adjointness, these operations can be seen to satisfy

$(m\otimes\delta_{k})\pitchfork p\quad\text{if and only if}\quad
m\pitchfork(\delta_{k}\Rightarrow f)\mathrlap{.}$ (8.4)

Indeed, more is true: by adjointness there is a natural bijection between the
diagonal fillers witnessing the statement $(m\otimes\delta_{k})\pitchfork p$
and those establishing $m\pitchfork(\delta_{k}\Rightarrow f)$.

The condition in (8.2) for $p\colon A\to X$ to be a uniform fibration can
therefore be reformulated as the requirement that, for all cofibrations
$m\colon S\rightarrowtail T$, we have $m\pitchfork(\delta_{k}\Rightarrow p)$
uniformly in $m$. But this of course just says that $\delta_{k}\Rightarrow p$
is a uniform _trivial_ fibration in the sense of 7.1. We record this for later
use (cf. [22, Proposition 7.4]).

######  Proposition 8.3.

A small map $p\colon A\to X$ is a uniform fibration if and only if the map
$\delta_{k}\Rightarrow p\colon A^{\mathrm{I}}\to X^{\mathrm{I}}\times_{X}A$ is
a uniform trivial fibration, for $k=0,1$. ∎

######  Remark 8.4.

As was the case for uniform trivial fibrations (Lemma 7.2), a uniform
fibration structure is determined by its values on the generating trivial
cofibrations, defined as those of the form $m\otimes\delta_{k}$ where $m\colon
S\rightarrowtail\mathsf{y}{c}$ is a cofibration with a representable codomain.
We leave it to the reader to reformulate 8.2 of a uniform fibration structure
on a map $p\colon A\to X$ in these terms.

Our aim now is to show how 8.2 can be formulated in the internal type theory
of $\tE$ and how it is thereby related to forcing. In light of 8.3 we would
like to use 7.5 to show that there is an element of
$\mathsf{TFib}(\delta_{k}\Rightarrow{f})$ over $X$, but for this to make sense
$\delta_{k}\Rightarrow{f}$ would need to be given as a display map. Thus let
$\alpha\colon X\to U$ classify $A\to X$. Consider the case $k=0$ and let
$\mathsf{ev_{0}}\colon X^{\mathrm{I}}\rightarrow X$ be the evaluation at the
point $\delta_{0}\colon 1\to\mathrm{I}$ (i.e.
$\mathsf{ev_{0}}=X^{\delta_{0}}$), so that the pullback in (8.3) above becomes

${X^{\mathrm{I}}.\alpha(\mathsf{ev_{0}})}$${X.\alpha}$${X^{\mathrm{I}}}$${X\mathrlap{.}}$$\scriptstyle{\mathsf{ev_{0}}}$
(8.5)

In what follows, we adopt the indexed-family style of writing a display map
$X.\alpha\to~{}X$ as $\sum_{x\colon X}\,\alpha(x)\to X$ for easier comparison
with [35].

######  Proposition 8.5.

Let $\alpha\colon X\to U$. Then the following conditions are equivalent.

  1. (i)

The projection $p\colon\sum_{x\mathord{\,:\,}X}\,\alpha(x)\to X$ admits a
uniform fibration structure.

  2. (ii)

There is a term of type

$\textstyle\prod_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\Big{(}\prod_{a\mathord{\,:\,}\alpha(x_{0})}\,\mathsf{TFib}(F_{0}(x,a))\times\prod_{a\mathord{\,:\,}\alpha(x_{1})}\,\mathsf{TFib}(F_{1}(x,a))\Big{)}\,,$

where $\mathsf{TFib}$ is as defined in (7.13).

Moreover, there is a bijection between such structures and such terms.

  * Proof.

Writing $x_{0}=\mathsf{ev_{0}}(x)$, for (8.5) we then have,

${\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\alpha(x_{0})}$${\sum_{x\mathord{\,:\,}X}\,\alpha(x)}$${X^{\mathrm{I}}}$${X\mathrlap{.}}$$\scriptstyle{\mathsf{ev_{0}}}$

Using the isomorphism

$\textstyle A^{\mathrm{I}}\ \cong\
\big{(}\sum_{x\mathord{\,:\,}X}\,\alpha(x)\big{)}^{\mathrm{I}}\ \cong\
\prod_{i\mathord{\,:\,}\mathrm{I}}\,\sum_{x\mathord{\,:\,}X}\,\alpha(x)\cong\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})\mathrlap{,}$

the map $p^{\mathrm{I}}\colon A^{\mathrm{I}}\rightarrow X^{\mathrm{I}}$ may be
rewritten as a display map over $X^{\mathrm{I}}$ in the form

$\textstyle\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})\to
X^{\mathrm{I}}\,.$

Up to isomorphism, our previous diagram (8.3) then becomes

${\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})}$${\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\alpha(x_{0})}$${\sum_{x\mathord{\,:\,}X}\,\alpha(x)}$${X^{\mathrm{I}}}$${X\mathrlap{.}}$$\scriptstyle{\delta_{0}\Rightarrow{p}}$$\scriptstyle{\mathsf{ev}_{0}}$

Thus for any $x\colon\mathsf{y}{c}\to X^{\mathrm{I}}$ the map
$(\delta_{0}\Rightarrow p)(x)$ over $\mathsf{y}{c}$ is the $0^{th}$ projection
of the type family $\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})$,

$\textstyle\pi_{0}\colon\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})\to\alpha(x_{0})\mathrlap{,}$

as indicated in the following diagram:

${{\prod_{i\mathord{\,:\,}\mathrm{I}}\,}\alpha(x_{i})}$${\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})}$${\alpha(x_{0})}$${\sum_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\alpha(x_{0})}$${\sum_{x\mathord{\,:\,}X}\,\alpha(x)}$${\mathsf{y}{c}}$${X^{\mathrm{I}}}$${X\mathrlap{.}}$$\scriptstyle{\pi_{0}}$$\scriptstyle{\delta_{0}\Rightarrow{p}}$$\scriptstyle{x}$$\scriptstyle{\mathsf{ev}_{0}}$
(8.6)

Now for any $x\colon\mathsf{y}{c}\to X^{\mathrm{I}}$ and section
$(x,a)\colon\mathsf{y}{c}\to\alpha(x_{0})$, we define
$F_{0}(x,a)\colon\mathsf{y}{c}\to U$ to be the fiber of $\pi_{0}$ at $(x,a)$,

$\textstyle F_{0}(x,a)\ =_{\mathrm{def}}\
\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})}\,s_{0}=a\mathrlap{.}$
(8.7)

The display map

$\textstyle\sum_{(x,a)\mathord{\,:\,}\sum_{x\colon
X^{\mathrm{I}}}\,\alpha(x_{0})}\,F_{0}(x,a)\ \overset{}{\longrightarrow}\
\sum_{x\colon X^{\mathrm{I}}}\,\alpha(x_{0})$

is then isomorphic to ${\delta_{0}\Rightarrow{p}}$ over $\sum_{x\colon
X^{\mathrm{I}}}\,\alpha(x_{0})$. Similarly, for
$(x,a)\colon\mathsf{y}{c}\to\alpha(x_{1})$, let
$F_{1}(x,a)\colon\mathsf{y}{c}\to U$ be the analogous type consisting of
fibers of
$\pi_{1}\colon\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})\to\alpha(x_{1})$
rather than $\pi_{0}$. The type in item (ii) then classifies uniform fibration
structures on $p\colon\sum_{x\mathord{\,:\,}X}\,\alpha(x)\to X$ by 7.5. ∎

Recall from [35, Definition 5.6] the following definition of a _$0$ -directed
filling structure_ $\mathsf{Fill}_{0}(\alpha)\colon U$ on an
$\mathrm{I}$-indexed family of types $\alpha\colon\mathrm{I}\to U$.

$\textstyle\mathsf{Fill}_{0}(\alpha)=\\\
\textstyle\prod_{\varphi\mathord{\,:\,}\Phi}\,\prod_{v\mathord{\,:\,}\\{\varphi\\}\to\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha_{i}}\,\prod_{a\mathord{\,:\,}\alpha_{0}}\,({\tilde{v}_{0}}=\lambda{a})\to\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha_{i}}(s_{0}=_{\alpha_{0}}a)\times({v}=\lambda{s})\,,$
(8.8)

where

$\textstyle\tilde{(-)}\ \colon\
\big{(}\\{\varphi\\}\to\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha_{i}\big{)}\
\cong\ \prod_{i\mathord{\,:\,}\mathrm{I}}\,\\{\varphi\\}\to\alpha_{i}$

is the canonical isomorphism, and the type $(v=\lambda s)$ is as in (7.4).
There is an analogous condition $\mathsf{Fill}_{1}(\alpha)$ in which $1$
replaces $0$ everywhere, describing $1$-directed filling from the other end of
the interval $\mathrm{I}$. Note that for $\alpha\colon\mathrm{I}\to U$, the
types $\mathsf{Fill}_{0}(\alpha)$ and $\mathsf{Fill}_{1}(\alpha)$ are
_closed_.

Now for any object $X$ and family of types $\alpha\colon X\to U$, we have the
family $x\colon X^{\mathrm{I}},i\colon\mathrm{I}\vdash\alpha\circ
x\colon\mathrm{I}\to U$ obtained by “restricting $\alpha$ along paths in $X$”,
i.e. composing $\alpha$ and $\mathsf{eval}\colon
X^{\mathrm{I}}\times\mathrm{I}\to X$. Thus we have the closed type

$\textstyle\mathsf{Fib}(\alpha)\ =_{\mathrm{def}}\
\prod_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\mathsf{Fill}_{0}(\alpha\circ{x})\times\mathsf{Fill}_{1}(\alpha\circ{x})\,.$
(8.9)

We show below that $\mathsf{Fib}(\alpha)$ is isomorphic to the type in item
(ii) of 8.5 and therefore also classifies uniform fibration structures on
$\sum_{x\mathord{\,:\,}X}\,\alpha(x)\to X$.

######  Proposition 8.6.

For any object $X$ and any $\alpha\colon X\to U$, there is an isomorphism,

$\textstyle\mathsf{Fib}(\alpha)\ \cong\
\prod_{x\mathord{\,:\,}X^{\mathrm{I}}}\,\Big{(}\prod_{a\mathord{\,:\,}\alpha(x_{0})}\,\mathsf{TFib}(F_{0}(x,a))\times\prod_{a\mathord{\,:\,}\alpha(x_{1})}\,\mathsf{TFib}(F_{1}(x,a))\Big{)}\,.$

  * Proof.

It clearly suffices to show

$\textstyle\mathsf{Fill}_{0}(\alpha\circ x)\ \cong\
\prod_{a\mathord{\,:\,}\alpha(x_{0})}\mathsf{TFib}(F_{0}(x,a))\,,$

in context $x\colon X^{\mathrm{I}}$, and similarly for $\mathsf{Fill}_{1}$.
Using (8.7), the type on the right becomes

$\textstyle\prod_{a\mathord{\,:\,}\alpha(x_{0})}\,\mathsf{TFib}\left(\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha(x_{i})}s_{0}=a\right)\,.$
(8.10)

Inserting the definition of $\mathsf{TFib}$ from (7.13) results in the type

$\textstyle\prod_{a\mathord{\,:\,}\alpha(x_{0})}\,\
\prod_{\varphi\mathord{\,:\,}\Phi}\,\
\prod_{v\mathord{\,:\,}{\\{\varphi\\}}\to\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha(x_{i})}s_{0}=a}\,\
\sum_{t\mathord{\,:\,}\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha(x_{i})}s_{0}=a}\,\
v=\lambda{t}\,,$ (8.11)

which simplifies to

$\textstyle\prod_{a\mathord{\,:\,}\alpha(x_{0})}\,\
\prod_{\varphi\mathord{\,:\,}\Phi}\,\
\prod_{v\mathord{\,:\,}\\{\varphi\\}\to\prod_{i\mathord{\,:\,}\mathrm{I}}\,\alpha(x_{i})}\,({\tilde{v}_{0}}=\lambda{a})\\\
\textstyle\to\
\sum_{s\mathord{\,:\,}\prod_{i\mathord{\,:\,}\mathrm{I}}\alpha(x_{i})}\,(s_{0}=a)\times(v=\lambda{s})\,.$
(8.12)

Comparing with (8.8), we see that this is indeed
$\mathsf{Fill}_{0}(\alpha\circ x)$. The case of $\mathsf{Fill}_{1}$ is
entirely analogous. ∎

It follows that the type $\mathsf{Fib}(\alpha)$ from (8.9) also classifies
uniform fibration structures on the type family $\alpha\colon X\to U$.

######  Corollary 8.7.

Let $\alpha\colon X\to U$. Then the following conditions are equivalent.

  1. (i)

The projection map $p\colon\sum_{x\mathord{\,:\,}X}\,\alpha(x)\to X$ is a
uniform fibration.

  2. (ii)

There is a term $t\mathord{\,:\,}\mathsf{Fib}(\alpha)$.

Moreover, there is a bijection between uniform fibration structures as in 8.2
and terms $t\mathord{\,:\,}\mathsf{Fib}(\alpha)$.

The construction of a universal uniform fibration given below (following [3,
17, 31]) requires the interval $\mathrm{I}$ to be _tiny_ , meaning that the
“path space” functor $X^{\mathrm{I}}$ has a right adjoint $X_{\mathrm{I}}$
called the $\mathrm{I}^{th}$-_root_. This is the case, for instance, when
$\tE=\mathrm{Psh}(\cC)$ is the category of cubical sets with $\cC$ the
Dedekind cube category [13] and $\mathrm{I}=\mathsf{y}{[1]}$ the 1-cube, which
then also satisfies the conditions in 8.1.

In order to use the approach of 7.10 to construct a universal fibration, we
need the analogue of 7.8 for $\mathsf{Fib}(\alpha)$, i.e. stability under
pullback. Unlike $\mathsf{TFib}(\alpha)$, however, the object
$\mathsf{Fib}(\alpha)$ is not indexed over $X$, but instead has the form

$\textstyle\mathsf{Fib}(\alpha)=\prod_{x\mathord{\,:\,}X^{I}}\,\mathsf{Fill}(\alpha\circ
x)\mathrlap{,}$ (8.13)

where $\mathsf{Fill}(\alpha\circ
x)=_{\mathrm{def}}\mathsf{Fill}_{0}(\alpha\circ
x)\times\mathsf{Fill}_{1}(\alpha\circ x)$. Now $\mathsf{Fill}(\alpha\circ x)$
is also not indexed over $X$, but rather over $X^{\mathrm{I}}$. However, we
can use it to construct a pullback stable family $\mathsf{Fib}^{*}(\alpha)$
over $X$ as follows (cf. [17, 31]). Applying the root functor to
$\mathsf{Fill}(\alpha\circ x)$, regarded as a display map over
$X^{\mathrm{I}}$, and pulling back along the unit of the adjunction,

${\mathsf{Fib}^{*}(\alpha)}$${\mathsf{Fill}(\alpha\circ
x)_{\mathrm{I}}}$${X}$${(X^{\mathrm{I}})_{\mathrm{I}}\mathrlap{,}}$${\lrcorner}$$\scriptstyle{\eta}$
(8.14)

we obtain a family $\mathsf{Fib}^{*}(\alpha)$ on $X$ that parametrises
fibration structures on $\alpha$, in the sense made precise in 8.8 below. It
may be noted that this construction of $\mathsf{Fib}^{*}(\alpha)$ is
categorical, rather than in the type theory of $\tE$ from Section 3. In fact,
such an internal construction is impossible, as is shown in [31], where a type
theoretic definition of $\mathsf{Fib}^{*}(\alpha)$ is obtained by extending of
the internal type theory of $\tE$ by a modal operator describing the comonad
$\Delta\circ\Gamma$ on $\tE$.

######  Proposition 8.8.

Let $\alpha\colon X\to U$.

  1. (i)

There is a natural bijection between sections of $\mathsf{Fib}^{*}(\alpha)$
over $X$ and global sections $1\to\mathsf{Fib}(\alpha)$.

  2. (ii)

The object $\mathsf{Fib}^{*}(\alpha)$ over $X$ is stable under pullback along
any map $t\colon Y\to X$, in the sense that the right hand square below is a
pullback whenever the left hand one is.

${Y.\alpha(t)}$${X.\alpha}$${Y}$${X\mathrlap{,}}$$\scriptstyle{t}$
${\mathsf{Fib}^{*}(\alpha(t))}$${\mathsf{Fib}^{*}(\alpha)}$${Y}$${X\mathrlap{.}}$$\scriptstyle{t}$

  * Proof.

For (i), by the specification (8.13), points $1\to\mathsf{Fib}(\alpha)$
correspond bijectively to sections of $\mathsf{Fill}(\alpha\circ x)$ over
$X^{\mathrm{I}}$. Let $\mathsf{fill}(\alpha)\colon X^{\mathrm{I}}\to U$
classify $\mathsf{Fill}(\alpha\circ x)\to X^{\mathrm{I}}$. We then have the
correspondence indicated below between maps $j_{1},j_{2},j_{3},j_{4}$,

${\mathsf{Fill}(\alpha\circ
x)}$${E}$${X^{\mathrm{I}}}$${U\mathrlap{,}}$$\scriptstyle{\mathsf{fill}(\alpha)}$$\scriptstyle{j_{1}}$$\scriptstyle{j_{2}}$
${X.\mathsf{fill}(\alpha)^{\sharp}}$${(E)_{\mathrm{I}}}$${X}$${U_{\mathrm{I}}\mathrlap{,}}$$\scriptstyle{\mathsf{fill}(\alpha)^{\sharp}}$$\scriptstyle{j_{4}}$$\scriptstyle{j_{3}}$

where $\mathsf{fill}(\alpha)^{\sharp}$ is the adjoint transpose of
$\mathsf{fill}(\alpha)$, and both squares are pullbacks.

It thus suffices to show that the following is also a pullback.

${\mathsf{Fib}^{*}(\alpha)}$${(E)_{\mathrm{I}}}$${X}$${U_{\mathrm{I}}\mathrlap{.}}$$\scriptstyle{\mathsf{fill}(\alpha)^{\sharp}}$

To see this, factor the transpose $\mathsf{fill}(\alpha)^{\sharp}$ as
$\mathsf{fill}(\alpha)_{\mathrm{I}}\circ\eta$, as indicated below, noting that
the root preserves pullbacks.

${\mathsf{Fib}^{*}(\alpha)}$${\mathsf{Fill}(\alpha\circ
x)_{\mathrm{I}}}$${{E}_{\mathrm{I}}}$${X}$${(X^{\mathrm{I}})_{\mathrm{I}}}$${U_{\mathrm{I}}}$$\scriptstyle{\eta}$$\scriptstyle{\mathsf{fill}(\alpha)^{\sharp}}$$\scriptstyle{\mathsf{fill}(\alpha)_{\mathrm{I}}}$

The square on the left is a pullback by the definition (8.14) of
$\mathsf{Fib}^{*}(\alpha)$.

For (ii), it now suffices to show that for every $t\colon Y\to X$,

$\mathsf{fill}(\alpha)^{\sharp}\circ
t=\mathsf{fill}({\alpha(t))}^{\sharp}\mathrlap{.}$ (8.15)

Since $\mathsf{fill}(\alpha)^{\sharp}\circ t=(\mathsf{fill}(\alpha)\circ
t^{\mathrm{I}})^{\sharp}$ by the naturality of transposition, it suffices to
show

$\mathsf{fill}(\alpha)\circ
t^{\mathrm{I}}=\mathsf{fill}(\alpha(t))\mathrlap{.}$ (8.16)

Now, by definition, $\mathsf{fill}(\alpha)\colon X^{\mathrm{I}}\to U$
classifies $\mathsf{Fill}(\alpha\circ x)=\mathsf{Fill}_{0}(\alpha\circ
x)\times\mathsf{Fill}_{1}(\alpha\circ x)$ (over $X^{\mathrm{I}}$), so we just
need to show that $\mathsf{Fill}_{0}(\alpha\circ x)\to X^{\mathrm{I}}$ is
stable under pullback along $t^{\mathrm{I}}\colon Y^{\mathrm{I}}\to
X^{\mathrm{I}}$ (the case $\mathsf{Fill}_{1}(\alpha\circ x)$ is analogous). As
shown in the proof of 8.6, over $X^{\mathrm{I}}$ we have

$\textstyle\mathsf{Fill}_{0}(\alpha\circ x)\ \cong\
\prod_{a\mathord{\,:\,}\alpha(x_{0})}\mathsf{TFib}(F_{0}(x,a))\mathrlap{.}$

Moreover, by the definition (8.7) the display map for $F_{0}(x,a)$, namely

$\textstyle\sum_{(x,a)\mathord{\,:\,}(\sum_{x\colon
X^{\mathrm{I}}}\,\alpha(x_{0}))}\,F_{0}(x,a)\ \overset{}{\longrightarrow}\
\sum_{x\colon X^{\mathrm{I}}}\,\alpha(x_{0})\,,$

is isomorphic to the pullback-hom ${\delta_{0}\Rightarrow{p_{\alpha}}}$ over
the isomorphism

$\textstyle\sum_{x\colon X^{\mathrm{I}}}\,\alpha(x_{0})\ \cong\
X^{\mathrm{I}}\times_{X}X.p_{\alpha}\,\mathrlap{.}$

Applying the functor ${\delta_{0}\Rightarrow{(-)}}$ to the pullback square on
the left below results in the upper one on the right:

${Y.\alpha(t)}$${X.\alpha}$${Y}$${X\mathrlap{,}}$$\scriptstyle{p_{\alpha}(t)}$${\lrcorner}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{t}$
${Y.\alpha(t)^{\mathrm{I}}}$${X.\alpha^{\mathrm{I}}}$${Y^{\mathrm{I}}\times_{Y}Y.p_{\alpha(t)}}$${X^{\mathrm{I}}\times_{X}X.p_{\alpha}}$${Y^{\mathrm{I}}}$${X^{\mathrm{I}}\mathrlap{.}}$$\scriptstyle{\delta_{0}\Rightarrow{p_{\alpha(t)}}}$${\lrcorner}$$\scriptstyle{\delta_{0}\Rightarrow{p_{\alpha}}}$${\lrcorner}$$\scriptstyle{t^{\mathrm{I}}}$

So we are done by the stability of $\mathsf{TFib}$ (7.8) and the Beck-
Chevalley condition for $\Pi$, using the lower pullback on the right. ∎

######  Theorem 8.9 (Universal fibration).

There is a universal small uniform fibration,
$\mathsf{Fib}_{\bullet}\to\mathsf{Fib}$, in the sense that every small
fibration $A\to X$ is a pullback of $\mathsf{Fib}_{\bullet}\to\mathsf{Fib}$
along a canonically determined classifying map $X\to\mathsf{Fib}$.

${A}$${\mathsf{Fib}_{\bullet}}$${X}$${\mathsf{Fib}}$${\lrcorner}$ (8.17)

  * Proof.

Define $\mathsf{Fib}=\mathsf{Fib}^{*}(\operatorname{id})$ and
$\mathsf{Fib}_{\bullet}\to\mathsf{Fib}$ by the pullback indicated below.

${\mathsf{Fib}_{\bullet}}$${E}$${\mathsf{Fib}}$${U}$${\lrcorner}$$\scriptstyle{\pi}$

The rest of the proof is the same as for 7.10. ∎

######  Remark 8.10.

As in 7.11, in terms of variables we have $\mathsf{Fib}=\sum_{\alpha\colon
U}\,\mathsf{Fib}^{*}(\alpha)$. Thus a uniform fibration is a small family
$\alpha\colon U$ equipped with a fibration structure
$f\colon\mathsf{Fib}^{*}(\alpha)$, and the universal one is indexed by the
type of all such pairs $(\alpha,f)$.

##  9\. Path types

The fundamental insight of Homotopy Type Theory [6, 18] is that identity terms
$p:\operatorname{Id}_{A}(a,b)$ in (intensional) Martin-Löf type theory [34]
behave like continuous paths $p\colon[0,1]\to A$ in a _space_ $A$, and the
identity type $\operatorname{Id}_{A}$ itself then acts like a _pathspace_
$A^{[0,1]}$. Moreover, the rules of the type theory then permit a formal
derivation of the _homotopy lifting property_ for type families $X\vdash A\
\mathsf{type}$, thus forcing them to be regarded as _fibrations_
$A\twoheadrightarrow X$.

To make this insight precise, for any object $A\in\tE$, define the _path
object_ $A^{\mathrm{I}}$ to be the exponential by the interval $\mathrm{I}$
(8.1). The path object is indexed over $A\times A$ by the pair of _endpoint
evaluations_ $\epsilon=(\epsilon_{0},\epsilon_{1})\colon
A^{\mathrm{I}}\overset{}{\longrightarrow}A\times A$, where
$\epsilon_{k}=A^{\delta_{k}}$ for $k=0,1$. Together with the _constant path_
map $\operatorname{\rho}=A^{!}\colon A\to A^{\mathrm{I}}$, where $!\colon A\to
1$, these maps make the following diagram commute.

${A}$${A^{\mathrm{I}}}$${A}$${A\times
A\mathrlap{.}}$$\scriptstyle{=}$$\scriptstyle{\operatorname{\rho}}$$\scriptstyle{\epsilon}$$\scriptstyle{\Delta_{A}}$
(9.1)

More generally, for $p\colon A\to X$ any (small) map, with classifying map
$\alpha\colon X\to U$, the path object of $p\cong p_{\alpha}$ in $\tE/_{X}$ is
the exponential of $p_{\alpha}$ by $\mathrm{I}_{X}=(\pi_{1}\colon
X\times\mathrm{I}\to X)$, which can be constructed in $\tE$ as the following
pullback along $\operatorname{\rho}_{X}\colon X\to X^{\mathrm{I}}$.

${X.\alpha^{\mathrm{I}}}$${(X.\alpha)^{\mathrm{I}}}$${X}$${X^{\mathrm{I}}\mathrlap{.}}$$\scriptstyle{p_{\alpha^{\mathrm{I}}}}$${\lrcorner}$$\scriptstyle{(p_{\alpha})^{\mathrm{I}}}$$\scriptstyle{\operatorname{\rho}_{X}}$

Let $\alpha^{\mathrm{I}}\colon X\to U$ classify $p_{\alpha^{\mathrm{I}}}\colon
X.\alpha^{\mathrm{I}}\to X$, so that in the type theory of $\tE$ we have the
_path type_ $X\vdash\alpha^{\mathrm{I}}\colon U$. Terms $X\vdash
u\colon\alpha^{\mathrm{I}}$ are called paths in $\alpha$. There are of course
maps over $X$ analogous to those in (9.1), of the form:

${X.\alpha}$${X.\alpha^{\mathrm{I}}}$${X.\alpha}$${X.\alpha\times
X.\alpha}$${X.(\alpha\times\alpha)\mathrlap{.}}$$\scriptstyle{=}$$\scriptstyle{\operatorname{\rho}_{\alpha}}$$\scriptstyle{\epsilon}$$\scriptstyle{\Delta_{\alpha}}$$\scriptstyle{\cong}$

Given any $x\colon\mathsf{y}{c}\to X$ and elements $c\Vdash
a,b\colon\alpha(x)$ (corresponding to sections of
$\mathsf{y}{c}.\alpha(x)\to\mathsf{y}{c}$), a path $c\Vdash
u\colon\alpha(x)^{\mathrm{I}}(a,b)$ thus represents a _homotopy_ $a\sim b$
(over $\mathsf{y}{c}$).

Regarding paths $a\sim b$ as “identifications” as in Homotopy Type Theory, the
path type $\alpha^{\mathrm{I}}$ acts as an _identity type_ for $\alpha$. Under
the propositions-as-types view, we should then expect a type family
$X.\alpha\vdash\beta\colon U$ to respect identifications $a\sim b$ in
$\alpha$, by the principle of “indistinguishability of identicals”: if $a\sim
b$ and $\beta(a)$, then $\beta(b)$, regarding $\beta\colon X.\alpha\to U$ as a
(type-valued) “propositional function” on $\alpha$. Indeed, we have the
following:

######  Lemma 9.1.

For any $X\in\tE$ and small map $A\to X$, let $B\to A$ be a small uniform
fibration. For the associated families of types $\alpha\colon X\to U$ and
$\beta\colon X.\alpha\to U$, and for any $x\colon\mathsf{y}{c}\to X$, suppose
we have terms $c\Vdash a,b\colon\alpha(x)$ and a path between them $c\Vdash
u\colon\alpha(x)^{\mathrm{I}}(a,b)$. Then for each $e$ with $c\Vdash
e\colon\beta(x,a)$ there is an associated $u*e$ with $c\Vdash
u*e\colon\beta(x,b)$.

  * Proof.

Consider the following diagram, in which $\lambda{u^{\prime}}=u$.

${\mathsf{y}{c}\times
1}$${X.\alpha.\beta}$${\mathsf{y}{c}\times\mathrm{I}}$${X.\alpha}$${\mathsf{y}{c}}$${X\mathrlap{.}}$$\scriptstyle{\mathsf{y}{c}\times\delta_{0}}$$\scriptstyle{(x,a,e)}$$\scriptstyle{p_{\beta}}$$\scriptstyle{u^{\prime}}$$\scriptstyle{j}$$\scriptstyle{x}$

The solid upper square commutes because
$u^{\prime}(\operatorname{id}\times\delta_{0})=(x,a)=p_{\beta}(x,a,e)\colon\mathsf{y}{c}\to
X.\alpha$, and by assumption $c\Vdash e\colon\beta(x,a)$. As the reader can
check, for the map on the left we have
$\mathsf{y}{c}\times\delta_{0}=0_{\mathsf{y}{c}}\otimes\delta_{0}$ with the
cofibration $0_{\mathsf{y}{c}}\colon 0\rightarrowtail\mathsf{y}{c}$, and thus
it is a (generating) trivial cofibration in the sense of 8.4. By assumption,
we have a uniform fibration structure $f\colon\mathsf{Fib}(\beta)$ over
$X.\alpha$, so by 8.7 we obtain a diagonal filler
$j=f(0_{\mathsf{y}{c}},\,(x,a,e),\,u^{\prime})$ as indicated. We can then take
$u*e=_{\mathrm{def}}\pi_{2}\,j(\mathsf{y}{c}\times\delta_{1})$, so that
$c\Vdash u*e\colon\beta(\pi_{1}\,j(\mathsf{y}{c}\times\delta_{1}))$. But

$\beta(\pi_{1}\,j(\mathsf{y}{c}\times\delta_{1}))=\beta(p_{\beta}\,j(\mathsf{y}{c}\times\delta_{1}))=\beta(u^{\prime}(\mathsf{y}{c}\times\delta_{1}))=\beta(x,b)\,.\qed$

The term $u*e$ is called the _transport_ of $e$ along $u$. It is in virtue of
this transport operation that fibrations are used as the type families in
Homotopy Type Theory, as we shall see in 9.4 . Of course, we then also need
the path type $\alpha^{\mathrm{I}}$ itself to be a fibration over
$\alpha\times\alpha$. Fortunately, we have the following result.

######  Lemma 9.2.

Let $X\in\tE$ and $\alpha\colon X\to U$. Given a uniform fibration structure
$f\colon\mathsf{Fib}(\alpha)$ over $X$, we can construct a uniform fibration
structure $f^{\prime}\colon\mathsf{Fib}(\alpha^{\mathrm{I}})$ over
$X.\alpha.\alpha\cong X.\alpha\times_{X}X.\alpha$.

  * Proof.

Consider a diagonal filling problem for the display map
$p_{\alpha^{\partial}}\colon X.\alpha^{\mathrm{I}}\to X.\alpha.\alpha$ with
respect to a generating trivial cofibration $m\otimes\delta_{k}$ with
cofibration $m\colon S\rightarrowtail\mathsf{y}{c}$ (see 8.4):

${\mathsf{y}{c}+_{S}(S\times\mathrm{I})}$${X.\alpha^{\mathrm{I}}}$${\mathsf{y}{c}\times\mathrm{I}}$${X.\alpha.\alpha\mathrlap{.}}$$\scriptstyle{u}$$\scriptstyle{m\otimes\delta_{k}\,}$$\scriptstyle{\,p_{\alpha^{\partial}}}$$\scriptstyle{v}$
(9.2)

In terms of the adjoint functors $\otimes$ and $\Rightarrow$, we have
$p_{\alpha^{\partial}}=(\partial\Rightarrow p_{\alpha})$, where
$\partial=[\delta_{0},\delta_{1}]\colon 1+1\rightarrowtail\mathrm{I}$, as the
reader can check. So by the adjoint relation (8.4), the above diagonal filling
problem can be reformulated equivalently as follows, where
$D=\operatorname{dom}((m\otimes\delta_{k})\otimes\partial)$.

${D}$${X.\alpha}$${(\mathsf{y}{c}\times\mathrm{I})\times\mathrm{I}}$${X\mathrlap{.}}$$\scriptstyle{u^{\prime}}$$\scriptstyle{(m\otimes\delta_{k})\otimes\partial\,}$$\scriptstyle{\,p_{\alpha}}$$\scriptstyle{v^{\prime}}$$\scriptstyle{j}$

Since $(m\otimes\delta_{k})\otimes\partial\cong(\partial\otimes
m)\otimes\delta_{k}$, and $\partial$ is a cofibration, and cofbrations are
closed under $\otimes$, the map on the left is a trivial cofibration. Thus
from the assumed fibration structure $f\colon\mathsf{Fib}(\alpha)$ we obtain a
diagonal filler $j=f(\partial\otimes m,u^{\prime},v^{\prime})$ as indicated.
Transposing $j\colon(\mathsf{y}{c}\times\mathrm{I})\times\mathrm{I}\to
X.\alpha$ to $j^{\prime}\colon\mathsf{y}{c}\times\mathrm{I}\to
X.\alpha^{\mathrm{I}}$ provides a diagonal filler for (9.2), which we may take
as the corresponding value of
$f^{\prime}\colon\mathsf{Fib}(\alpha^{\mathrm{I}})$,

$f^{\prime}(m,u,v)=_{\mathrm{def}}f(\partial\otimes
m,u^{\prime},v^{\prime})^{\prime}$

(up to the iso $(m\otimes\delta_{k})\otimes\partial\cong(\partial\otimes
m)\otimes\delta_{k}$). Uniformity of $f^{\prime}$ then follows from that of
$f$ and the naturality of adjoint transposition. ∎

Recalling 8.1, a consequence of the connection
$c_{0}\colon\mathrm{I}\times\mathrm{I}\to\mathrm{I}$ is the contractibility of
(the fibers of) the $0^{th}$-endpoint map $\epsilon_{0}\colon
X.\alpha^{\mathrm{I}}\overset{}{\longrightarrow}X.\alpha$ (and similarly for
$c_{1}$ and $\epsilon_{1}$).

######  Lemma 9.3.

Let $\alpha\colon X\to U$ with elements $c\Vdash a,b\colon\alpha(x)$. For any
path $u\colon a\sim b$ in $\alpha(x)$, there is a path
$\varepsilon_{u}\colon\operatorname{\rho}_{a}\sim u$ in the path type
$\alpha(x)^{\mathrm{I}}$. Formally, from $c\Vdash
u\colon\alpha(x)^{\mathrm{I}}(a,b)$, we can construct
$c\Vdash\varepsilon_{u}\colon(\alpha(x)^{\mathrm{I}})^{\mathrm{I}}(\operatorname{\rho}_{a},u)$.

  * Proof.

Over $X$, we of course have an iso
$X.(\alpha(x)^{\mathrm{I}})^{\mathrm{I}}\cong
X.\alpha(x)^{\mathrm{I}\times\mathrm{I}}$, and so we can use the connection
$c_{0}\colon\mathrm{I}\times\mathrm{I}\to\mathrm{I}$ to obtain a map over $X$
of the form

$\varepsilon\colon
X.\alpha(x)^{\mathrm{I}}\overset{}{\longrightarrow}X.\alpha(x)^{\mathrm{I}\times\mathrm{I}}\cong
X.(\alpha(x)^{\mathrm{I}})^{\mathrm{I}}\,.$

It follows from the connection diagrams in 8.1(iii) that $\varepsilon_{u}$
satifies the required forcing condition. ∎

Lemma 9.3 can be understood informally as follows: the fiber at
$a\colon\alpha$ of the endpoint map $\epsilon_{0}\colon
X.\alpha^{\mathrm{I}}\overset{}{\longrightarrow}X.\alpha$ may be regarded as a
“homotopy singleton”,

$\textstyle\mathsf{ho}{\\{a\\}}=\sum_{b\mathord{\,:\,}\alpha}\,a\sim b\,.$

The lemma says that, up to homotopy, the only element in
$\mathsf{ho}{\\{a\\}}$ is the constant path $\operatorname{\rho}_{a}\colon
a\sim~{}a$.

Using the previous three lemmas we can show that Martin-Löf’s rules [34] for
identity types $\operatorname{Id}_{\alpha}$ are satisfied by the path types
$\alpha^{\mathrm{I}}$, provided that we interpret types as (uniform)
fibrations (cf. [6]). In the following, we take $A\to 1$ rather than the
general case $A\to X$ merely for notational convenience, and use displayed
variables for a more familiar presentation. The judgement $\Gamma\vdash A\
\mathsf{type}$ will be interpreted to mean $\Gamma\vdash A\colon\mathsf{Fib}$,
where $\mathsf{Fib}=\sum_{\alpha\colon U}\,\mathsf{Fib}^{*}(\alpha)$ is the
base of the universal (small, uniform) fibration (8.10), and so we can write
$A\colon\mathsf{Fib}$ as a pair $A=(\alpha,f)$ with $\alpha\colon U$ and
$f\colon\mathsf{Fib}^{*}(\alpha)$.

######  Theorem 9.4.

Suppose the presheaf topos $\tE$ has a tiny interval $\mathrm{I}$ with
connections. Then in any context $\Gamma$, for any
$A=(\alpha,f)\colon\mathsf{Fib}$ with $\alpha\colon U$ and
$f\colon\mathsf{Fib}^{*}(\alpha)$, let
$A^{\mathrm{I}}=(\alpha^{\mathrm{I}},f^{\prime})\colon\mathsf{Fib}$ for
$\alpha^{\mathrm{I}}\colon U$ and
$f^{\prime}\colon\mathsf{Fib}^{*}(\alpha^{\mathrm{I}})$. The following
standard _formation_ , _introduction_ , and _elimination_ rules for identity
types then hold in the internal type theory of $\tE$.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
47.82097pt\hbox{$\displaystyle\penalty 1A\ \mathsf{type}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.30867pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
x\mathord{\,:\,}A,\,y\mathord{\,:\,}A\,\vdash\,A^{\mathrm{I}}(x,y)\
\mathsf{type}$}}}}\qquad\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 50.02647pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=100.05295pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle
x\mathord{\,:\,}A\,\vdash\,\operatorname{\rho}(x)\colon
A^{\mathrm{I}}(x,x)$}}}}$ ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1x\colon A,\,y\colon A,\,z\colon
A^{\mathrm{I}}(x,y)\,\vdash\,B(x,y,z)\ \mathsf{type}\qquad\qquad x\colon
A\,\vdash\,b(x)\colon B(x,x,\operatorname{\rho}(x))$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=336.84416pt\hbox{}}}\hbox{\kern
66.74382pt\hbox{$\displaystyle x\colon A,\,y\colon A,\,z\colon
A^{\mathrm{I}}(x,y)\,\vdash\,\mathsf{j}_{b}(x,y,z)\colon
B(x,y,z)\mathrlap{.}$}}}}$

If, moreover, the constant path map $\operatorname{\rho}\colon A\to
A^{\mathrm{I}}$ is a cofibration, then the following _computation_ rule also
holds.

$x\mathord{\,:\,}A\,\vdash\,\mathsf{j}_{b}(x,x,\operatorname{\rho}(x))=b(x)\colon
B(x,x,\operatorname{\rho}(x))$ (9.3)

  * Proof.

We follow the approach in [2, Section 2.4]. Reasoning first in an arbitrary
context, which we leave implicit, let $A=(\alpha,f)\colon\mathsf{Fib}$ with
$\alpha\colon U$ and $f\colon\mathsf{Fib}^{*}(\alpha)$. Then by Lemma 9.2 we
have $f^{\prime}\colon\mathsf{Fib}^{*}(\alpha^{\mathrm{I}})$, whence
$A^{\mathrm{I}}=(\alpha^{\mathrm{I}},f^{\prime})\colon\mathsf{Fib}$. Thus we
have the formation rule. The introduction rule follows from (9.1). The
underlying types those rules are displayed in the following two diagrams.

${1.\alpha.\alpha}$${1.\alpha}$${E}$${1.\alpha}$${1}$${U}$${\lrcorner}$$\scriptstyle{p_{\alpha}}$${\lrcorner}$$\scriptstyle{p_{\alpha}}$$\scriptstyle{\alpha}$
${1.\alpha}$${E}$${1.\alpha.\alpha}$${U}$$\scriptstyle{\operatorname{\rho}}$$\scriptstyle{\Delta}$$\scriptstyle{\alpha^{\mathrm{I}}}$
(9.4)

The premises of the elimination rule are then interpreted as the solid part of
the following, letting $B=(\beta,g)\colon\mathsf{Fib}$.

${1.\alpha.\alpha.\alpha^{\mathrm{I}}}$${E}$${1.\alpha.\alpha}$${U}$${\lrcorner}$$\scriptstyle{\alpha^{\mathrm{I}}}$
${1.\alpha}$${E}$${1.\alpha.\alpha.\alpha^{\mathrm{I}}}$${U}$$\scriptstyle{(\Delta,\operatorname{\rho})}$$\scriptstyle{b}$$\scriptstyle{j}$$\scriptstyle{\beta}$
(9.5)

The conclusion of elimination asserts the existence of the indicated diagonal
arrow $j$ making the _lower_ triangle commute, while the computation rule
states that the _upper_ one does. To build such a map $j$ it suffices to show
that for any $c$ and $x\colon\mathsf{y}{c}\to
1.\alpha.\alpha.\alpha^{\mathrm{I}}$, there is an element
$j_{x}\colon\mathsf{y}{c}\to E$ such that

$c\Vdash j_{x}\colon\beta(x)\,,$

uniformly in $c$. Since $x$ can be rewritten as
$(a,a^{\prime},u)\colon\mathsf{y}{c}\to 1.\alpha.\alpha.\alpha^{\mathrm{I}}$,
we have $c\Vdash u\colon\alpha^{\mathrm{I}}(a,a^{\prime})$. By Lemma 9.3 we
then obtain
$c\Vdash\varepsilon_{u}\colon(\alpha(x)^{\mathrm{I}})^{\mathrm{I}}(\operatorname{\rho}{(a)},u)$.
Substituting $a$ in the second premise of the elimination rule yields $c\Vdash
b(a)\colon\beta(a,a,\operatorname{\rho}(a))$. Transporting the latter along
$\varepsilon_{u}$ by Lemma 9.1 then provides
$c\Vdash\varepsilon_{u}*b(a)\colon\beta(a,a^{\prime},u)$. Now set

$j_{(a,a^{\prime},u)}=_{\mathrm{def}}\ \varepsilon_{u}*b(a)\,.$

Uniformity in $c$ follows from the same for each of the terms in the
construction of $j_{(a,a^{\prime},u)}$. Indeed, given $f\colon d\to c$, we
have

$d\Vdash
j_{(a,a^{\prime},u)}(f)=(\varepsilon_{u}*b(a))(f)=\varepsilon_{uf}*b(af)=j_{(af,a^{\prime}f,uf)}\colon\beta(af,a^{\prime}f,uf)\,.$
(9.6)

Finally, if $\operatorname{\rho}\colon A\to A^{\mathrm{I}}$ is a cofibration
then, looking at (9.5), the map $j$ can be (uniformly) replaced by a homotopic
one $j\sim j^{\prime}$ that _also_ makes the upper triangle commute, by a
standard argument using the fibration on the right. The new map $j^{\prime}$
then validates _both_ the elimination and computation rules.

Note that the required coherence conditions for $A^{\mathrm{I}}$ and $j$ with
respect to all context maps $Y\to X$ are ensured by the same device used for
$\Pi$ in (1.19); namely, we apply the above construction once in a universal
case constructed from the classifying type $E\to U$, and then obtain all of
the instances in a uniform way by composition. See [2, Section 2.4] for
details. ∎

######  Remark 9.5.

The condition that the constant path map $\operatorname{\rho}\colon A\to
A^{\mathrm{I}}$ is a cofibration holds, for instance, when _all_ monos are
taken as cofibrations, as in a Cisinski model structure. When this fails, as
it may for presheaves not valued in sets, one can still recover the
computation rule (9.3) by factoring $\operatorname{\rho}\colon A\to
A^{\mathrm{I}}$ into a cofibration followed by a (uniform) trivial fibration
(7.9), as shown in [46].

##  10\. Conclusions

We conclude the paper by outlining some directions for future work. First,
while here we considered $\mathop{\mathbf{Set}}$-valued presheaves, where
$\mathop{\mathbf{Set}}$ is the category of sets associated to ZFC extended
with an inaccessible cardinal, it is also interesting to consider presheaf
categories valued in other kinds of categories or categories of internal
presheaves in some topos. Such a project may also connect with the idea of
developing the material here in a constructive metatheory, as suggested to us
by Thierry Coquand and Michael Rathjen. Secondly, one could try to extend our
results to categories of sheaves. One preliminary issue for this is to find an
adequate counterpart of the Hofmann-Streicher universe and of the classifier
of small maps. One may also try to develop the material here without using a
universe, adopting the approach of [43] to replace quantification over the
universe. Finally, one may wish to consider extending the Kripke-Joyal forcing
introduced here to other forms of type theory, such as the modal type theory
studied in [31].

## References

  * [1] S. Awodey.  A cubical model of homotopy type theory.  Annals of Pure and Applied Logic, 169(12):1270–1294, 2018.
  * [2] S. Awodey.  Natural models of homotopy type theory.  Mathematical Structures in Computer Science, 28(2):241–286, 2018\.
  * [3] S. Awodey.  A Quillen model structure on the category of cartesian cubical sets, 21 October 2021.  Preprint available from https://github.com/awodey/math/blob/master/QMS/qms.pdf.
  * [4] S. Awodey and A. Bauer.  Propositions as [types].  Journal of Logic and Computation, 14(4):447–471, 2004.
  * [5] S. Awodey and F. Rabe.  Kripke semantics for Martin-Löf’s extensional type theory.  Logical Methods in Computer Science, 7(3):1–25, 2011.
  * [6] S. Awodey and M. A. Warren.  Homotopy theoretic models of identity types.  Mathematical Proceedings of the Cambridge Philosophical Society, 146:45–55, 2009.
  * [7] B. van den Berg and E. Faber.  Effective Kan fibrations in simplicial sets, 2020.  arXiv:2009.12670.
  * [8] B. van den Berg and R. Garner.  Topological and simplicial models of identity types.  ACM Transactions in Computational Logic, 13(1):1–44, 2012.
  * [9] M. Bezem, T. Coquand, and S. Huber.  A model of type theory in cubical sets.  In R. Matthes and A. Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107 – 128. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2015.
  * [10] A. Boileau and A. Joyal.  La logique des topos.  The Journal of Symbolic Logic, 45(1):6–16, 1981.
  * [11] J. Bourke and R. Garner.  Algebraic weak factorisation systems I: accessible AWFS.  Journal of Pure and Applied Algebra, 220:108–147, 2016.
  * [12] J. Bourke and R. Garner.  Algebraic weak factorisation systems II: categories of weak maps.  Journal of Pure and Applied Algebra, 220:148–174, 2016.
  * [13] U. Buchholtz and E. Morehouse.  Varieties of cubical sets.  In P. P. Höfner, D. Pous, and G. Struth, editors, Relational and Algebraic Methods in Computer Science, volume 10226 of Lecture Notes in Computer Science, pages 77–92. Springer, 2017.
  * [14] D.-C. Cisinski.  Les préfaisceaux comme modèles des types d’homotopie.  Astérisque, 308:xxiv+392, 2006.
  * [15] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg.  Cubical type theory: a constructive interpretation of the univalence axiom.  In T. Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018.
  * [16] T. Coquand.  A cubical type theory, 2015.  Slides of an invited lecture given at the Mathematical Foundations of Programming Semantics conference, Nijmegen. Available from https://www.cse.chalmers.se/~coquand/nijm1.pdf.
  * [17] T. Coquand.  Univalent type theory and modular formalization of mathematics, 2017.  Slides of a talk given at the Big Proof conference, Isaac Newton Institute, Cambridge. Available from https://www.newton.ac.uk/seminar/21728/.
  * [18] N. Gambino and R. Garner.  The identity type weak factorisation system.  Theoretical Computer Science, 409:94–109, 2008.
  * [19] N. Gambino and S. Henry.  Towards a constructive simplicial model of Univalent Foundations, 2019\.  arXiv:2009.12670. To appear in Journal of the London Mathematical Society.
  * [20] N. Gambino and J. Kock.  Polynomial functors and polynomial monads.  Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013.
  * [21] N. Gambino and M. F. Larrea.  Models of Martin-Löf type theory from algebraic weak factorisation systems.  Journal of Symbolic Logic, To appear.  https://arxiv.org/abs/1906.01491.
  * [22] N. Gambino and C. Sattler.  The Frobenius condition, right properness, and uniform fibrations.  Journal of Pure and Applied Algebra, 221(12):3027–3068, 2017.
  * [23] R. Garner.  Understanding the small object argument.  Applied Categorical Structures, 17(3):247–285, 2009.
  * [24] M. Grandis and W. Tholen.  Natural weak factorisation systems.  Archivum Mathematicum, 42:397–408, 2006.
  * [25] S. Henry.  A constructive account of the Kan-Quillen model structure and of Kan’s $\mathrm{Ex}^{\infty}$ functor, 2019.  ArXiv:1905.06160.
  * [26] M. Hofmann.  On the interpretation of type theory in locally cartesian closed categories.  In Computer Science Logic (CSL ’94), volume 933 of Lecture Notes in Computer Science, pages 427–441. Springer, 1994.
  * [27] M. Hofmann.  Syntax and semantics of dependent types.  In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 79–130. Cambridge University Press, 1997.
  * [28] M. Hofmann and T. Streicher.  Lifting Grothendieck universes.  Available from the second-named author’s web page, https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf, 1997\.
  * [29] P. T. Johnstone.  Sketches of an Elephant: A Topos Theory Compendium.  Oxford University Press, 2002.
  * [30] A. Joyal and I. Moerdijk.  Algebraic Set Theory.  London Mathematical Society Lecture Note Series. Cambridge University Press, 1995.
  * [31] D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters.  Internal universes in models of homotopy type theory.  In H. Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:17, 2018.
  * [32] S. Mac Lane and I. Moerdijk.  Sheaves in geometry and logic. A first introduction to topos theory.  Universitext. Springer-Verlag, 1994.
  * [33] M. E. Maietti.  Modular correspondence between dependent type theories and categories including pretopoi and topoi.  Mathematical Structures in Computer Science, 15:1089–1149, 2005\.
  * [34] B. Nordström, K. Petersson, and J. Smith.  Martin-Löf type theory.  In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 5, pages 1–37. Oxford University Press, 2001.
  * [35] I. Orton and A. M. Pitts.  Axioms for Modelling Cubical Type Theory in a Topos.  Logical Methods in Computer Science, 14(4):1–33, 2018.
  * [36] G. Osius.  A note on Kripke-Joyal semantics for the internal language of topoi.  In F.W. Lawvere, C. Maurer, and G.C. Wraith, editors, Model Theory and Topoi, volume 445 of Lecture Notes in Computer Science, pages 349–354. Springer, 1975.
  * [37] A. M. Pitts.  Categorical logic.  In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 5, pages 39–128. Oxford University Press, 2001.
  * [38] D. G. Quillen.  Homotopical algebra, volume 43 of Lecture Notes in Mathematics.  Springer, 1967.
  * [39] E. Riehl.  Categorical homotopy theory.  Cambridge University Press, 2014.
  * [40] G. Rosolini.  Continuity and Effectiveness in Topoi.  PhD thesis, University of Oxford, 1986.
  * [41] C. Sattler.  The equivalence extension property and model structures, 2017.  Available from ArXiv. http://arxiv.org/abs/1704.06911.
  * [42] R. A. G. Seely.  Local cartesian closed categories and type theory.  Mathematical Proceedings of the Cambridge Philosophical Society, 95:33–48, 1984.
  * [43] M. Shulman.  Stack semantics and the comparison of material and structural set theories, 2010.  ArXiv:1004.3802.
  * [44] M. Shulman.  All $(\infty,1)$-toposes have strict univalent universes, 2019.  arXiv.1904.07004.
  * [45] A. Swan.  An algebraic weak factorisation system on 01-substitution sets: a constructive proof.  Journal of Logic & Analysis, 8:1–35, 2016.
  * [46] A. Swan.  Identity types in algebraic model structures and cubical sets, 2018.  arXiv.1808.00915.
  * [47] A. Swan.  Some remarks on locally representable algebraic weak factorisation systems, 2021.  Talk at the International Category Theory Conference 2020-21.
  * [48] A. S. Troelstra and D. van Dalen.  Constructivism in Mathematics.  North-Holland, 1988.
  * [49] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [50] V. Voevodsky.  An experimental library of formalized mathematics based on the univalent foundations.  Mathematical Structures in Computer Science, 25(5):1278–1294, 2015\.