September 29, 2022
We give a construction of classifiers for double negation stable h-propositions in a variety of cubical set models of homotopy type theory and cubical type theory. This is used to give some relative consistency results: classifiers for double negation stable propositions exist in cubical sets whenever they exist in the metatheory; the Dedekind real numbers can be added to homotopy type theory without changing the consistency strength; we construct a model of homotopy type theory with extended Church’s thesis, which states that all partial functions with double negation stable domain are computable.
In approaches to the semantics of homotopy type theory (HoTT) based on model structures, such as simplicial sets [1] and cubical sets [2]–[5], we have categories that can be regarded as models of type theory in two different ways. Simplicial sets and cubical sets are toposes and as such can be viewed as models for extensional type theory. They also have notions of Kan fibration and homotopy that are combined with the topos structure to produce models of HoTT. In particular there are two different definitions of families of propositions in a given context, depending on whether we interpret equality according to the locally cartesian closed structure, or using homotopy as in [6]. A fibration between fibrant objects, \(f : X \to Y\), is a proposition in context \(Y\) according to the underlying topos structure when it is a monomorphism, which equivalently says the diagonal map \(X \to X \times_Y X\) has a section. It is a proposition from the perspective of homotopy when the map \(\operatorname{Path}_Y(X) \to X \times_Y X\) has a section, where \(\operatorname{Path}_Y(X)\) is the type of paths in \(X\) over \(Y\), defined as the following pullback. \[\begin{tikzcd} \operatorname{Path}_Y(X) \ar[d] \ar[r] & X^\mathbb{I}\ar[d] \\ Y \ar[r] & Y^\mathbb{I} \end{tikzcd}\] To avoid confusion with monomorphisms, we will refer to the latter as homotopy propositions or just h-propositions.
In simplicial sets in a classical setting, where we have the law of excluded middle and axiom of choice, there is a tight correspondence between the two definitions. Every h-proposition is equivalent to a pullback of the coproduct inclusion \(1 \to 1 + 1\) and in particular must be equivalent to a monomorphism (see e.g. [7] or [8]). On the other hand, in a constructive setting h-propositions can in general behave quite differently to monomorphisms (see e.g. [9] or [10]). In this paper we will consider a restricted class of h-propositions: those which are stable under double negation, which we refer to as \(\neg \neg\)-stable h-propositions. For this restricted class we can recover some of the good behaviour of h-propositions in a classical setting, and in particular construct classifying objects giving us a restricted form of resizing. We will show \(\neg \neg\)-stable h-propositions suffice to construct the Dedekind real numbers and to formulate and prove consistency of an extended version of Church’s thesis for partial functions \(\mathbb{N}\rightharpoondown \mathbb{N}\).
We recall some basic definitions and theorems about cubical sets. Although there are a few variations on the definition of cubical sets [3]–[5], for this paper we will only use a few properties that hold for several of the different definitions. Throughout we assume we are working in a metatheory of extensional type theory with propositional truncation, i.e. the internal language of a regular locally cartesian closed category [11], [12].
Firstly, we assume that we are given a category \(\square\) which is a Lawvere theory, i.e. \(\square\) has finite products, and an object \(I\) such that any object is an \(n\)-fold product of \(I\) for some \(n \in \mathbb{N}\). We write \(I^n\) as \([n]\). In particular \([0]\) is the terminal object of \(\square\). We refer to \(\square\) as the category of cubes.
We refer to the presheaf category \(\widehat{\square}\) as the category of cubical sets. For a cubical set, \(X\), we write the set at an object \([n]\) as \(X_n\), and for \(s : [n] \to [m]\) we write \(X_s\) for the function \(X_m \to X_n\).
Cubical sets can be used to model homotopy type theory. Maps \(X \to Y\) in \(\widehat{\square}\) may possess a kind of structure known as Kan fibration structure, and types in homotopy type theory are interpreted as maps in \(\widehat{\square}\) together with Kan fibration structure. We refer to a pair consisting of a map \(f : X \to Y\) and a Kan fibration structure on \(f\) as a Kan fibration, or just fibration. A fibrant object is an object \(X\) together with a Kan fibration \(X \to 1\).
Definition 1. We say a map \(m : A \to B\) is a trivial cofibration if we can choose a diagonal filler for each lifting problem of \(m\) against a fibration \(f : X \to Y\). That is, given a commutative square as in the solid lines in the diagram below, we have a choice of map \(j : B \to X\) making two commutative triangles, as in the dotted line below. \[\begin{tikzcd} A \ar[r] \ar[d, "m"] & X \ar[d, "f"] \\ B \ar[r] \ar[ur, dotted, "j" description] & Y \end{tikzcd}\]
We will use the following facts about Kan fibrations and the interpretation of homotopy type theory in cubical sets:
Contexts are interpreted as objects \(Y\), types in context \(Y\) are interpreted as Kan fibrations \(X \to Y\) and terms of a type \(f : X \to Y\) are interpreted as sections of \(f\). The empty context is interpreted as the terminal object.
Fibrations are preserved by pullback along any map, and this is used to interpret substitution in HoTT.
The natural number object and initial object are fibrant and they are the underlying objects of the interpretations of the natural number type and empty type in the interpretation of HoTT.
Kan fibrations are closed under composition and composition is used to interpret \(\Sigma\) types in the model of HoTT.
Kan fibrations are closed under dependent product and dependent products are used to interpret \(\Pi\) types in the model of HoTT.
\(I\) has at least one global section, say \(\delta : 1 \to I\).
For every object \(A\) and every map \(d : 1 \to \mathbf{y}I\) the map \(d \times A : A \to \mathbf{y}I \times A\) is a trivial cofibration. “Kan fibrations are in particular Hurewicz fibrations.”
Cubical sets admit propositional truncation operators \(\| - \|_Y : \widehat{\square}/Y \to \widehat{\square}/Y\) which are preserved by reindexing and used to interpret propositional truncation in HoTT. (See e.g. [4], [13], [14])
Any map between constant cubical sets is a fibration.
Proposition 2. Every object of \(\square\) admits a global section.
Proof. We show this for all objects \(n\) of \(\square\) by induction on \(n\). For \(n = 0\) \([n]\) is the terminal object, so we can use the identity map. For any \(n\), \([n + 1] \cong [n] \times [1]\), and so we have e.g. \([n] \times \delta : [n] \to [n + 1]\). Given a map \(s : [0] \to [n]\) we can compose to get \(([n] \times \delta) \circ s : [0] \to [n + 1]\). ◻
Lemma 1. For any representable \(\mathbf{y}[n]\), any map \(1 \to \mathbf{y}[n]\) is a trivial cofibration.
Proof. Note that \(1 = \mathbf{y}[0]\). Hence it suffices to show by induction on \(n\) that for any map \(s : [0] \to [n]\), \(\mathbf{y}s : \mathbf{y}[0] \to \mathbf{y}[n]\) is a trivial cofibration. For \(n = 0\), since \([0]\) is the terminal object, any map \([0] \to [0]\) is an isomorphism, and so a trivial cofibration.
Given any map \(s : [0] \to [n + 1]\), we have \([n + 1] \cong [n] \times [1]\), and so we can factor \(s\) as \(([n] \times d) \circ s'\), where \(d : [0] \to [1]\) is defined by \(d := \pi_1 \circ s\) and \(s' : [0] \to [n]\) is defined by \(\pi_0 \circ s\). By induction \(\mathbf{y}s'\) is a trivial cofibration, and \(\mathbf{y}[n] \times \mathbf{y}d\) is a trivial cofibration, by [it:kanishurewicz] in the list of basic facts about cubical sets above. ◻
Since \(\square\) has a terminal object, the unique functor \(\square \to 1\) has a right adjoint. This induces a string of adjunctions \(\Delta \dashv \Gamma \dashv \nabla\) by reindexing and right Kan extension as illustrated below. \[\begin{tikzcd}[sep=5em] \mathbf{Set}\ar[r, bend left, yshift=0.6em, "\Delta" description] \ar[r, bend right, swap, yshift=-0.6em, "\nabla" description] \ar[r, phantom, yshift = 1em, "\perp"] \ar[r, phantom, yshift = -1em, "\perp"] & \widehat{\square}\ar[l, "\Gamma" description] \end{tikzcd}\]
Since \(\Delta\) can be explicitly described as reindexing along the unique functor \(\square \to 1\), one can easily show the following proposition.
Proposition 3. \(\Delta\) preserves all limits, colimits and dependent products.
Remark 4. The above results also hold for simplicial sets, so the arguments below will also apply there.
We can now show a key theorem about the behaviour of propositional truncation in cubical sets, using a technique due to Uemura. The idea here is that propositional truncation does not identify points of a type, but only adds new paths between them. Hence we should visualise h-propositions in general not as spaces with at most one point, but rather as many points where any two are connected by a path.
Theorem 5. Suppose we are given a fibration \(f : W \to \Delta Z\) in cubical sets. If \(\| W \|_{\Delta Z} \to \Delta Z\) has a section, then so does the map \(\Gamma W \to \Gamma \Delta Z \cong Z\).
Proof. We first recall that \(\nabla_Z \Gamma W\) is defined as follows. The unit map \(Z \to \Gamma \Delta Z\) is an isomorphism, and so has an inverse, say \(i : \Gamma \Delta Z \stackrel{\cong}{\to} Z\). Under the adjunction \(\Gamma \dashv \nabla\), \(i\) corresponds to a map \(\Delta Z \to \nabla Z\), and composing \(i\) with \(\Gamma f : \Gamma W \to \Gamma \Delta Z\) gives a map \(\Gamma W \to Z\). We then define \(\nabla_Z \Gamma W\) as the pullback below. \[\begin{tikzcd} \nabla_Z \Gamma W \ar[r] \ar[d] \ar[dr, phantom, very near start, "\lrcorner"]& \nabla \Gamma W \ar[d] \\ \Delta Z \ar[r] & \nabla Z \end{tikzcd}\] The left hand map \(\nabla_Z \Gamma W \to \Delta Z\) is an h-proposition and in particular a Kan fibration - see [9] for details. We can then extend the diagram above to the solid lines in the diagram below. \[\begin{tikzcd} W \ar[d] \ar[drr, bend left] \ar[dr] & & \\ \| W \|_{\Delta Z} \ar[dr] \ar[r, dotted] & \nabla_Z \Gamma W \ar[d] \ar[r] \ar[dr, phantom, very near start, "\lrcorner"]& \nabla \Gamma W \ar[d] \\ & \Delta Z \ar[r] & \nabla Z \end{tikzcd}\] Since the map \(\nabla_Z \Gamma W \to \Delta Z\) is an h-proposition we obtain the dotted map in the diagram above. Composing this with the section of \(\| W \|_{\Delta Z} \to \Delta Z\) gives us a section of the map \(\nabla_Z \Gamma W \to \Delta Z\). We can then use this to obtain a section of \(\Gamma W \to \Gamma \Delta Z\) using the adjunction \(\Gamma \dashv \nabla\), as in [9]. ◻
Remark 6. Theorem 5 is fairly specific to cubical sets. In order to apply Uemura’s proof we additionally need to assume that cofibrations are pointwise decidable and that the interval is representable, has disjoint endpoints and no points other than the endpoints. Most critically, Uemura’s proof is specific to the definition of Kan fibration for cubical sets. This is the same as one of the common ways to define Kan fibration in simplicial sets, but e.g. does not apply to localisations, which can have a smaller class of fibrations on the same underlying category.
Corollary 7. Given a Kan fibration \(X \to Y\) in cubical sets, if the fibration \(\| X \|_Y \to Y\) has a section, then so does the map \(\Gamma X \to \Gamma Y\).
Proof. Write \(e : \Delta \Gamma Y \to Y\) for the counit map of the adjunction \(\Delta \dashv \Gamma\). We pullback the section of \(\| X \|_Y \to Y\) along \(e\) as illustrated below. \[\begin{tikzcd} e^\ast \| X \|_{Y} \ar[r] \ar[d] \ar[dr, phantom, very near start, "\lrcorner"]& \| X \|_Y \ar[d] \\ \Delta \Gamma Y \ar[r] \ar[u, bend left] & Y \ar[u, bend right] \end{tikzcd}\] Propositional truncation is stable under pullback, and so we have \(e^\ast \|X\|_Y \cong \| e^\ast(X)\|_{\Delta\Gamma Y}\). However, we can now apply Theorem 5 with \(Z := \Gamma Y\) and \(W := e^\ast(X)\) and observe \(\Gamma (e^\ast(X)) \cong \Gamma X\) to obtain the conclusion. ◻
Theorem 5 gives us an easy direct way to see how it can happen that not every h-proposition is equivalent to a monomorphism. Suppose we are working internally in a category where the axiom of choice fails, i.e. where there is a regular epimorphism \(f : X \to Z\) in \(\mathbf{Set}\) that does not have a section. Suppose that the h-proposition \(\| \Delta X \|_{\Delta Z} \to \Delta Z\) is logically equivalent to a monomorphism \(m : Y \to \Delta Z\). Using the logical equivalence, the regular epimorphism \(\Delta(f) : \Delta X \to \Delta Z\) factors through \(m\), which implies \(m\) is an isomorphism. Using the other direction of the logical equivalence, we see that \(\| \Delta X \|_{\Delta Z} \to \Delta Z\) has a section, and so \(f\) must also have a section.
As we remarked at the end of the last section, h-propositions in \(\widehat{\square}\) are not necessarily the same as monomorphisms. However, we have a third class we can consider: monomorphisms of the form \(\Delta(m)\) where \(m\) is a monomorphism in sets. We might wonder if there are examples of h-propositions in \(\widehat{\square}\) that are monomorphisms but do not arise from monomorphisms in \(\mathbf{Set}\) because they are not in the image of \(\Delta\).
The aim of this section is to show that in fact this is not the case: once we restrict to h-propositions that are monomorphisms they are necessarily of the form \(\Delta(m)\) where \(m\) is a monomorphism in \(\mathbf{Set}\). Moreover, we will see a useful theorem that can be applied to classes of monomorphisms in \(\mathbf{Set}\) that are all classified by a single “universal” element \(m\). For a monic fibration \(f : X \to Y\), once we know \(\Gamma(f)\) belongs to the class, we can deduce that \(f\) is a pullback of \(\Delta(m)\).
For this section and the next we only need a smaller subset of the properties of cubical sets. In fact the results of this section will hold for any category of internal presheaves on an internal category \(\mathcal{C}\) in a locally cartesian closed category equipped with a weak factorisation system with the following properties, referring to the left class of the weak factorisation system as trivial cofibrations and the right class as fibrations.
\(\mathcal{C}\) has a terminal object.
Every object \(c\) of \(\mathcal{C}\) admits a map \(1 \to c\).
Every map \(1 \to \mathbf{y}c\) is a trivial cofibration.
Proposition 8. Let \(m : P \rightarrowtail Q\) be a monomorphism in a locally cartesian closed category \(\mathcal{E}\). The following are equivalent:
In the internal language of \(\mathcal{E}\) we have \(\forall q, q' : Q \mathpunct{.} (P_{q} \leftrightarrow P_{q'}) \rightarrow q = q'\)
For any monomorphism \(f : X \to Y\), there is at most one map \(\chi : Y \to Q\) forming the bottom map in a pullback diagram of the form below: \[\label{eq:1} \begin{tikzcd} X \ar[r] \ar[d, "f"] \ar[dr, phantom, very near start, "\lrcorner"]& P \ar[d, "m"] \\ Y \ar[r, "\chi"] & Q \end{tikzcd}\qquad{(1)}\]
Proof. We first show the direction \((\Rightarrow)\). Suppose that we have two maps \(\chi, \chi' : Y \to Q\) fitting into the bottom map of a pullback as in ?? . To show \(\chi = \chi'\), it suffices to prove in the internal language that for all \(y : Y\) we have \(\chi(y) = \chi'(y)\). However, we have equivalences \(P_{\chi(y)} \leftrightarrow X_{y}\) and \(P_{\chi'(y)} \leftrightarrow X_{y}\) by expressing the fact that the squares are pullbacks in the internal language. Combining these gives an equivalence \(P_{\chi(y)} \leftrightarrow P_{\chi'(y)}\) and so we deduce \(\chi(y) = \chi'(y)\) by assumption.
We now show the direction \((\Leftarrow)\). We construct in the internal language the type \(Y := \sum_{q, q' : Q} P_{q} \leftrightarrow P_{q'}\). We obtain a monomorphism \(f : X \to Y\) by pulling back \(m\) along the projection map \(\pi_0 : \sum_{q, q' : Q} P_{q} \leftrightarrow P_{q'} \;\to\; Q\). We define \(\chi := \pi_0\). We define \(\chi'\) by projecting out the second \(Q\) component, i.e. \(\chi' := \pi_0 \circ \pi_1\). Using the equivalence \(P_{q} \leftrightarrow P_{q'}\), we can show \(f\) is also the pullback of \(m\) along \(\chi'\). Hence \(\chi = \chi'\) by assumption, and so we have that \(q = q'\) whenever \(P_{q} \leftrightarrow P_{q'}\). ◻
Definition 9. If \(m : P \to Q\) satisfies the equivalent conditions above, we say it is extensional.
We recall some standard facts and terminology about extensional monomorphisms.
Definition 10. We refer to the unique map \(\chi\), when it exists, as the classifying map for the monomorphism \(f\) in ?? . We say \(m : P \to Q\) is the classifier for the class of monomorphisms obtained by pulling it back along arbitrary maps.
Remark 11. A given class of monomorphisms has at most one classifier up to isomorphism.
Proposition 12. If \(m : P \to Q\) is extensional, then \(P\) is subterminal, and terminal whenever \(\exists q : Q \mathpunct{.} P_q\) holds in the internal language.
Proof. Internally, we can think of \(P\) as \(\sum_{q : Q} P_q\). Given \(q, q'\) such that \(P_q\) and \(P_{q'}\) are both inhabited, we have \(P_q \Leftrightarrow \top \Leftrightarrow P_{q'}\) and so \(q = q'\) by extensionality. Since any two elements of \(P_q = P_{q'}\) are equal, we can deduce that \(\sum_{q : Q} P_q\) has at most one element. ◻
Proposition 13. Suppose we have exact quotients. Then every monomorphism is a pullback of an extensional monomorphism.
Proof. Given a monomorphism \(m : P \to Q\), we define an equivalence relation on \(Q\) by setting \(q \sim q'\) whenever we have \(P_q \leftrightarrow P_{q'}\). We define \(Q'\) to be the quotient \(Q/{\sim}\). Given \(x : Q'\) we define a proposition \(P'_x\) as \(\prod_{q : Q} x = [q] \rightarrow P_q\). By exactness, we have that for \(q, q' : Q\), whenever \([q] = [q']\) we have \(P_q = P_{q'}\). It follows that for \(q : Q\), \(P_q \;\leftrightarrow\; \prod_{q' : Q} ([q] = [q'] \rightarrow P_{q'})\). From this it follows that \(m\) is the pullback of \(m' := \sum_{x : Q'} P'_x\) along the quotient map. ◻
When working with extensional monomorphisms \(P \to Q\) in the internal language, we will also write the fibre \(P_x\) as \([x]\) for \(x : Q\).
We now see the first key theorem, which shows that given an extensional monomorphism in our metatheory, the class of monomorphisms classified by the extensional monomorphism is essentially unchanged by passing into cubical sets via \(\Delta\).
Lemma 2. Suppose that \(f : X \to Y\) is both a monomorphism and a fibration. For any map \(s : 1 \to [n]\) in the cube category \(\square\), the naturality square below is a pullback. \[\begin{tikzcd} X_{n} \ar[d, tail, "f_n"] \ar[r, "X_{s}"] & X_{0} \ar[d, tail, "f_0"] \\ Y_{n} \ar[r, "Y_{s}"] & Y_{0} \end{tikzcd}\]
Proof. In any case we can construct the pullback \(s^\ast(f_0)\) as follows: \[\begin{tikzcd} X_{n} \ar[dr, swap, tail, "f_n"] \ar[r, "X_{s}"] & s^\ast(X_{0}) \ar[r] \ar[d, tail, "s^\ast(f_0)"] \ar[dr, phantom, very near start, "\lrcorner"]& X_{0} \ar[d, tail, "f_0"] \\ & Y_{n} \ar[r, "Y_{s}"] & Y_{0} \end{tikzcd}\]
Since \(f_n\) and \(s^\ast(f_0)\) are both monomorphisms, and we already have a map \(X_{n} \to s^\ast(X_{0})\) over \(Y_{n}\), to show they are isomorphic it suffices to construct a map in the other direction \(s^\ast(X_{0}) \to X_{n}\) over \(Y_{n}\). Elements of \(s^\ast(X_{0})\) correspond precisely to commutative squares as in the solid lines below. \[\begin{tikzcd} \mathbf{y}[0] \ar[r] \ar[d, "\mathbf{y}s"] & X \ar[d, "f"] \\ \mathbf{y}[n] \ar[r] \ar[ur, dotted] & Y \end{tikzcd}\]
However, since \(\mathbf{y}s\) is a trivial cofibration by Lemma 1 and \(f\) is a fibration by assumption, we can choose a diagonal filler as in the dotted line above. This precisely gives us a choice of element of \(X_{n}\) in the fibre of \(y \in Y_{n}\). Putting these together gives the required map \(s^\ast(X_{0}) \to X_{n}\). ◻
Lemma 3. Suppose that \(f : X \to Y\) is both a monomorphism and a fibration. For any map \(s : [n] \to [m]\) in the cube category the corresponding naturality square is a pullback. \[\begin{tikzcd} X_{m} \ar[d, "f_m"] \ar[r, "X_{s}"] & X_{n} \ar[d, "f_n"] \\ Y_{m} \ar[r, "Y_{s}"] & Y_{n} \end{tikzcd}\]
Proof. By Proposition 2 we have some map \(t : 1 \to [n]\). We can therefore extend the diagram above as follows. \[\begin{tikzcd} X_{m} \ar[d, "f_m"] \ar[r, "X_{s}"] & X_{n} \ar[d, "f_n"] \ar[r, "X_{t}"] & X_{0} \ar[d, "f_0"] \\ Y_{m} \ar[r, "Y_{s}"] & Y_{n} \ar[r, "Y_{t}"] & Y_{0} \end{tikzcd}\]
By Lemma 2 both the right hand square and the whole rectangle are pullbacks. Hence the left hand square is also a pullback. ◻
Theorem 14. Suppose that \(f : X \to Y\) is a map in cubical sets that is both a fibration and a monomorphism, and that \(\Gamma(f) : \Gamma(X) \to \Gamma(Y)\) is a pullback of an extensional monomorphism \(g : P \to Q\). Then \(f\) is a pullback of \(\Delta(g) : \Delta(P) \to \Delta(Q)\).
Proof. First note that by Proposition 2 and Lemma 2, for each \(n\) the map \(f_n : X_{n} \to Y_{n}\) is a pullback of \(f_0 : X_{0} \to Y_{0}\) along some map, and so a pullback of \(g\). By extensionality, this determines a unique map \(\chi_n : Y_{n} \to Q\). To show this gives a morphism of cubical sets, we need to check naturality, which amounts to the following commutative triangles for each \(s : [n] \to [m]\). \[\begin{tikzcd} Y_m \ar[d, swap, "Y_{s}"] \ar[r, "\chi_m"] & Q \\ Y_n \ar[ur, swap, "\chi_n"] & \end{tikzcd}\]
However, note that \(\chi_n \circ Y_s\) is a classifying map for \(f_m\), by observing that both squares in the diagram below are pullbacks; the left hand square by Lemma 3 and the right hand square by the definition of \(\chi_n\). Since \(\chi_m\) is also a classifying map for \(f_m\) we have \(\chi_n \circ Y_s = \chi_m\) by extensionality. \[\begin{tikzcd} X_m \ar[r, "X_s"] \ar[d] & X_n \ar[r] \ar[d] & P \ar[d] \\ Y_m \ar[r, "Y_s"] & Y_n \ar[r, "\chi_n"] & Q \end{tikzcd}\]
Finally, since pullbacks are computed pointwise, it is clear from the definition of \(\chi_n\) that \(f\) is the pullback of \(\Delta(g)\) along \(\chi\). ◻
Remark 15. Fibrations which are also monomorphisms can be understood syntactically by augmenting type theory with a universe of strict propositions [15]. As a consequence of Theorem 14, when cubical sets are constructed in the internal language of a topos we can interpret the universe of strict propositions as \(\Delta(\Omega)\).
We have seen so far that in general it is best to view h-propositions not as types with “at most one point” but rather as types with many points that are all joined together by paths. Next, we saw in Section 3 that the subclass of monic fibrations, which are h-propositions that really do have at most one point, is well behaved and corresponds closely to monomorphisms in sets.
We now restrict to the subclass of \(\neg\neg\)-stable h-propositions. The main motivation for doing this is that, as we will see, \(\neg\neg\)-stable h-propositions are necessarily monomorphisms up to equivalence, allowing us to apply the results from Section 3.
In contrast to the class of all monic fibrations, we have a clear definition of which h-propositions are \(\neg\neg\)-stable inside type theory. As a consequence of this, we can define classes both of \(\neg\neg\)-stable propositions in sets and of \(\neg\neg\)-stable h-propositions in cubical sets. Hence we can compare these two classes, and we will see that in fact they are closely related. In particular, given a classifier for \(\neg\neg\)-stable propositions in sets, say \(\Omega_{\neg\neg}\), we can obtain a classifier of \(\neg\neg\)-stable h-propositions in cubical sets simply as the constant cubical set \(\Delta(\Omega_{\neg\neg})\).
Although the class of \(\neg\neg\)-stable h-propositions is a somewhat restricted class compared to the class of all h-propositions, it suffices for some key constructions. For this paper these applications are constructing the Dedekind real numbers and defining extended Church’s thesis. The latter is related to the fact that \(\neg\neg\)-stable propositions play an important role in realizability models, and e.g. appear frequently in [16].
Again, we will not need all of the properties of cubical sets. The results of this section will hold for any category of internal presheaves in a locally cartesian closed category equipped with a weak factorisation system, such that in addition to the properties from Section 3 we have the following.
Dependent products preserve fibrations.
For any \(Y\), the unique map \(\bot \to Y\) is a fibration.
Throughout this section, for a given map \(X \to Y\) we write \(\neg X\) to mean the negation of \(X\) computed in the slice category over \(Y\), i.e. functions to \(\bot\) using the local exponential over \(Y\).
Lemma 4. For any map \(f : X \to Y\), the negation \(f' : \neg X \to Y\) is a monomorphism. If \(f\) is a fibration, then so is \(f'\).
Proof. The exponential \((-)^X\) in \(\widehat{\square}/Y\) preserves limits and so in particular preserves subterminals. Since \(\bot \to Y\) is subterminal in \(\widehat{\square}/Y\), so is \(\neg X = \bot^X\).
To show that \(f'\) is a fibration, we recall that the list of basic facts about cubical sets in Section 2 included the facts that the initial object is fibrant and dependent products preserve fibrations. The map \(\bot \to Y\) is the pullback of \(0 \to 1\) along the unique map \(Y \to 1\), and so also a fibration. The local exponential can be constructed using dependent product and pullback, and so also preserves fibrations. These two together suffice to show \(f' : \neg X \to Y\) is a fibration. ◻
Lemma 5. For any map \(f : X \to Y\), we have an isomorphism between \((\neg X)_0\) and \(\neg X_0\) as subobjects of \(Y_0\).
Proof. Since these are both subobjects of \(Y_0\), to show they are isomorphic, it suffices to show they are logically equivalent over \(Y_0\).
We first construct the map \((\neg X)_0 \to \neg X_0\) over \(Y_0\). By the adjunction between products and exponentials in \(\mathbf{Set}/Y_0\), it suffices to construct a map \(X_0 \times (\neg X)_0 \to \bot\). However, this can be obtained by simply applying \(\Gamma\) to the evaluation map \(X \times (\neg X) \to \bot\).
We now construct the map \(\neg X_0 \to (\neg X)_0\) over \(Y_0\). We can explicitly describe \(\neg X_0\) as the subobject of \(Y_{0}\) consisting of \(y \in Y_0\) such that the fibre \(f_0^{-1}(y)\) is empty. Using this, we need to find a (necessarily unique) global section of \(\neg X\) over \(y\). This is the same as constructing a map \(\ulcorner y \urcorner^\ast X \to \bot\), where \(\ulcorner y \urcorner : 1 \to Y\) corresponds to \(y \in Y_0\) under the Yoneda equivalence. That is, for each \(n \in \square\) we need to derive a contradiction from the existence of \(x \in X_n\) such that \(f_n(x) = Y_!(y)\), where \(!\) is the unique map \([n] \to [0]\). However, for any \(n\) we can find a map \(s : [0] \to [n]\) by Proposition 2, and so given any such \(x\) produce an element \(X_s(x)\) of \(X_0\), which must lie in the fibre of \(y\) since \(! \circ s\) is necessarily the identity on \([0]\). ◻
Theorem 16. Suppose \(m : 1 \to \Omega_{\neg \neg}\) is a classifier for all \(\neg \neg\)-stable propositions. Then \(\Delta(m) : \Delta(1) \to \Delta(\Omega_{\neg \neg})\) is a homotopy classifier for all \(\neg \neg\)-stable h-propositions in cubical sets.
Proof. Suppose that \(f : X \to Y\) is a \(\neg \neg\)-stable h-proposition. This implies that \(f\) is equivalent to its double negation, which we will write as \(f' : \neg \neg X \to Y\). By Lemma 4 \(f'\) is a monomorphism. By Lemma 5 \(f'_0 : (\neg \neg X)_0 \to Y_0\) is equivalent to \(\neg (\neg X)_0\) and so also \(\neg \neg\)-stable. Hence \(f'_0\) is a pullback of \(m : 1 \to \Omega_{\neg \neg}\) and so by Theorem 14 \(f'\) is a pullback of \(\Delta(m) : \Delta(1) \to \Delta(\Omega_{\neg \neg})\). Since \(f\) is equivalent to \(f'\) it is therefore a homotopy pullback of \(\Delta(m) : \Delta(1) \to \Delta(\Omega_{\neg \neg})\).
Finally, to show \(\Delta(1) \to \Delta(\Omega_{\neg \neg})\) classifies the \(\neg \neg\)-stable h-propositions exactly, we need to verify that it is \(\neg \neg\)-stable itself. However, this follows from the fact that \(\Delta\) preserves initial object and dependent products, and so preserves double negation. ◻
There are many situations where we have access to classifiers for \(\neg \neg\)-stable propositions, the most important being the following.
Example 1. Any topos has a classifier for all \(\neg \neg\)-stable propositions by defining it as the obvious subobject of the subobject classifier.
Example 2. A category of assemblies has a classifier for \(\neg \neg\)-stable propositions, assuming they were constructed in a metatheory with the same. Namely, if \(\Omega_{\neg \neg}\) is a classifier for \(\neg \neg\)-stable propositions in sets, we define an assembly with underlying set \(\Omega_{\neg \neg}\) and uniform realizability predicate \(E(p) := \{0\}\). Every \(\neg \neg\)-stable monomorphism is a uniform map in the sense of [16]. In this way, we can think of \(\neg \neg\)-stable h-propositions in cubical assemblies as proof irrelevant on two different levels. By Lemma 4 they are monomorphisms, and so types where any two elements are strictly equal. However, in addition their underlying monomorphism in assemblies is also \(\neg \neg\)-stable by Lemma 5, and so uniform, which can be seen as a form of proof irrelevance inherent to categories of assemblies and other realizability models.
Remark 17. To follow up on Remark 15, as an alternative to interpreting strict propositions as the collection of all monomorphisms, we could instead restrict to only \(\neg \neg\)-stable propositions, and in particular interpret the universe of strict propositions as \(\Delta(\Omega_{\neg \neg})\).
We recall, e.g. from [17] that the Dedekind reals can be defined constructively using the notion of left cut, as given below.
Definition 18. A Dedekind left cut is a set \(L \subseteq \mathbb{Q}\) satisfying the following properties:
(Boundedness) There exist rational numbers \(a \in L\) and \(b \notin L\).
(Openness) For all \(a \in L\) there merely exists \(b \in L\) such that \(b > a\).
(Locatedness) For all \(a < b \in \mathbb{Q}\) either \(a \in L\) or \(b \notin L\).
Remark 19. It follows from locatedness that \(L\) is downwards closed.
In this paper we will, however, not use left cuts directly, but instead a variant that we refer to as cocut. The reason for this is that it will turn out that cocuts are \(\neg \neg\)-stable as subsets of \(\mathbb{Q}\), allowing us to apply the results of Section 4.
Definition 20. A co-left cut or just a cocut is a set \(C \subseteq \mathbb{Q}\) satisfying the following properties:
(Boundedness) There exist rational numbers \(a \notin C\) and \(b \in C\).
(Closedness) For all \(a \in \mathbb{Q}\), if \(b \in C\) for all \(b > a\), then \(a \in C\).
(Locatedness) For all \(a < b \in \mathbb{Q}\) either \(a \notin C\) or \(b \in C\).
As before, note that any cocut is upwards closed by locatedness.
We can translate between the two definitions using the following operations. For each \(L \subseteq \mathbb{Q}\) we define \(\neg L\) and \(L^<\) as follows: \[\begin{align} \neg L &:= \mathbb{Q}\setminus L \\ L^< &:= \{ a \in \mathbb{Q}\;|\; \exists b \in L \mathpunct{.} a < b \} \end{align}\]
Proposition 21.
If \(L \subseteq \mathbb{Q}\) is a left cut then \(\neg L\) is a cocut, and \(L = (\neg \neg L)^<\).
If \(C \subseteq \mathbb{Q}\) is a cocut then \((\neg C)^<\) is a left cut and \(C = \neg ((\neg C)^<)\).
Proof. Suppose first that \(L\) is a left cut. It is clear that \(\neg L\) is bounded, and closedness and locatedness of \(\neg L\) easily follow from openness and locatedness of \(L\) respectively. Given \(a \in L\), there exists \(b \in L\) such that \(a < b\). We then have \(b \in \neg \neg L\), and so \(a \in (\neg \neg L)^<\). Hence \(L \subseteq (\neg \neg L)^<\). Given \(a \in (\neg \neg L)^<\), there exists \(b \in \neg \neg L\) such that \(a < b\). By locatedness, either \(a \in L\) or \(b \notin L\). However, the latter contradicts \(b \in \neg \neg L\), and so we have \(a \in L\), giving \((\neg \neg L)^< \subseteq L\).
Now suppose that \(C\) is a cocut. Note that \((\neg C)^<\) is open by definition, and it is bounded by the boundedness of \(C\). To check locatedness, suppose we are given \(a < b \in \mathbb{Q}\). By locatedness of \(C\) we know that either \(\frac{a + b}{2} \notin C\) or \(b \in C\). The former implies \(a \in (\neg C)^<\) and the latter implies \(b \notin (\neg C)^<\).
To check that \(C \subseteq \neg((\neg C)^<)\), suppose \(a \in C\). To show \(a \in \neg((\neg C)^<)\), we need to derive a contradiction from the assumption \(a \in (\neg C)^<\), so suppose there is \(b > a\) such that \(b \notin C\). However, since \(C\) is upwards closed, this contradicts \(a \in C\), as required. We now check that \(\neg((\neg C)^<) \subseteq C\). Suppose that \(a \in \neg((\neg C)^<)\). To show \(a \in C\), it suffices, by closedness, to check that for all \(b > a\), \(b \in C\). For any \(b > a\), we have by locatedness that either \(\frac{a + b}{2} \notin C\) or \(b \in C\). The former implies that \(a \in (\neg C)^<\), contradicting \(a \in \neg((\neg C)^<)\), and so we must have \(b \in C\), as required. ◻
Proposition 22. Let \(C\) be a cocut. Then \(a \in C\) if and only if for all \(n \in \mathbb{N}\), \(a + \frac{1}{n + 1} \in C\).
Proof. The implication \((\Rightarrow)\) follows from the fact that \(C\) is upwards closed.
It remains to check the implication \((\Leftarrow)\). Suppose that for all \(n \in \mathbb{N}\), \(a + \frac{1}{n + 1} \in C\). To show \(a \in C\) it suffices by closedness to show that \(b \in C\) for all \(b > a\). For any \(b > a\) we can find \(n\) such that \(a < a + \frac{1}{n + 1} < b\). By assumption \(a + \frac{1}{n + 1} \in C\), and so \(b \in C\) since \(C\) is upwards closed. ◻
Corollary 23. If we have a classifier for \(\neg \neg\)-stable propositions in the metatheory, then there is a type of all Dedekind real numbers in cubical sets.
Proof. By Proposition 21, every cocut \(C\) is equivalent to \(\neg ((\neg C)^<)\) and so \(\neg \neg\)-stable. Hence we can construct the collection of all cocuts using the classifier for \(\neg \neg\)-stable h-propositions given in Theorem 16. ◻
As stated in the conclusion to [10], the main barrier to finding a model of extended Church’s thesis was finding a good way to formulate partial functions within cubical sets. However, \(\neg\neg\)-stable propositions suffice for stating a formulation of extended Church’s thesis for partial functions based on the axiom \(\mathbf{ECT}'_0\) appearing in [18]. Namely, given a classifier for \(\neg\neg\)-stable h-propositions, \(\Omega_{\neg \neg}\), we define for types \(X\) and \(Y\) the type \(\operatorname{Partial}_{\neg \neg}(X, Y) := \sum_{D : X \to \Omega_{\neg\neg}} \prod_{x : X} [D(x)] \to Y\).
We will state Church’s thesis using Kleene’s \(T\) predicate and extraction function \(U\). Recall that \(T(e, x, z)\) is a primitive recursive predicate stating that \(z\) encodes a valid sequence of states for the \(e\)th Turing machine with input \(x\) starting with the initial state and ending with the halting state. \(U(z)\) is then the resulting output of the halting computation.
Definition 24. Extended Church’s thesis, or \(\mathbf{ECT}\) is the axiom \[\prod_{f : \operatorname{Partial}_{\neg \neg}(\mathbb{N}, \mathbb{N})}\left\| \sum_{e : \mathbb{N}}\prod_{x : \mathbb{N}} \prod_{w : [\pi_0(f)(x)]} \sum_{z : \mathbb{N}}T(e, x, z) \times U(z) = \pi_1(f)(x, w)\right\|\]
Remark 25. Note that \(\mathbf{ECT}\) does not assert the existence of a computable partial function with the same domain as \(f\) but rather with a domain which is a superset of that of \(f\), and in many cases the domain will be strictly larger. For example, define \(T \subseteq \mathbb{N}\) to be the set of numbers \(e\) such that the computable function \(\varphi_e\) is total. In the presence of Markov’s principle \(T\) is \(\neg \neg\)-stable, and so \(\mathbf{ECT}\) tells us that any function \(\mathbb{N}^\mathbb{N}\to \mathbb{N}\) can be represented as a partial function \(\varphi_e : \mathbb{N}\rightharpoondown \mathbb{N}\) whose domain includes \(T\). However, the domain of any computable partial function is computably enumerable, whereas \(T\) is not computably enumerable, and so the domain of \(\varphi_e\) cannot be equal to \(T\).
First note that we have an “absoluteness” result for partial functions from \(\mathbb{N}\) to \(\mathbb{N}\) with \(\neg\neg\)-stable domain, i.e. the following proposition.
Proposition 26. The type of partial functions from \(\mathbb{N}\) to \(\mathbb{N}\) with \(\neg\neg\)-stable domain in homotopy type theory is implemented in cubical sets as \(\Delta(\operatorname{Partial}_{\neg \neg}(\mathbb{N}, \mathbb{N}))\).
Proof. \(\Delta\) preserves all dependent products and sums, the natural number object, and by Theorem 16 also preserves the classifier for \(\neg\neg\)-stable propositions. But these suffice to construct \(\operatorname{Partial}_{\neg \neg}(\mathbb{N}, \mathbb{N})\). ◻
Theorem 27. The following axioms can be consistently added to Martin-Löf type theory:
Propositional truncation
The axiom of univalence
The existence of a classifier for \(\neg\neg\)-stable h-propositions
Extended Church’s thesis
Markov’s principle
Proof. Following [10] we first construct the cubical assemblies model of homotopy type theory by defining cubical sets internally in assemblies over the first Kleene algebra. We then define a reflective subuniverse where extended Church’s thesis is forced to hold by nullification. Namely we nullify the family of propositions defined as the interpretation of the following types in cubical assemblies. \[f : \operatorname{Partial}_{\neg \neg}(\mathbb{N}, \mathbb{N}) \vdash \left\| \sum_{e : \mathbb{N}}\prod_{x : \mathbb{N}} \prod_{w : [\pi_0(f)(x)]} \sum_{z : \mathbb{N}}T(e, x, z) \times U(z) = \pi_1(f)(x, w)\right\|\] To ease notation, we define \(A\) and \(B\) as follows. \[\begin{align} A &:= \operatorname{Partial}_{\neg \neg}(\mathbb{N}, \mathbb{N}) \\ B &:= \sum_{e : \mathbb{N}} \prod_{x : \mathbb{N}} \prod_{w : [\pi_0(f)(x)]} \sum_{z : \mathbb{N}}T(e, x, z) \times U(z) = \pi_1(f)(x, w) \end{align}\]
By Proposition 26 the interpretation of \(A\) in cubical assemblies is discrete, and moreover is the image under \(\Delta\) of the interpretation of the same type in assemblies. Since the category of assemblies satisfies extended Church’s thesis, by a similar argument to that in [16], the interpretation of \(A \vdash B\) in assemblies is well supported. We can therefore apply the same arguments as in [10] to show that the reflective subuniverse has the same natural number type and empty type as the original cubical assemblies model. The latter implies that the model is non trivial, and that every \(\neg\neg\)-stable h-proposition in the reflective subuniverse is already \(\neg\neg\)-stable in the original model. It follows that \(1 \to \Delta(\Omega_{\neg \neg})\) still acts as a classifier for \(\neg\neg\)-stable h-propositions in the reflective subuniverse. We can therefore use the same argument as in [10] to show that the resulting model is non trivial and satisfies extended Church’s thesis and Markov’s principle. ◻
In Section 5 we gave a construction of the Dedekind reals in cubical sets that relied on having a classifier for \(\neg\neg\)-stable propositions in our metatheory. Since this involves some impredicativity, it is not always viewed as constructively acceptable. We therefore also give a predicative proof using a smaller class of h-propositions that suffice to construct the Dedekind real numbers.
Definition 28. A monomorphism \(A \to B\) is \(\Pi^0_1\) if there is a function \(g : B \times \mathbb{N}\to 2\) such that \(\prod_{b : B} (A_b \leftrightarrow \prod_{n : \mathbb{N}} g(b, n) = 0)\).
Example 3. Every exact locally cartesian closed category with natural number object has an extensional monomorphism \(1 \to \Omega_{\Pi^0_1}\) such that every \(\Pi^0_1\) monomorphism is a pullback of \(1 \to \Omega_{\Pi^0_1}\), as a special case of Proposition 13.
Example 4. Categories of assemblies have classifiers for \(\Pi^0_1\)-monomorphisms, assuming they are constructed in a metatheory that also has a classifier for \(\Pi^0_1\)-monomorphisms.
Definition 29. An h-proposition \(f : X \to Y\) is weakly \(\Pi^0_1\) if there is an h-proposition \(R \to Y \times \mathbb{N}\) together with terms witnessing \(\prod_{y : Y} \prod_{n : \mathbb{N}} \| R_{y, n} + \neg X_{y}\|\) and \(\prod_{y : Y} (X_y \leftrightarrow \prod_{n : \mathbb{N}} R_{y, n})\).
The following two propositions are not formally required, but explain our choice of terminology.
Proposition 30. Every \(\Pi^0_1\) h-proposition is weakly \(\Pi^0_1\).
Proof. Suppose that we have \(g : B \times \mathbb{N}\to 2\) as in Definition 28. Define \(R_{b, n} := g(b, n) = 0\). For any \(b : B\) and \(n : \mathbb{N}\), either \(g(b, n) = 0\) or \(g(b, n) = 1\). The former is precisely \(R_{b, n}\), and the latter implies \(\neg \prod_{n : \mathbb{N}} R_{b, n}\) and thereby \(\neg [b]\), and so we have \(R_{b, n} \vee \neg [b]\). ◻
Proposition 31. Suppose that every function \(\mathbb{N}\to \mathbb{N}\) is computable. Then a subobject of \(\mathbb{N}^k\), say \(A \hookrightarrow \mathbb{N}^k\) is a \(\Pi^0_1\)-monomorphism if and only if there is a primitive recursive formula \(\phi(x_1,\ldots,x_k; y)\) in the language of first order arithmetic such that \[\forall x_1,\ldots,x_k \mathpunct{.} A(x_1,\ldots,x_k) \leftrightarrow \forall y \mathpunct{.} \phi(x_1,\ldots,x_k;y)\]
Proof. Let \(g : \mathbb{N}^k \times \mathbb{N}\to 2\) be as in Definition 28. Let \(e\) be a code for a Turing machine whose output matches \(g\), i.e. for all \(x_1,\ldots,x_k, y\) we have \(\varphi_e(x_1,\ldots,x_k, y) = g(x_1,\ldots,x_k, y)\). By standard arguments we may assume we are given a primitive recursive bijection \(i : \mathbb{N}\stackrel{\cong}{\to} \mathbb{N}\times \mathbb{N}\). We take \(\phi(x_1,\ldots,x_k; y)\) to be the formula stating that if \(\varphi_e(x_1,\ldots,x_k, \pi_0(i(y)))\) halts within \(\pi_1(i(y))\) steps then \(\varphi_e(x_1,\ldots,x_k, \pi_0(i(y))) = 0\), which is clearly primitive recursive.
The converse is clear. ◻
The motivation for the definition of weakly \(\Pi^0_1\) h-proposition is that we can apply it to the definition of the Dedekind reals in terms of cocuts, while also using some of our earlier observations about \(\neg \neg\)-stable h-propositions.
Lemma 6. Every cocut \(C\) is weakly \(\Pi^0_1\).
Proof. We define \(R_{a, n} := a + \frac{1}{n + 1} \in C\). Locatedness tells us that for all \(n\), \(a \notin C\) or \(R_{a, n}\). Proposition 22 tells us that \(a \in C\) if and only if \(\prod_{n : \mathbb{N}} R_{a, n}\). ◻
Lemma 7. Every weakly \(\Pi^0_1\) h-proposition is \(\neg \neg\)-stable.
Proof. We work internally in homotopy type theory. We assume we are given an element of \(\neg \neg X_y\) for some \(y : Y\). To show \(X_y\) we can equivalently prove \(\prod_{n : \mathbb{N}} R_{y, n}\). For any \(n : \mathbb{N}\) we have by assumption either \(R_{y, n}\) or \(\neg X_{y}\). The latter contradicts \(\neg \neg X_{y}\), and so we have \(R_{y, n}\). Since this is true for all \(n\), we deduce \(X_{y}\). ◻
Theorem 32. If \(1 \to \Omega_{\Pi^0_1}\) is a classifier for \(\Pi^0_1\) monomorphisms in our metatheory, then every weakly \(\Pi^0_1\) h-proposition, \(f : X \to Y\), is a homotopy pullback of \(\Delta(1) \to \Delta(\Omega_{\Pi^0_1})\) in cubical sets.
Proof. We need to check that every weakly \(\Pi^0_1\) h-proposition \(f : X \to Y\) is equivalent to one obtained by pulling back \(\Delta(1) \to \Delta(\Omega_{\Pi^0_1})\). First note that we may assume without loss of generality that \(f\) is a monomorphism, since by Lemma 7 it is equivalent to the double negation \(\sum_{y : Y} \neg \neg X_y \to Y\), which is a monomorphism by Lemma 4. In order to apply Theorem 14 we need to check that \(\Gamma(X) \to \Gamma(Y)\) is \(\Pi^0_1\). By applying Corollary 7 with \(X := \sum_{y : Y, n : \mathbb{N}} R_{y, n} + \neg X_{y}\) and \(Y := Y \times \mathbb{N}\), together with the definition of weakly \(\Pi^0_1\) h-proposition we have a section of \(\Gamma(R + \neg X) \to \Gamma (Y \times \mathbb{N})\). Since \(\Gamma\) preserves all limits and colimits and \(\mathbb{N}\) is discrete, this gives us a map \(g : \Gamma (Y) \times \mathbb{N}\to \Gamma(R) + \Gamma(\neg X)\). For each \(y \in \Gamma(Y)\) we can define a function \(g'_y : \mathbb{N}\to 2\) where \(g'_y(n) = 0\) when \(g(y, n) = \mathtt{inl}(z)\) for \(z \in \Gamma(R)\) and \(g'_y(n) = 1\) when \(g(y, n) = \mathtt{inr}(\ast)\). Using the term witnessing \(\prod_{y : Y} (X_y \leftrightarrow \prod_{n : \mathbb{N}} R_{y, n})\) we can show that each fibre \(\Gamma(X)_y\) is inhabited if and only if \(g'_y(n) = 0\) for all \(n\). Hence \(\Gamma(X) \to \Gamma(Y)\) is indeed \(\Pi^0_1\) and so we can apply Theorem 14. ◻
Remark 33. Since we were able to explicitly define binary sequences \(g'_y\) in the proof above, it might appear at first that we did not need the extensionality condition and could have used instead e.g. the map \(1 \to 2^\mathbb{N}\) pointing to the constantly zero sequence in place of the classifier \(1 \to \Omega_{\Pi^0_1}\). However, this would not work. The sequence \(g'_y\) depends on the choice of point \(y\), and so we could have different choices of sequence for each of two points joined by a path, whereas in order to get a well defined map to \(\Delta(\Omega_{\Pi^0_1})\) we need to assign the same element of \(\Omega_{\Pi^0_1}\) to both points. Note that when we defined such a map in Theorem 14 we made essential use of extensionality.
Corollary 34. Suppose we are given a classifier \(1 \to \Omega_{\Pi^0_1}\) for \(\Pi^0_1\) monomorphisms in our metatheory. Let \(U_n\) be a universe of small types. Then it holds in the interpretation of HoTT in cubical sets that every weakly \(\Pi^0_1\) h-proposition in \(U_n\) is equivalent to one belonging to \(\Delta(\Omega_{\Pi^0_1})\).
Proof. We apply Theorem 32 where \(Y\) is the type of all weakly \(\Pi^0_1\) h-propositions in \(U_n\) and \(X \to Y\) the projection map from inhabited weakly \(\Pi^0_1\) h-propositions in \(U_n\). ◻
Corollary 35. Assume that there is a classifier for all \(\Pi^0_1\) monomorphisms in our metatheory. Then there is a collection of all Dedekind real numbers in cubical sets.
Proof. Internally in HoTT we can think of \(\Delta(1) \to \Delta(\Omega_{\Pi^0_1})\) as a family of h-propositions, which by Theorem 32 includes all weakly \(\Pi^0_1\) h-propositions. We now work internally in HoTT, and define a subtype of \(\Delta(\Omega_{\Pi^0_1})^\mathbb{Q}\) consisting of those \(C : \mathbb{Q}\to \Delta(\Omega_{\Pi^0_1})\) which are cocuts. We need to check that it holds internally in HoTT that every cocut belongs to this collection. However, for every cocut \(C : \mathbb{Q}\to \mathbf{hProp}\), and every rational \(a : \mathbb{Q}\), \(C(a)\) is weakly \(\Pi^0_1\) by Lemma 6, and so \(C\) is indeed equal to one in this collection. ◻
In [19] Rathjen observes that since it is possible to define models of type theory with univalence in a constructive and predicative metatheory, the proof theoretic strength of type theory is unchanged by adding the univalence axiom. In particular, writing \(\mathbf{MLTT}^-\) for the theory obtained by removing \(W\)-types from Martin-Löf type theory, and \(\mathbf{UA}\) for the univalence axiom, the proof theoretic strength of \(\mathbf{MLTT}^- + \mathbf{UA}\) is the same as \(\mathbf{MLTT}^-\) [19]. From Corollary 35 we can see the same argument applies with the addition of the Dedekind reals. Namely, write \(\mathbb{R}_\mathbf{D}\) for the axiom that the Dedekind reals exist (at the first universe level, say). We then have the following result.
Corollary 36. \(\mathbf{MLTT}^- + \mathbf{UA} + \mathbb{R}_\mathbf{D}\) has the same strength as \(\mathbf{MLTT}^-\), which is the same as \(\mathbf{ATR}_0\). Its proof theoretic ordinal is \(\Gamma_0\).
In [20] an alternative definition of real number is given, based on the Cauchy reals, but using a higher inductive principle that ensures Cauchy completeness, which does not necessarily hold for the Cauchy real numbers in the absence of the axiom of countable choice. Write \(\mathbb{R}_{\mathbf{HIT}}\) for the axiom that the HIT reals, as defined in loc. cit., exist (at the first universe level, say). Although it is likely \(\mathbb{R}_{\mathbf{HIT}}\) can be constructed in cubical sets by the same methods as in [14], such a proof would require an infinitary inductive definition in the metatheory, which is not available in absolutely predicative systems such as \(\mathbf{MLTT}^-\). This suggests the following conjecture.
Conjecture 37. \(\mathbf{MLTT}^- + \mathbf{UA} + \mathbb{R}_{\mathbf{HIT}}\) has strictly greater proof theoretic strength than that of \(\mathbf{MLTT}^-\).
Note that in the presence of countable choice, the Cauchy real numbers are already Cauchy complete, and therefore satisfy the higher inductive principle for the higher inductive Cauchy reals. However, countable choice easily holds in many models of extensional type theory with propositional truncation, e.g. the regular locally cartesian closed category of sets within \(\mathbf{CZF} + \{\mathbf{wInacc}(n) \;|\; n > 0\} + \mathbf{RDC}\), as listed in [19]. Hence, if the conjecture above is true, it would provide a natural example of an axiom which raises the consistency strength of \(\mathbf{MLTT}^-\) when combined with the univalence axiom, while having no effect on the consistency strength of extensional type theory.
We can think of h-propositions that are double negation stable as those that are proof irrelevant in a strong sense. One way that this manifests is in the key idea we saw in Lemma 4: in cubical sets they are interpreted as monomorphisms, i.e. types where any two elements are strictly equal. We can therefore think of them as possessing no nondegenerate paths or homotopies, even up to strict equality. In particular we can obtain a classifier from the constant cubical set on the corresponding classifier in our metatheory.
When we construct cubical sets inside a realizability model, such as assemblies, we can additionally say that double negation stable h-propositions carry no computational information, in the sense of uniform maps of assemblies.
Although the class of double negation stable h-propositions is rather restricted, we saw two places where they can play a useful role. By defining Dedekind real numbers in terms of cocuts, we ensured that all of the computational information associated to a real number is contained within the terms witnessing boundedness and locatedness, with the underlying subset of \(\mathbb{Q}\) entirely proof irrelevant.
The second place we used double negation stable h-propositions was in our formulation of extended Church’s thesis. The domain of a partial function \(\mathbb{N}\rightharpoondown \mathbb{N}\) is a function \(D : \mathbb{N}\to \mathbf{hProp}\). We should expect the partial function to be a computable partial function when for each \(n : \mathbb{N}\), \(D(n)\) carries no computational information beyond \(n\) itself, which we can ensure by requiring that it is \(\neg \neg\)-stable. We made this precise through realizability, and gave an example of a model of HoTT where extended Church’s thesis holds.