Proof. We first check that cofibrations are closed under retracts. Suppose that $n \colon C \to D$ is a retract of a monomorphism $m \colon A \to B$ , as illustrated below.

One can show that when $m$ is a monomorphism, the left hand square above is a pullback. It follows that if $m$ is a cofibration, then $n$ is a pullback of $m$ and so also a cofibration.

Now by the retract argument, if a map has the left lifting property against all trivial fibrations, then it is a retract of a cofibration, and so a cofibration.

Hence to prove the proposition, it suffices to show that every generating trivial cofibration is a cofibration. That is, for every cofibration $m \colon A \to B$ , and for $i = 0, 1$ , $\delta _i \hat {\times } m$ is a cofibration. However, the pushout product $\delta _i \hat {\times } m$ can be viewed as a union of cofibrations into $B \times {\mathbb{I}}$ , and we assumed that cofibrations are closed under finite union.

Proof. This easily follows from the fact that every object is cofibrant (Remark2).

Proof. See Frumin and van den Berg (Reference Frumin and van den Berg2019, Proposition 4.1)

Proof. See Frumin and van den Berg (Reference Frumin and van den Berg2019, Proposition 4.3).

Proof. See Frumin and van den Berg (Reference Frumin and van den Berg2019, Proposition 4.5).Footnote ²

Proof. Given an object $X$ , we factorise the map $X \to 1$ as a cofibration followed by a trivial fibration, to get $X \to X' \to 1$ , where the map $X \to X'$ is a cofibration, and in particular, a monomorphism and the map $X' \to 1$ is a trivial fibration, and so in particular a fibration.

Proof. This follows from the fact that path types, fibrations and trivial fibrations are closed under pullbacks.

Proof. Let $s \colon Y \to X$ be a section of $f$ and let $t \colon X \times _Y X \to P_Y X$ be a section of the map $P_Y X \to X \times _Y X$ . In particular, $f \circ s$ is trivially homotopic to $1_{Y}$ . The map $h := t \circ \langle 1_{X}, s \circ f \rangle$ is a homotopy from $1_{X}$ to $s \circ f$ over $Y$ .

Furthermore, we can use $h$ to exhibit $f$ as a retract of the trivial fibration $p_1^f \colon P_Y(X) \to X$ , which shows it is also a trivial fibration.

Proof. Without loss of generality say that $m_0$ is a cofibration.

First, observe that the result would be trivial if we knew that $t_0$ and $t_1$ agreed on $A_0 \cap A_1$ . We therefore aim to produce a new map $t_1'$ ensuring that $t_0$ and $t_1'$ agree on $A_0 \cap A_1$ .

If we pullback $f$ along $m_1$ , then the resulting map $m_1^\ast (f) \colon m_1^\ast (X) \to A_1$ is also an hproposition, and using $t_1$ , we can show it has a section. We deduce by Proposition15 that it is a trivial fibration. Furthermore, observe that the inclusion $\iota _1 \colon A_0 \cap A_1 \rightarrow A_1$ is a pullback of $m_0$ , and so a cofibration. We will define a lifting problem of $\iota _1$ against $m_1^\ast (f)$ . Let $\bar {t_0} \colon A_0 \cap A_1 \to m_1^\ast (X)$ be the pullback of $t_0$ along $m_1$ , so that if $\pi _0 \colon m_1^\ast (X) \to X$ is one of the projections in the pullback then $\pi _0 \circ \bar {t_0} = t_0 \circ \iota _0$ . Then, let $j$ be a diagonal filler in the following diagram.

We then define $t_1'$ to be $\pi _0 \circ j$ . One can then verify that $f \circ t_1' = m_1$ and $t_1' \circ \iota _1 = t_0 \circ \iota _0$ , and we can now easily define the required $t$ using the universal property of the union.

Proof. Note that $r^X$ is a split monomorphism in any case (with retraction $X^{\delta _0}$ ). It follows that 1 and 2 are equivalent.

Showing 2 and 3 are equivalent is straightforward.

Proof. 4 was already observed by Uemura (Reference Uemura, Dybjer, Santo and Pinto2019, Proposition 16). The rest are straightforward.

Proof. First, note that $\mathbb{I}$ is not necessarily fibrant, but we can embed it in a fibrant object $\tilde {\mathbb{I}}$ using Proposition13. Write $\iota$ for the inclusion ${\mathbb{I}} \to \tilde {\mathbb{I}}$ .

Since $\mathbb{I}$ is connected, $\mathbb{N}$ is fibrant by Proposition21. Since dependent products preserve fibrations, $\tilde {\mathbb{I}}^{\mathbb{N}}$ is also fibrant. Hence by the assumption that path types are identity types, $r^{\tilde {\mathbb{I}}^{\mathbb{N}}}$ is a cofibration. We will show that the map $1 \to 2^{\mathbb{N}}$ is a cofibration by exhibiting it as a pullback of $r^{\tilde {\mathbb{I}}^{\mathbb{N}}}$ .

We define the map $e \colon 2^{\mathbb{N}} \to (\tilde {\mathbb{I}}^{\mathbb{N}})^{\mathbb{I}}$ as below.

\begin{align*} e(\alpha )(i)(n) = \begin{cases} \iota (0) & \alpha (n) = 0 \\ \iota (i) & \alpha (n) = 1 \end{cases} \end{align*}

To check that $\lambda x.\lambda n.0$ is a pullback of $r^{\tilde {\mathbb{I}}^{\mathbb{N}}}$ along $e$ , it suffices to show, in the internal logic of $\mathbb{C}$ , that for all $\alpha \in 2^{\mathbb{N}}$ , $\alpha = \lambda n.0$ if and only if $e(\alpha )$ lies in the image of $r^{\tilde {\mathbb{I}}^{\mathbb{N}}}$ , which is the case if and only if $e(\alpha )$ is constant as a function ${\mathbb{I}} \to \tilde {\mathbb{I}}^{\mathbb{N}}$ .

It is easy to check that $e(\lambda n.0)$ is constant. Hence, we just show the converse, that if $e(\alpha )$ is constant then for all $n \in \mathbb{N}$ , $\alpha (n) = 0$ .

So suppose that $\alpha \in 2^{\mathbb{N}}$ and $e(\alpha )$ is constant. Let $n$ be an element of $\mathbb{N}$ . We know that $\alpha (n) = 0$ or $\alpha (n) = 1$ , so to show that $\alpha (n) = 0$ it suffices to show that $\alpha (n) \neq 1$ . Suppose that $\alpha (n) = 1$ . Since $e(\alpha )$ is constant, for all $i, i' \in {\mathbb{I}}$ we have $e(\alpha )(i)(n) = e(\alpha )(i')(n)$ , and so $\iota (i) = \iota (i')$ . In particular, applying this to the endpoints $0$ and $1$ , we have $\iota (0) = \iota (1)$ and so $0 = 1$ since $\iota$ is monic. But then we get a contradiction by the disjointness of the endpoints. We have now shown $\alpha (n) \neq 1$ , and so $\alpha (n) = 0$ . This applies for arbitrary $n$ , and so $\alpha = \lambda n.0$ .

Proof. Let $m \colon A \to B$ be any monomorphism. We need to show it is a cofibration.

Working in the internal logic of $\mathbb{C}$ , we define an equivalence relation on ${\mathbb{I}} \times B$ . Given $(i, b)$ and $(i', b')$ in ${\mathbb{I}} \times B$ , we set $(i, b) \sim (i', b')$ if $b = b'$ and either $i = i'$ or $m^{-1}(\{b\})$ is inhabited. It is straightforward to verify that this is an equivalence relation.

By Proposition13 there exists a fibrant object $X$ such that ${\mathbb{I}} \times B / {\sim }$ is a subobject of $X$ . Say $\iota \colon {\mathbb{I}} \times B / {\sim } \to X$ is the subobject inclusion.

We define $e \colon B \to X^{\mathbb{I}}$ to be the map that sends each $b \in B$ to $\lambda i.\iota ([(i, b)])$ .

Now, still reasoning internally in $\mathbb{C}$ , we show that for each $b \in B$ , $m^{-1}(\{b\})$ is inhabited if and only if $e(b)$ lies in the image of $r^X$ .

Suppose first that $m^{-1}(\{b\})$ is inhabited. Then for any $i, i' \in {\mathbb{I}}$ , we have $[(i, b)] = [(i', b)]$ . Hence, $e(b) = \lambda i.\iota ([(i, b)])$ is a constant function, and so lies in the image of $r^X$ .

Conversely, suppose that $e(b) = \lambda i.\iota ([(i, b)])$ lies in the image of $r^X$ . Then it is a constant function, and in particular, we have $\iota ([(0, b)]) = \iota ([(1, b)])$ , where $0$ and $1$ are the images of $\delta _0$ and $\delta _1$ , respectively. Since $\iota$ is monic, we deduce $[(0, b)] = [(1, b)]$ . Since quotients are exact, we now have $(0, b) \sim (1, b)$ , and so either $0 = 1$ , or $m^{-1}(\{b\})$ is inhabited. But we assumed the endpoints are disjoint and so we do have that $m^{-1}(\{b\})$ is inhabited as required.

Since $r^X$ is monic, we can now deduce that $e$ fits into a pullback diagram as below.

This witnesses $m$ as a pullback of the cofibration $r^X$ , and so $m$ is itself a cofibration, as required.

Proof. We first note that since $B$ is discrete, the subobject $A$ must be too. Since $m$ is a map between discrete objects it is a fibration by Proposition21. However, we still need to show that it is a small fibration. We first replace $A$ with the mapping path space, which we view as a small fibration $A' \to B$ . Explicitly, we can define $A'$ as a type internally in type theory with the following definition (where the equality is implemented using path types).

\begin{equation*} A'(b) := \Sigma _{a : A} m(a) = b \end{equation*}

This gives a well defined small fibration since $B$ and $A$ are small types, and universes are closed under path types. We now note that since $B$ is discrete, we in fact have an isomorphism $A' \cong A$ , and so $m$ is a small fibration as required.

Proof. We first construct the map $A_0 \cup A_1 \to \| A_0 + A_1 \|$ .

We clearly have maps $t_i$ for $i = 0,1$ in the following commutative diagram.

Since $\| A_0 + A_1 \|$ is an hproposition and each $m_i$ is a cofibration, we can apply Lemma 16 to get the required map $A_0 \cup A_1 \to \| A_0 + A_1 \|$ .

We next construct the map $\| A_0 + A_1 \| \to A_0 \cup A_1$ . Since $m \colon A_0 \cup A_1 \to B$ is a map between discrete objects, it is a fibration, albeit not necessarily small. Since it is a monomorphism and a fibration, it is an hproposition. Hence, we can obtain the required map as a filler in the following lifting problem.

Proof. Write $f : C \to B$ for the hproposition logically equivalent to $m$ and let $\gamma \colon B \to U$ be a classifying map for $f$ .

Since $U$ is univalent, the map $\pi _X \colon \Sigma _{X : U} \Sigma _{Y : U} \operatorname {Equiv}(X, Y) \to U$ is a trivial fibration. We will aim to define a lifting problem of $m$ against $\pi _X$ , as illustrated below.

(1)

We take the bottom map $B \to U$ to be $\gamma$ .

The next step is to construct the top map $\alpha$ of the lifting problem. This amounts to finding maps $\xi , \zeta \colon A \to U$ together with an equivalence $e$ over $A$ between $\xi ^{\ast }(\tilde {U})$ and $\zeta ^{\ast }(\tilde {U})$ . We are forced to take $\xi$ to be $\gamma \circ m$ for the lifting problem to be a commutative square.

We define $\zeta$ to be $u \circ !_{A}$ where we recall that $u : 1 \to U$ is the unit.

Now unfolding these values for $\xi$ and $\zeta$ , it remains to construct a homotopy equivalence between $m^{\ast }(C)$ and $A$ over $A$ . Using the map $A \to C$ over $B$ , $m^{\ast }(f)$ has a section just by the universal property of the pullback. It is an hproposition by Proposition14. Hence, it is a homotopy equivalence over $A$ by Proposition15.

So we do have a well defined map $\alpha \colon A \to \Sigma _{X : U} \Sigma _{Y : U} \operatorname {Equiv}(X, Y)$ such that $\pi _X \circ \alpha = \gamma$ and $\pi _Y \circ \alpha = u \circ !_{A}$ . Let $j$ be a diagonal filler as in (1). We will write $Y$ for the pullback of $\tilde {U}$ along $\pi _{Y} \circ j$ .

We now use all of this to show $m$ is pointwise $\neg \neg$ -stable. We recall that we are working in a category of presheaves over a category $\mathbb{E}$ and switch to the internal logic of $\mathbb{E}$ . Let $c$ be an object of $\mathcal{C}$ and let $b \in B(c)$ . Suppose that $m_c^{-1}(b)$ is not empty. We need to show that it is inhabited.

Note that if $m_c^{-1}(b)$ was inhabited, then the upper triangle in the lifting diagram would imply that $\pi _Y(j_c(b)) = u(c)$ . We can therefore deduce that $\pi _Y(j_c(b))$ is not not equal to $u(c)$ . However, we can now apply the fact that $U$ is pointwise $\neg \neg$ -separated to show that in fact $\pi _Y(j_c(b))$ is equal to $u(c)$ . Furthermore, for all $\sigma \colon c' \to c$ in $\mathcal{C}$ , we have that $m_{c'}^{-1}(B(\sigma )(b))$ is not empty, and so we similarly can show that $\pi _Y(j_{c'}(B(\sigma )(b)))$ is equal to $u_{c'}(B(\sigma )(b))$ . Therefore, if $\bar {b} \colon \mathbf{y} c \to B$ is the map corresponding to $b$ under Yoneda, then the composition $\pi _Y \circ j \circ \bar {b}$ factors through the unit type $u \colon 1 \to U$ . Hence, the pullback of $Y$ along $\bar {b}$ is an isomorphism. Furthermore, we can pullback the equivalence to obtain an equivalence between $\bar {b}^\ast (Y)$ and $\bar {b}^\ast (C)$ . We deduce that $\bar {b}^\ast (C)$ has a section. This gives us an element of $C(c)$ in the fibre of $b$ .

Finally, applying the map $C \to A$ from the logical equivalence gives us an element of $A (c)$ in the fibre of $b$ as required.

Proof. By extensionality, there is a unique empty set, which we denote $\emptyset$ as usual. We take $z$ to be the small set $\{\emptyset \}$ (which is the usual implementation of the terminal object in $\mathbf{Set}$ anyway). Suppose that $x$ is a (small) set and that the double negation of $x = z$ holds. Now let $y$ be any element of $x$ . Suppose that $y$ contains an element $w$ . Then $y \neq \emptyset$ , and so $y \notin z$ . Hence, $x \neq z$ , contradicting the double negation of $x = z$ . But we have now shown that every element $y$ of $x$ is empty, and so $x$ is a subset of $\{\emptyset \}$ . We can now deduce that $x$ has at most one element, as required.

Proof. Since $V_\kappa (\mathcal{A})$ is a model of set theory, we can carry out exactly the same argument as in Lemma 36 internally in the model. Since the definition of the equality relation for the universe in the topos is defined the same as in McCarty’s model of set theory, it follows that we do get a weakly $\neg \neg$ -stable unit in the topos.

Proof. Suppose that $u \colon 1 \to V$ is a weakly $\neg \neg$ -stable unit in $V$ . First note that $V_{\mathcal{C}}$ has a pointwise weakly $\neg \neg$ -stable unit $u' \colon 1 \to V_{\mathcal{C}}$ defined as follows. In the internal logic of $\mathcal{E}$ , we need to define a map $1 \to V_{\mathcal{C}}(c)$ for each object $c$ of $\mathcal{C}$ . An element of $V_{\mathcal{C}}(c)$ consists first of a map $\Sigma _{d \in \mathcal{C}} \hom (d, c) \to V$ . We define each such map to be constantly equal to $u$ . We take the action on morphisms to be the identity everywhere.

Next, note that the identity on $1$ is an isomorphism and so a fibration, and so $u'$ does factor through $i \colon U \to V_{\mathcal{C}}$ to give a map $u'' \colon 1 \to U$ .

We finally need to check that $u''$ is pointwise weakly $\neg \neg$ -stable. That is, we need to show, in the internal logic of $\mathbb{E}$ , that for all $c \in \mathcal{C}$ and every $x \in U(c)$ , if $\neg \neg x = u''(c)$ then $\mathrm{El}(x)$ has at most one element. First, note that if $\neg \neg x = u''(c)$ , then also $\neg \neg i(x) = u'(c)$ . It follows that for every $d \in \mathcal{C}$ , and every $f \colon d \to c$ , we have $\neg \neg i(x)(d, f) = u$ . In particular, we have $\neg \neg i(x)(c, 1_c) = u$ . Hence, $\mathrm{El}(i(x)(c, 1_c))$ has at most one element. But this is precisely the definition of $\mathrm{El}(i(x))(c)$ .

Proof. Let $m : A \to B$ be a cofibration with a contractibility representation witnessed by a $U$ -small fibration $g \colon D \to B$ with a section $d_{0} \colon B \to D$ such that $A$ is logically equivalent to $\operatorname {IsContr}(D)$ over $B$ . Let $\beta \colon B \to U$ be a classifying map for $g$ .

As in the proof of Lemma 34, we define a map $\alpha \colon A \to \Sigma _{X : U} \Sigma _{Y : U} \operatorname {Equiv}(X, Y)$ that we will use along with $\beta$ to define a lifting problem.

Given $a \in A$ , we need to define small types $X(a)$ and $Y(a)$ , together with an equivalence $e$ between them. As before, we are forced to take $X(a)$ to be $\beta (m(a))$ in order for the square to commute. We take $Y(a)$ to be the pointwise weakly $\neg \neg$ -stable unit.

To complete the upper horizontal map in our lifting problem, we now need to construct an equivalence between $m^\ast (D)$ and the unit type over $A$ . Using the logical equivalence between $A$ and $\operatorname {IsContr}(D)$ , pulled back along $m$ , we have a section of $\operatorname {IsContr}(m^{\ast }(D)) \to A$ and so $m^{\ast }(D)$ is contractible over $A$ . Since any two contractible types are equivalent we deduce that $m^{\ast }(D)$ is equivalent to the unit type over $A$ .

Now since $m$ is a cofibration by assumption, we have a diagonal filler $j$ in the diagram below.

(2)

We take $y \colon B \to U$ to be the composition of $j$ with the projection to the $Y$ component. We will write $Y$ for the pullback of $\mathrm{El}$ along $y$ .

We now recall that we are working in a category of internal presheaves and switch to the internal logic of $\mathbb{E}$ . Let $c$ be an object of $\mathcal{C}$ and let $b \in B(c)$ . We will deduce that $m_c^{-1}(\{b\})$ is inhabited from its double negation. As before, note that if $m_c^{-1}(\{b\})$ is inhabited, then the upper triangle of (2) implies that $y_c(b)$ is equal to $u(c)$ for all $c \in \mathcal{C}$ . Hence, if $m^{-1}(\{b\})$ is not not inhabited, then $y_c(b)$ is not not equal to $u(c)$ . Since $u(c)$ is weakly $\neg \neg$ -stable, we deduce that if $m_c^{-1}(\{b\})$ is not not inhabited then $Y(c, b)$ has at most one element for every $c \in \mathcal{C}$ . Hence, by the same argument as in Lemma 34 the pullback of $Y$ along the map $\bar {b} \colon \mathbf{y} c \to B$ is an hproposition. Since the pullback of $D$ along $\bar {b}$ is equivalent to the pullback of $Y$ over $\mathbf{y} c$ , it is also an hproposition. By pulling back $d_{0}$ , $\bar {b}^{\ast }(D)$ has a section. Putting these together give us a section of $\bar {b}^{\ast }(\operatorname {IsContr}(D))$ and so a section of the logically equivalent $\bar {b}^{\ast }(A)$ , witnessing that $m_c^{-1}(\{b\})$ is inhabited.

Proof. We aim to apply Lemmas 23 and 34.

We define $B$ to consist of those $\alpha (n)$ in $2^{\mathbb{N}}$ such that $\alpha (n) = 1$ at most once. Note that $\Delta$ preserves exponentials, limits, colimits and the natural number object. Hence, $\Delta B$ is also a subobject of $2^{\mathbb{N}}$ in $\mathbb{C}$ and so discrete.

We define two subobjects $A_0$ and $A_1$ of $B$ as below.

\begin{align*} A_0 &:= \{ \alpha \in B \;|\; \forall n \in \mathbb{N},\, \alpha (2n) = 0 \} \\ A_1 &:= \{ \alpha \in B \;|\; \forall n \in \mathbb{N},\, \alpha (2n + 1) = 0 \} \end{align*}

Observe that $\Delta (A_0)$ and $\Delta (A_1)$ can both be written as pullbacks of the constant map $1 \to 2^{\mathbb{N}}$ , which is a cofibration by Lemma 23, and so the inclusions are both cofibrations.

We check that $\Delta (B)$ , $\Delta (A_0)$ and $\Delta (A_1)$ are small. Since small maps are closed under dependent products, composition and path types, we can implement the types below as small fibrant objects, where equality is interpreted using path types.

\begin{align*} B' &:= \Sigma _{\alpha : 2^{\mathbb{N}}} \, \Pi _{n, m : \mathbb{N}}\, \alpha (n) = 1 \,\times \, \alpha (m) = 1 \;\to \; n = m \\ A_0' &:= \Sigma _{\alpha : B'} \, \Pi _{n : \mathbb{N}} \, \alpha (2n) = 0 \\ A_1' &:= \Sigma _{\alpha : B'} \, \Pi _{n : \mathbb{N}} \, \alpha (2n + 1) = 0 \end{align*}

Since all objects involved are discrete, the same definition applies whether we interpret these types ‘extensionally’ (i.e. using the internal language of $\mathbb{C}$ in the usual way) or ‘intensionally’ (i.e. using the homotopical structure, and in particular path types for the equalities). Furthermore, as we observed earlier $\Delta$ preserves limits, exponentials and the natural number object, and so we see that $\Delta (B)$ , $\Delta (A_0)$ and $\Delta (A_1)$ are respectively isomorphic to $B'$ , $A_0'$ and $A_1'$ , and therefore small.

We define $A$ to be the union of $A_0$ and $A_1$ , with $m$ the inclusion $A \hookrightarrow B$ . Since $\Delta$ preserves unions and cofibrations are closed under unions, $\Delta (m)$ is a cofibration. Furthermore, by Lemma 33 $\Delta (A)$ is logically equivalent to $\| \Delta (A_{0}) + \Delta (A_{1}) \|$ , which is $U$ -small by the assumption that $U$ is closed under propositional truncation.

We can therefore apply Lemma 34 to show that $m$ is $\neg \neg$ -stable. However one can check that $A$ is $\neg \neg$ -dense in $B$ , and that $\mathbf{LLPO}$ precisely states that every element of $B$ belongs to $A$ . It follows that $\mathbf{LLPO}$ holds in $\mathbb{E}$ .

Proof. It is well known that in categories of assemblies every object is $\neg \neg$ -separated, as long as we assume excluded middle in the meta theory (see e.g. van Oosten (Reference van Oosten2008, Section 3.1) or Streicher (Reference Streicher2018)). Hence, any object in a category of internal presheaves over assemblies is pointwise $\neg \neg$ -separated. In particular this applies to any universe. It is also well known that $\mathbf{LLPO}$ fails in assemblies over $\mathcal{K}_1$ and over $\mathcal{K}_2$ . For example, Richman (Reference Richman1990, Theorem 5) proved that in the presence of countable choice a weak form of $\mathbf{LLPO}$ is not consistent with Church’s thesis. However, both Church’s thesis and countable choice hold in assemblies. A similar argument applies in function realisability (i.e. realisability over $\mathcal{K}_2$ ) by getting a contradiction from continuous choice rather than Church’s thesis; see for example the proof of Rathjen and Swan (Reference Rathjen and Swan2020, Corollary 7.23).

We apply Lemma 47.

Proof. By Lemma 36, any inaccessible set $V$ has a weakly $\neg \neg$ -stable unit. We deduce by Lemma 42 that any homotopical universe on $V$ has a pointwise weakly $\neg \neg$ -stable unit. Now if $m$ is the inclusion of a subobject of $\{0\}$ then it is a map between two small sets $m \colon A \hookrightarrow B$ with $A \subseteq \{0\}$ and $B = \{0\}$ . Since the interval is representable, $\Delta (A)$ and $\Delta (B)$ are both discrete and so fibrant. By Theorem24, $\Delta (m)$ is a cofibration. Since $A$ and $B$ are small sets, it follows that $\Delta (A)$ and $\Delta (B)$ are $U$ -small. Hence, $m$ is a small hproposition by Proposition32. Hence, it has a contractibility representation. Hence, $\Delta (m)$ is pointwise $\neg \neg$ -stable by Lemma 45, and so $m$ is $\neg \neg$ -stable.

We have shown that arbitrary subsets of $\{0\}$ are $\neg \neg$ -stable, and so deduce the law of excluded middle.

Proof. We need to show that $\top \colon 1 \to 2$ is not a subobject classifier, so it suffices to find a monomorphism that is not a pullback of $1 \to 2$ . We take this monomorphism to be the canonical map $2 \to \nabla 2$ .

Since $\mathcal{A}$ is non-trivial we have $\underline {0} \neq \underline {1}$ , by a similar proof to van Oosten (Reference van Oosten2008, Proposition 1.3.1, part iii). Therefore, all maps from $\nabla 2$ to $2$ are constant, and clearly, the map $2 \to \nabla 2$ is not the pullback along either of the constant maps.

Proof. By Lemma 37, any McCarty universe $\mathbf{Mc}(\mathcal{A})$ has a weakly $\neg \neg$ -stable unit. Hence, any homotopical Hofmann-Streicher universe on $\mathbf{Mc}(\mathcal{A})$ has a pointwise weakly $\neg \neg$ -stable unit by Lemma 42.

Suppose we are given a monomorphism $m \colon A \rightarrowtail B$ in $\mathbf{RT}(\mathcal{A})$ where $A$ and $B$ are $\mathbf{Mc}(\mathcal{A})$ -small. Since the interval is representable, $\Delta (A)$ and $\Delta (B)$ are discrete and so $U$ -small. By Theorem24 $\Delta (m)$ is a cofibration, and so a $U$ -small hproposition by Proposition32. We deduce by Lemma 45 that any such $m$ is $\neg \neg$ -stable.

However, we can show directly from the definition of McCarty universe that $\Omega$ is $\mathbf{Mc}(\mathcal{A})$ -small using the corresponding assumption on the inaccessible used to construct it. Hence, the subobject classifier $1 \to \Omega$ is $\neg \neg$ -stable, showing that the law of excluded middle holds in $\mathbf{RT}(\mathcal{A})$ , contradicting Lemma 50.

Proof. Note that any map $1 \to 2^{\mathbb{N}}$ can be viewed as a pullback of an endpoint inclusion $1 \to \nabla 2$ using classical logic in the metatheory, and so it is a cofibration. Furthermore, one can show directly that $\nabla 2$ is connected.

Given a $\neg \neg$ -separated universe, we use the same argument as in Theorem48.

Given instead a McCarty universe, we replace the use of Lemma 34 with Lemma 45 using the contractibility representation of the monomorphisms $A \hookrightarrow B$ appearing in Lemma 47 and using Lemma 37 for the weakly $\neg \neg$ -stable unit.

Proof. We first show that the map $1 \to 2^{\mathbb{N}}$ defined to be constantly $\lambda n.0$ can be viewed as a pullback of the endpoint inclusion $\delta _0 \colon 1 \to [0, 1]$ . We define a continuous map $h \colon 2^{\mathbb{N}} \to [0, 1]$ by taking $h(\alpha )$ to be $\Sigma _{n = 0}^\infty \,2^{-\alpha (n)}$ . This is evidently computable, and so does define a map in $\mathcal{KV}$ , and it is straightforward to check that $\lambda n.0$ is the pullback of $\delta _0$ along $h$ . It follows that any such map is a cofibration.

We then use the same argument as in Theorem52 together with the observation that $\mathbf{LLPO}$ fails in $\mathcal{KV}$ .

Proof. This follows from the uniqueness condition in the definition of canonical.

Proof. Write $C$ for the type $\|\Sigma _{x : A} m = y \|$ . Then, we have the valid judgement $y : B \vdash C(y) : U$ . Note that if we reindex along $m$ , we get the type $x : A \vdash C[y/m] : U$ . In any case, $C$ is an hproposition, and in context $x : A$ we can clearly construct an inhabitant $| (x, \mathtt {refl}_{m}) |$ of $C[y/m]$ . Hence, in context $x : A$ , $C[y/m]$ is contractible and so we can construct a term witnessing that $C[y/m]$ is equivalent to the unit type $1 : U$ . We take the component witnessing the map $1 \to C[y/m]$ to be $\lambda z.(x, \mathtt {refl}_{m})$ . We omit writing out the other components of the equivalence.

Since $m$ is a cofibration by assumption, we can deduce by univalence that there is a type $D$ with $\Gamma , y : B \vdash D : U$ together with a term witnessing that $D$ is equivalent to $C$ in context $\Gamma , y : B$ . Explicitly, we use a diagonal filler in the lifting problem below.

We take $r$ to be the component of the equivalence witnessing the map $D \to C$ and drop the other parts of the equivalence. The required definitional equalities then follow from the upper triangle of the diagram.

Proof. Suppose we are given a map $\tau \colon \Xi \to \Gamma .B$ . Note that we can split up $\tau$ as $(\sigma , b)$ where $\sigma \colon \Xi \to \Gamma$ and $\Xi \vdash b : B[\sigma ]$ .

Let $r$ be as in the statement of Lemma 56. We first use decidable type checking to decide whether the following judgement is valid.

\begin{equation*} \Xi \vdash r[\sigma ][y/b][d/\ast ] : \| \Sigma _{x : A} m[\sigma ] = b \| \end{equation*}

If it is not valid we say there is no such term $a$ satisfying the condition. If it is valid, we continue.

Now using the assumption that the truncation map is canonical, we can effectively decide whether or not there exists a term $c$ satisfying the following.

\begin{align*} \Xi &\vdash c : \Sigma _{x : A} m[\sigma ] = b \\ \Xi &\vdash r[\sigma ][y/b][d/\ast ] \equiv |c| \end{align*}

If the check returns false we say there is no such term $a$ satisfying the condition. If it is valid, then we can effectively find such a term $c$ , and we continue.

We next use type checking to decide if the following judgement is valid.

\begin{equation*} \Xi \vdash c \equiv (\pi _0 c, \mathtt {refl}_{m[\sigma ][x/\pi _0 c]}) \end{equation*}

If so, then we have found a suitable term taking $a := \pi _0 c$ , otherwise we say there is no such term.

We now need to show that the term $a$ is unique and that if any of the three checks above returns false then there really is no such term $a$ . It suffices for both to show that if $a$ is any such term then all the checks above return true, and that for any such term $c$ we have $\Xi \vdash a \equiv \pi _0 c$ . So, let $a$ be any term such that $\Xi \vdash a : A$ and $\Xi \vdash m[\sigma ][x/a] \equiv b$ .

Substituting $a$ for $x$ in the two judgements given by Lemma 56 gives the following.

\begin{align*} \Xi &\vdash D[\sigma ][y/b] \equiv 1 \\ \Xi &\vdash r[\sigma ][y/b][d/\ast ] \equiv |(a, \mathtt {refl}_{b})| \end{align*}

The first judgement implies that $\ast$ is a term of type $D[\sigma ][y/b]$ , which implies that the first type check succeeds. The second judgement implies that the second check succeeds with $c := (a, \mathtt {refl}_{b})$ and that moreover any such $c$ is of this form up to definitional equality.

Proof. Since $m$ is an embedding, by definition the type $\Sigma _{x : A}\,m = y$ is an hproposition in context $\Gamma , y : B$ . It easily follows that the truncation map $\Gamma .B.\Sigma _{x : A}\,m = y \to \Gamma .B.\|\Sigma _{x : A}\,m = y\|$ has a retraction and hence is canonical. We can now apply Lemma 57.

Proof. This is a special case of Lemma 57 where we take $\Gamma$ to be empty.