3.10 When are propositions truncated?

At first glance, it may seem that the truncated versions of $+$ and $\mathrm{\Sigma }$ are actually closer to the informal mathematical meaning of “or” and “there exists” than the untruncated ones. Certainly, they are closer to the precise meaning of “or” and “there exists” in the first-order logic which underlies formal set theory, since the latter makes no attempt to remember any witnesses to the truth of propositions. However, it may come as a surprise to realize that the practice of informal mathematics is often more accurately described by the untruncated forms.

For example, consider a statement like “every prime number is either $2$ or odd.” The working mathematician feels no compunction about using this fact not only to prove theorems about prime numbers, but also to perform constructions on prime numbers, perhaps doing one thing in the case of $2$ and another in the case of an odd prime. The end result of the construction is not merely the truth of some statement, but a piece of data which may depend on the parity of the prime number. Thus, from a type-theoretic perspective, such a construction is naturally phrased using the induction principle for the coproduct type “$(p=2)+(p\text{ is odd})$”, not its propositional truncation.

Admittedly, this is not an ideal example, since “$p=2$” and “$p$ is odd” are mutually exclusive, so that $(p=2)+(p\text{ is odd})$ is in fact already a mere proposition and hence equivalent to its truncation (see http://planetmath.org/node/87851Exercise 3.7). More compelling examples come from the existential quantifier. It is not uncommon to prove a theorem of the form “there exists an $x$ such that …” and then refer later on to “the $x$ constructed in Theorem Y” (note the definite article). Moreover, when deriving further properties of this $x$, one may use phrases such as “by the construction of $x$ in the proof of Theorem Y”.

A very common example is “$A$ is isomorphic to $B$”, which strictly speaking means only that there exists some isomorphism between $A$ and $B$. But almost invariably, when proving such a statement, one exhibits a specific isomorphism or proves that some previously known map is an isomorphism, and it often matters later on what particular isomorphism was given.

Set-theoretically trained mathematicians often feel a twinge of guilt at such “abuses of language”. We may attempt to apologize for them, expunge them from final drafts, or weasel out of them with vague words like “canonical”. The problem is exacerbated by the fact that in formalized set theory, there is technically no way to “construct” objects at all — we can only prove that an object with certain properties exists. Untruncated logic in type theory thus captures some common practices of informal mathematics that the set theoretic reconstruction obscures. (This is similar to how the univalence axiom validates the common, but formally unjustified, practice of identifying isomorphic objects.)

On the other hand, sometimes truncated logic is essential. We have seen this in the statements of $\mathrm{𝖫𝖤𝖬}$ and $\mathrm{𝖠𝖢}$; some other examples will appear later on in the book. Thus, we are faced with the problem: when writing informal type theory, what should we mean by the words “or” and “there exists” (along with common synonyms such as “there is” and “we have”)?

A universal consensus may not be possible. Perhaps depending on the sort of mathematics being done, one convention or the other may be more useful — or, perhaps, the choice of convention may be irrelevant. In this case, a remark at the beginning of a mathematical paper may suffice to inform the reader of the linguistic conventions in use therein. However, even after one overall convention is chosen, the other sort of logic will usually arise at least occasionally, so we need a way to refer to it. More generally, one may consider replacing the propositional truncation with another operation on types that behaves similarly, such as the double negation operation $A\mapsto \mathrm{\neg }\mathrm{\neg }A$, or the $n$-truncations to be considered in http://planetmath.org/node/87580Chapter 7. As an experiment in exposition, in what follows we will occasionally use adverbs to denote the application of such “modalities” as propositional truncation.

For instance, if untruncated logic is the default convention, we may use the adverb merely to denote propositional truncation. Thus the phrase

“there merely exists an $x:A$ such that $P(x)$”

indicates the type $\parallel {\sum }_{(x:A)}P(x)\parallel$. Similarly, we will say that a type $A$ is merely inhabited to mean that its propositional truncation $\parallel A\parallel$ is inhabited (i.e. that we have an unnamed element of it). Note that this is a definition of the adverb “merely” as it is to be used in our informal mathematical English, in the same way that we define nouns like “group” and “ring”, and adjectives like “regular” and “normal”, to have precise mathematical meanings. We are not claiming that the dictionary definition of “merely” refers to propositional truncation; the choice of word is meant only to remind the mathematician reader that a mere proposition contains “merely” the information of a truth value and nothing more.

On the other hand, if truncated logic is the current default convention, we may use an adverb such as purely or constructively to indicate its absence, so that

“there purely exists an $x:A$ such that $P(x)$”

would denote the type ${\sum }_{(x:A)}P(x)$. We may also use “purely” or “actually” just to emphasize the absence of truncation, even when that is the default convention.

In this book we will continue using untruncated logic as the default convention, for a number of reasons.

1. We want to encourage the newcomer to experiment with it, rather than sticking to truncated logic simply because it is more familiar.

2. Using truncated logic as the default in type theory suffers from the same sort of “abuse of language” problems as set-theoretic foundations, which untruncated logic avoids. For instance, our definition of “$A\simeq B$” as the type of equivalences between $A$ and $B$, rather than its propositional truncation, means that to prove a theorem of the form “$A\simeq B$” is literally to construct a particular such equivalence. This specific equivalence can then be referred to later on.

3. We want to emphasize that the notion of “mere proposition” is not a fundamental part of type theory. As we will see in http://planetmath.org/node/87580Chapter 7, mere propositions are just the second rung on an infinite ladder, and there are also many other modalities not lying on this ladder at all.

4. Many statements that classically are mere propositions are no longer so in homotopy type theory. Of course, foremost among these is equality.

5. On the other hand, one of the most interesting observations of homotopy type theory is that a surprising number of types are automatically mere propositions, or can be slightly modified to become so, without the need for any truncation. (See Lemma 3.3.5 (http://planetmath.org/33merepropositions#Thmprelem4),http://planetmath.org/node/87577Chapter 4,http://planetmath.org/node/87580Chapter 7,http://planetmath.org/node/87583Chapter 9,http://planetmath.org/node/87584Chapter 10.) Thus, although these types contain no data beyond a truth value, we can nevertheless use them to construct untruncated objects, since there is no need to use the induction principle of propositional truncation. This useful fact is more clumsy to express if propositional truncation is applied to all statements by default.

6. Finally, truncations are not very useful for most of the mathematics we will be doing in this book, so it is simpler to notate them explicitly when they occur.

Title	3.10 When are propositions truncated?