Chapter 195Core route

Truncation Levels, Propositions, and Logic

Recall from definition 189.43 that a type is a mere proposition when any two of its elements are equal, and a set when each identity type is a mere proposition. Iterating this condition gives the truncation levels. Unit lies at the bottom, $2$ is a set but not a proposition, and a univalent universe is not a set.

The hierarchy of truncation levels

The hierarchy is generated from contractibility by iterating the passage to identity types.

Recall from definition 62.19 that $isContr (A) : = \sum_{a : A} \prod_{x : A} a =_{A} x$ ; its two components are the centre and the contraction. We keep this notation fixed throughout the truncation hierarchy.

For $1$ , the pair $(⋆, λ x . {refl}_{⋆})$ is a contraction because Unit- $η$ makes every $x$ judgmentally $⋆$ . By contrast $2$ is not contractible: a contraction would identify $tt$ and $ff$ , contradicting theorem 29.14.

Definition 66.2 — Truncation levels ¶

For each integer $n \geq - 2$ the predicate $is - n - type : U \to U$ is defined by recursion on $n$ : $\begin{aligned} is - (- 2) - type (X) & : = isContr (X), \\ is - (n + 1) - type (X) & : = \prod_{x, y : X} is - n - type (x =_{X} y) . \end{aligned}$ A type $X$ with $is - n - type (X)$ inhabited is a $n$ -type, also called an $n$ -truncated type.

Referenced from 10 locations

Unfolding once gives $\begin{aligned} is - - 1 - type (X) & = \prod_{x, y : X} isContr (x =_{X} y), \\ is - 0 - type (X) & = \prod_{x, y : X} is - - 1 - type (x =_{X} y) . \end{aligned}$ We call $(- 1)$ -types propositions and $0$ -types sets.

Remark 66.3 — Indexing ¶

The index $n$ in definition 66.2 is a numeral of the metatheory, so $is - n - type$ is a family of definitions, one per level, and statements “for all $n$ ” are proved by metatheoretic induction with base case $- 2$ . Equivalently, an internal treatment indexes levels by $k : N$ via $n = k - 2$ .

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Definition 66.4 — Propositions and sets ¶

For a type $A$ put $isProp (A) : = \prod_{x : A} \prod_{y : A} x =_{A} y, isSet (A) : = \prod_{x : A} \prod_{y : A} isProp (x =_{A} y) .$ A type with $isProp (A)$ inhabited is a mere proposition, meaning that every two elements are equal. A type with $isSet (A)$ inhabited is a set, meaning that each identity type is a mere proposition. Theorem 66.9 identifies propositions with $(- 1)$ -types and sets with $0$ -types.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Convention 195.4 — Theory signatures ¶

The hierarchy through closure under $Σ$ -types is developed in the intensional base of chapter 26–chapter 30. Write ${HoTT}_{0}$ for that base plus the univalence axiom of definition 65.6; this is the signature used whenever function extensionality or paths in a universe enter. Each theorem below is read in the weaker base unless its statement, proof, or nearest signature marker uses ${HoTT}_{0}$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

The proof that propositions are sets uses transport in the based path family, ${transport}_{p} (q) = q \cdot p$ . We record it with the three path-induction laws used alongside it.

Lemma 66.5 — Path algebra recollections ¶

Let $A$ be a type, $a, y, z : A$ , and $p : y =_{A} z$ .

For $q : a =_{A} y$ , transport in the family of based paths is concatenation: ${tr}_{p}^{z^{'} \mapsto a =_{A} z^{'}} (q) = q \cdot p$ .
$ap$ is functorial: ${ap}_{g \circ f} (p) = {ap}_{g} ({ap}_{f} (p))$ , ${ap}_{id} (p) = p$ , and ${ap}_{f} (p \cdot p^{'}) = {ap}_{f} (p) \cdot {ap}_{f} (p^{'})$ .
For families $B, C$ over $A$ and $b : B (y)$ , ${tr}_{p}^{x \mapsto B (x) + C (x)} (inl (b)) = inl ({tr}_{p}^{B} (b))$ , and dually for $inr$ .
The based path space $\sum_{x : A} a =_{A} x$ is contractible, with center $(a, refl)$ .

Referenced from 9 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.5 — Path algebra recollections

Proof. (1)–(3): path induction on $p$ ; after $p : = refl$ both sides are equal by the computation rules of $tr$ and $ap$ (chapter 30) and the unit laws of theorem 30.20. (4): the center is $(a, refl)$ ; given $(x, q)$ , path induction on $q$ reduces the required path $(a, refl) = (x, q)$ to $refl$ . ◻

Lemma 66.6 — Contractibility propagates to paths ¶

If $A$ is contractible, then $x =_{A} y$ is contractible for all $x, y : A$ .

Referenced from 5 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.6 — Contractibility propagates to paths

Proof. Let $a$ be the center with contraction $C$ . Take $C (x)^{- 1} \cdot C (y)$ as center of $x =_{A} y$ . For $p : x =_{A} y$ , path induction reduces the goal $C (x)^{- 1} \cdot C (x) = p$ to the case $p : = refl$ , which is the inverse law of theorem 30.20. ◻

Lemma 66.7 — Pointed propositions ¶

If $A$ is a proposition and $a : A$ , then $A$ is contractible; conversely every contractible type is an inhabited proposition.
If $P$ and $Q$ are propositions and there are maps $f : P \to Q$ and $g : Q \to P$ , then $P ≃ Q$ .
An inhabited proposition is equivalent to $1$ .

Referenced from 15 locations

Proof of Lemma 66.7 — Pointed propositions

Proof. (1) With $h : isProp (A)$ , the pair $(a, h (a))$ contracts $A$ ; conversely a contraction $C$ yields $h (x, y) : = C (x)^{- 1} \cdot C (y)$ . (2) The composite $g \circ f$ is homotopic to ${id}_{P}$ because $P$ is a proposition, and likewise $f \circ g \sim {id}_{Q}$ ; theorem 62.27 turns this quasi-inverse into an equivalence. (3) By (2) with $Q : = 1$ : the maps are $λ x . ⋆$ and the constant at the given point, and $1$ is a proposition since any two of its elements are equal to $⋆$ by the $η$ -rule (chapter 27). ◻

Lemma 66.8 — Propositions are sets ¶

If $A$ is a proposition, then $A$ is a set.

Referenced from 5 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.8 — Propositions are sets

Proof. Let $h : isProp (A)$ ; fix $x : A$ and put $g : = h (x) : \prod_{y : A} x =_{A} y$ . For $y, z : A$ and $p : y =_{A} z$ , dependent application (chapter 62) gives ${apd}_{g} (p) : {tr}_{p}^{z^{'} \mapsto x =_{A} z^{'}} (g (y)) = g (z)$ , and by lemma 66.5(1) the left-hand side is $g (y) \cdot p$ . Hence $g (y) \cdot p = g (z)$ , so $p = g (y)^{- 1} \cdot g (z)$ by the groupoid laws (theorem 30.20). The right-hand side does not depend on $p$ : any two $p, q : y =_{A} z$ are both equal to $g (y)^{- 1} \cdot g (z)$ , hence equal. ◻

Theorem 66.9 — The bottom levels ¶

A type $A$ is a $(- 1)$ -type if and only if it is a proposition, and a $0$ -type if and only if it is a set.

Referenced from 6 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.9 — The bottom levels

Proof. If $is - (- 1) - type (A)$ , each $x =_{A} y$ is contractible, and its center provides $isProp (A)$ . Conversely let $h : isProp (A)$ ; each $x =_{A} y$ is inhabited by $h (x, y)$ and is a proposition by lemma 66.8, hence contractible by lemma 66.7(1). The second claim follows by applying the first to each $x =_{A} y$ . ◻

Theorem 66.10 — Cumulativity ¶

For every $n \geq - 2$ : if $A$ is an $n$ -type, then $A$ is an $(n + 1)$ -type.

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.10 — Cumulativity

Proof. Induction on $n$ . Base case: a contractible type has contractible path types, i.e. is a $(- 1)$ -type (lemma 66.6). Inductive step: if $A$ is an $(n + 1)$ -type, each $x =_{A} y$ is an $n$ -type, hence an $(n + 1)$ -type by the inductive hypothesis, so $A$ is an $(n + 2)$ -type. ◻

Corollary 66.11 ¶

A proposition is an $n$ -type for every $n \geq - 1$ ; a set is an $n$ -type for every $n \geq 0$ ; and if $A$ is an $n$ -type, then $x =_{A} y$ is an $n$ -type for all $x, y : A$ .

Referenced from 5 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.11

Proof. Iterate theorem 66.10 from theorem 66.9. For the last claim: $A$ is an $(n + 1)$ -type, and unfold definition 66.2. ◻

Example 195.12 — First rungs ¶

$1$ is contractible, with center $⋆$ and contraction given by $1$ -induction into $x \mapsto (⋆ = x)$ . The type $0$ is a proposition by empty elimination but is not contractible, since a center would inhabit it. The type $2$ is a set (lemma 65.21) but not a proposition, because $tt = ff$ is empty. The path-space calculation of proposition 189.44 makes $N$ a set, and $0 \neq suc (0)$ shows it is not a proposition. Finally, univalence in ${HoTT}_{0}$ makes $U$ not a set (theorem 65.22). These examples do not imply that every type is $n$ -truncated for some finite $n$ ; no such bound is assumed.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Exercise 66.1 ¶

★☆☆ Write out the path-induction proofs of lemma 66.5(1)–(3), naming at each step the computation rule of $tr$ or $ap$ (chapter 30) being used.

Referenced from 3 locations

Exercise 66.2 ¶

★★☆ Show that the following are equivalent for a type $A$ : (i) $A$ is contractible; (ii) $A ≃ 1$ ; (iii) $A$ is an inhabited proposition.

Referenced from 3 locations

Exercise 66.3 ¶

★☆☆ A retraction is a map $r : X \to Y$ with a section $s : Y \to X$ and a homotopy $r \circ s \sim {id}_{Y}$ . Show that a retract of a contractible type is contractible.

Referenced from 3 locations

Exercise 66.4 ¶

★☆☆ Show that $is - (- 2) - type$ cannot be weakened: exhibit a type all of whose identity types are contractible that is not itself contractible, and explain why the hierarchy is nevertheless not extended downward.

Referenced from 3 locations

Closure properties

If $r : X \to Y$ has a section $s$ , then paths in $Y$ are retracts of paths in $X$ . Hence the truncation level of $X$ descends to $Y$ .

Theorem 66.13 — Closure under retracts ¶

Let $r : X \to Y$ have a section $s : Y \to X$ with $ϵ : r \circ s \sim {id}_{Y}$ . If $X$ is an $n$ -type ( $n \geq - 2$ ), then so is $Y$ .

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.13 — Closure under retracts

Proof. Induction on $n$ . Base case ( $n = - 2$ ): let $x_{0}$ be the center of $X$ with contraction $C$ ; then $r (x_{0})$ is a center for $Y$ , since for $y : Y$ we have ${ap}_{r} (C (s (y))) \cdot ϵ (y) : r (x_{0}) =_{Y} y$ .

Inductive step: assume the claim for $n$ , let $X$ be an $(n + 1)$ -type and $y, y^{'} : Y$ ; we show $y =_{Y} y^{'}$ is an $n$ -type by exhibiting it as a retract of the $n$ -type $s (y) =_{X} s (y^{'})$ . The section is ${ap}_{s}$ ; the retraction is $t (q) : = ϵ (y)^{- 1} \cdot {ap}_{r} (q) \cdot ϵ (y^{'})$ . For $p : y =_{Y} y^{'}$ , naturality of $ϵ$ (theorem 62.13) at $p$ gives $ϵ (y) \cdot p = {ap}_{r \circ s} (p) \cdot ϵ (y^{'})$ , and ${ap}_{r \circ s} (p) = {ap}_{r} ({ap}_{s} (p))$ by lemma 66.5(2); whiskering by $ϵ (y)^{- 1}$ and the groupoid laws (theorem 30.20) then yield $t ({ap}_{s} (p)) = p$ . Conclude by the inductive hypothesis. ◻

Corollary 66.14 — Invariance under equivalence ¶

If $X ≃ Y$ and $X$ is an $n$ -type, then $Y$ is an $n$ -type.

Referenced from 9 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.14 — Invariance under equivalence

Proof. By proposition 62.24, an equivalence $f : X \to Y$ has a quasi-inverse $g : Y \to X$ with $f \circ g \sim {id}_{Y}$ ; thus $Y$ is a retract of $X$ . Apply theorem 66.13. ◻

Theorem 66.15 — Closure under Σ ¶

Let $n \geq - 2$ , let $A$ be an $n$ -type, and let $B$ be a family over $A$ with each $B (a)$ an $n$ -type. Then $\sum_{x : A} B (x)$ is an $n$ -type.

Referenced from 7 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.15 — Closure under Σ

Proof. Induction on $n$ . Base case: let $a_{0}$ center $A$ and $b_{0}$ center $B (a_{0})$ ; given $(a, b)$ , the contraction of $A$ gives $p : a_{0} =_{A} a$ , and ${tr}_{p}^{B} (b_{0}) = b$ holds because any two elements of the contractible type $B (a)$ are equal (lemma 66.7(1)); by theorem 62.30 these two data assemble to $(a_{0}, b_{0}) =_{} (a, b)$ , so $(a_{0}, b_{0})$ is a center.

Inductive step: for $(a_{1}, b_{1}), (a_{2}, b_{2})$ , theorem 62.30 gives $((a_{1}, b_{1}) =_{} (a_{2}, b_{2})) ≃ \sum_{p : a_{1} =_{A} a_{2}} {tr}_{p}^{B} (b_{1}) =_{B (a_{2})} b_{2},$ and the right-hand side is an $n$ -type by the inductive hypothesis (base $a_{1} =_{A} a_{2}$ and fibers both $n$ -types); conclude by corollary 66.14. ◻

From this point to the propositional-truncation signature marker, the ambient theory is ${HoTT}_{0}$ . The first additional consequence used is function extensionality, derived from univalence in theorem 65.18.

Theorem 66.16 — Closure under Π ¶

Let $n \geq - 2$ and let $B$ be a family over $A$ with each $B (a)$ an $n$ -type. Then $\prod_{x : A} B (x)$ is an $n$ -type. In particular $A \to B$ is an $n$ -type whenever $B$ is.

Referenced from 14 locations

Proof of Theorem 66.16 — Closure under Π

Proof. Induction on $n$ . Base case: $f_{0} : = λ x . c (x)$ , where $c (x)$ is the center of $B (x)$ , is a center: for $g$ , function extensionality (theorem 65.18) turns the pointwise contraction paths $c (x) = g (x)$ into $f_{0} = g$ . Inductive step: for $f, g : \prod_{x : A} B (x)$ , by theorem 65.18 the map $happly$ is an equivalence $(f =_{} g) ≃ \prod_{x : A} f (x) =_{B (x)} g (x)$ ; the right-hand side is an $n$ -type by the inductive hypothesis, so conclude by corollary 66.14. ◻

Definition 66.17 — Embedding ¶

A map $f : A \to B$ is an embedding if ${ap}_{f} : (x =_{A} x^{'}) \to (f (x) =_{B} f (x^{'}))$ is an equivalence for all $x, x^{'} : A$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proposition 66.18 — Descent along embeddings ¶

If $f : A \to B$ is an embedding and $B$ is an $n$ -type with $n \geq - 1$ , then $A$ is an $n$ -type.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proof of Proposition 66.18 — Descent along embeddings

Proof. For $x, x^{'} : A$ the type $x =_{A} x^{'}$ is equivalent to $f (x) =_{B} f (x^{'})$ , which is an $(n - 1)$ -type by definition 66.2; apply corollary 66.14. (The claim fails at $n = - 2$ : $0 \to 1$ is an embedding.) ◻

Lemma 66.19 — Contractible fibers project away ¶

If $C$ is a family over $A$ with each $C (a)$ contractible, then ${pr}_{1} : \sum_{x : A} C (x) \to A$ is an equivalence.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.19 — Contractible fibers project away

Proof. A quasi-inverse is $a \mapsto (a, c (a))$ with $c (a)$ the center of $C (a)$ . One composite is ${pr}_{1} (a, c (a)) \equiv a$ ; for the other, $(x, u)$ and $(x, c (x))$ are identified by theorem 62.30 via $refl$ and the contraction of $C (x)$ . Conclude by theorem 62.27. ◻

Lemma 66.20 — Paths in subtypes ¶

Let $P$ be a family of propositions over $A$ and $u, v : \sum_{x : A} P (x)$ . Then ${ap}_{{pr}_{1}}$ is an equivalence $(u =_{} v) ≃ ({pr}_{1} (u) =_{A} {pr}_{1} (v))$ ; in particular ${pr}_{1}$ is an embedding.

Referenced from 8 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.20 — Paths in subtypes

Proof. By theorem 62.30, $(u =_{} v) ≃ \sum_{p : {pr}_{1} u =_{A} {pr}_{1} v} {tr}_{p}^{P} ({pr}_{2} u) =_{P ({pr}_{1} v)} {pr}_{2} v$ . Each fiber is a path type in the proposition $P ({pr}_{1} v)$ , hence an inhabited proposition (lemma 66.8), hence contractible (lemma 66.7(1)); apply lemma 66.19. That the composite equivalence is ${ap}_{{pr}_{1}}$ is a path induction. ◻

Lemma 66.21 ¶

$isContr (A)$ is a proposition, for every type $A$ .

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.21

Proof. Let $(a, C), (a^{'}, C^{'}) : isContr (A)$ . By theorem 62.30 it suffices to give $p : = C (a^{'}) : a =_{A} a^{'}$ and a path ${tr}_{p} (C) = C^{'}$ in $\prod_{x : A} a^{'} =_{A} x$ . Since $A$ is contractible, each $a^{'} =_{A} x$ is contractible (lemma 66.6), hence a proposition; by theorem 66.16 (level $- 1$ ) the $Π$ -type is a proposition, so any two of its elements are equal. ◻

Theorem 66.22 — Being truncated is a proposition ¶

For every $n \geq - 2$ and every type $X$ , the type $is - n - type (X)$ is a proposition. In particular $isProp (X)$ and $isSet (X)$ are propositions.

Referenced from 6 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.22 — Being truncated is a proposition

Proof. Induction on $n$ ; the base case is lemma 66.21, and the inductive step is theorem 66.16 at level $- 1$ applied twice to $\prod_{x : X} \prod_{y : X} is - n - type (x =_{X} y)$ .

For the named bottom levels, let $h, g : isProp (X)$ . Since a proposition is a set (lemma 66.8), $h (x, y) = g (x, y)$ ; function extensionality in $x$ and $y$ gives $h = g$ . For $isSet (X)$ , apply this pointwise equality one dimension higher to its two path-family witnesses and then use function extensionality twice. Thus $isSet (X)$ is a proposition. The mutual implications of theorem 66.9 are therefore equivalences by lemma 66.7(2). ◻

Corollary 66.23 — Being an equivalence is a proposition ¶

For every $f : A \to B$ , the type $isEquiv (f) \equiv \prod_{b : B} isContr ({fib}_{f} (b))$ of definition 62.21 is a proposition. Consequently $A ≃ B \equiv \sum_{f : A \to B} isEquiv (f)$ has the level of its function part: two equivalences are equal as soon as their underlying functions are.

Referenced from 7 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.23 — Being an equivalence is a proposition

Proof. Theorem 66.16 at level $- 1$ with lemma 66.21; the final claim is lemma 66.20. ◻

Definition 66.24 ¶

For $n \geq - 2$ put $n - {Type}_{U} : = \sum_{X : U} is - n - type (X)$ , with ${Prop}_{U} : = (- 1) - {Type}_{U}$ and ${Set}_{U} : = 0 - {Type}_{U}$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Theorem 66.25 — The type of n-types ¶

$n - {Type}_{U}$ is an $(n + 1)$ -type.

Referenced from 4 locations

Proof of Theorem 66.25 — The type of n-types

Proof. Let $(X, p), (X^{'}, p^{'}) : n - {Type}_{U}$ . The family $is - n - type$ consists of propositions (theorem 66.22), hence $((X, p) =_{} (X^{'}, p^{'})) \overset{l e m m a 66.20}{≃} (X =_{U} X^{'}) \overset{d e f i n i t i o n 65.6}{≃} (X ≃ X^{'}),$ so it suffices that $X ≃ X^{'}$ is an $n$ -type. For $n \geq - 1$ : $X \to X^{'}$ is an $n$ -type (theorem 66.16) and each $isEquiv (f)$ is a proposition (corollary 66.23), hence an $n$ -type (corollary 66.11); apply theorem 66.15. For $n = - 2$ : both types are contractible, so $X \to X^{'}$ is contractible and $X ≃ X^{'}$ is an inhabited proposition (inhabited via $X ≃ 1 ≃ X^{'}$ , lemma 66.7(3)), hence contractible. ◻

Lemma 195.26 — Dependent sum over a contractible base ¶

If $A$ is contractible with center $a_{0}$ and $D : A \to U$ , then $\sum_{x : A} D (x) ≃ D (a_{0}) .$

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 195.26 — Dependent sum over a contractible base

Proof. Let $c : \prod_{x : A} a_{0} =_{A} x$ be the contraction. Put $Φ (x, d) : = {tr}_{c (x)^{- 1}}^{D} (d), Ψ (d) : = (a_{0}, d) .$ The type $a_{0} =_{A} a_{0}$ is contractible by lemma 66.6, so $c (a_{0}) = {refl}_{a_{0}}$ . Functoriality of transport then gives $Φ (Ψ (d)) = d$ . For the other composite, the base component of a path from $Ψ (Φ (x, d))$ to $(x, d)$ is $c (x)$ . Its fiber component is ${tr}_{c (x)}^{D} ({tr}_{c (x)^{- 1}}^{D} (d)) \overset{l e m m a 62.7 (i)}{=} {tr}_{c (x)^{- 1} \cdot c (x)}^{D} (d) \overset{p r o p o s i t i o n 62.2 (i i)}{=} d .$ By theorem 62.30, the pair consisting of the base path $c (x)$ and this fiber path gives $Ψ (Φ (x, d)) = (x, d)$ . Theorem 62.27 turns these two homotopies into the displayed equivalence. ◻

Exercise 66.5 ¶

★★☆ Reconstruct lemma 195.26. Show explicitly why the fiber component of the second round trip must transport first along $c (x)^{- 1}$ and then along $c (x)$ .

Referenced from 3 locations

Exercise 66.6 ¶

★★☆ Deduce from theorem 66.15 that $A \times B$ is an $n$ -type when $A$ and $B$ are, and give a direct proof for $n = 0$ using theorem 62.30.

Referenced from 3 locations

Exercise 66.7 ¶

★★☆ Using the characterization of paths in coproducts (theorem 62.35), show that $A + B$ is an $n$ -type whenever $A$ and $B$ are and $n \geq 0$ . Show that the claim fails at $n = - 1$ .

Referenced from 3 locations

Exercise 66.8 ¶

★☆☆ Show directly (without theorem 66.13) that a retract of a proposition is a proposition.

Referenced from 3 locations

Exercise 66.9 ¶

★★☆ Show that if $A$ and $B$ are sets, then $A ≃ B$ is a set.

Referenced from 3 locations

Sets, axiom K, and Hedberg’s theorem

Sets are the types for which identity proofs are unique; this section characterizes them by Streicher’s axiom K and proves Hedberg’s theorem: decidable equality forces a type to be a set.

Theorem 66.26 — UIP and K ¶

A type $X$ is a set if and only if it satisfies axiom K: $\prod_{x : X} \prod_{p : x =_{X} x} p =_{} refl .$

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.26 — UIP and K

Proof. K is the instance $q : = refl$ of $isSet$ . Conversely, given K and $p, q : x =_{X} y$ , path induction on $q$ reduces the goal $p = q$ to $p^{'} = refl$ for $p^{'} : x =_{X} x$ , which is K. In the exact groupoid-model fragment of corollary 54.36, neither principle is derivable for general $X$ . ◻

The tempting direct proof of path uniqueness case-splits on a decision $d (x, y)$ . Its positive branch gives a path $r : x = y$ , but not the required identifications of arbitrary $p, q : x = y$ with $r$ : $p, q : x = y, d (x, y) \equiv inl (r) ⊬ p = q .$ The negative branch is impossible when a path is given, but that does not repair the positive branch. The collapse lemma turns the decision into a weakly constant family by sending every input path to the same chosen $r$ .

Lemma 66.27 — Collapse lemma ¶

Suppose $X$ carries a family of weakly constant endomaps of its path types: maps $f_{x, y} : (x =_{X} y) \to (x =_{X} y)$ together with $κ_{x, y} : \prod_{p : x =_{X} y} \prod_{q : x =_{X} y} f_{x, y} (p) =_{} f_{x, y} (q)$ for all $x, y : X$ . Then $X$ is a set.

Referenced from 8 locations

Proof of Lemma 66.27 — Collapse lemma

Proof. First, every $p : x =_{X} y$ satisfies $p = f_{x, x} (refl)^{- 1} \cdot f_{x, y} (p) .$ Indeed, by path induction on $p$ it suffices to check $refl = f_{x, x} (refl)^{- 1} \cdot f_{x, x} (refl)$ , which is the inverse law of theorem 30.20. Now for $p, q : x =_{X} y$ , (66.1) and $ap$ of $r \mapsto f_{x, x} (refl)^{- 1} \cdot r$ applied to $κ_{x, y} (p, q)$ give $\begin{aligned} p & \overset{(66.1)}{=} f_{x, x} (refl)^{- 1} \cdot f_{x, y} (p) \\ \overset{ap a p p l i e d t o κ_{x, y} (p, q)}{=} f_{x, x} (refl)^{- 1} \cdot f_{x, y} (q) \\ \overset{(66.1), b a c k w a r d s}{=} q . \end{aligned}$ ◻

Definition 66.28 — Decidable equality ¶

A type $X$ has decidable equality if $\prod_{x : X} \prod_{y : X} (x =_{X} y) + \neg (x =_{X} y)$ is inhabited, where $\neg A : = A \to 0$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Theorem 66.29 — Hedberg ¶

If $X$ has decidable equality, then $X$ is a set.

Referenced from 7 locations

Proof of Theorem 66.29 — Hedberg

Proof. Let $d$ decide equality. Fix $x, y : X$ and define $E_{x, y} : = x =_{X} y$ . By coproduct recursion, define $\begin{aligned} g & : (E_{x, y} + \neg E_{x, y}) \to E_{x, y} \to E_{x, y}, \\ g (inl (r)) & : = λ p . r, \\ g (inr (w)) & : = λ p . {rec}_{0} (w (p)) . \end{aligned}$ Put $f_{x, y} : = g (d (x, y))$ . Each $g (c)$ is weakly constant, by coproduct induction on $c$ : in the case $inl (r)$ both values are $r$ , so $refl$ suffices; in the case $inr (w)$ , for given $p, q$ the element $w (p) : 0$ yields ${rec}_{0} (w (p)) : g (c) (p) =_{} g (c) (q)$ . Hence $f_{x, y}$ is weakly constant for all $x, y$ , and lemma 66.27 applies. ◻

Corollary 66.30 ¶

$N$ and $2$ are sets.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.30

Proof. Both have decidable equality: for $2$ by a four-way case analysis using theorem 29.14; for $N$ by double induction, using that $0 \neq suc (n)$ and that $suc$ is injective — both consequences of the path-space computation for $N$ (theorem 62.39). Its code family is $1$ when both numerals are zero, $0$ when exactly one is zero, and the code for $(m, n)$ at $(suc (m), suc (n))$ ; induction decides whether the code is inhabited. Transporting that decision across theorem 62.39 decides each path type. Apply theorem 66.29. ◻

Proposition 66.31 — Separated types are sets ¶

If $\neg \neg (x =_{X} y) \to (x =_{X} y)$ for all $x, y : X$ , then $X$ is a set.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proof of Proposition 66.31 — Separated types are sets

Proof. Let $s$ witness the hypothesis. Since $0$ is a proposition, each $\neg \neg (x =_{X} y)$ is a proposition by theorem 66.16 (level $- 1$ ; here $funext$ is used). Put $f_{x, y} (p) : = s (x, y, λ k . k (p))$ . For $p, q$ , the arguments $λ k . k (p)$ and $λ k . k (q)$ are equal in the proposition $\neg \neg (x =_{X} y)$ , so $ap$ of $s (x, y)$ makes $f_{x, y}$ weakly constant. Apply lemma 66.27. ◻

Exercise 66.10 ¶

★★☆ Construct the decision procedure $d : \prod_{m : N} \prod_{n : N} (m =_{N} n) + \neg (m =_{N} n)$ by double induction, deriving $0 \neq suc (n)$ and injectivity of $suc$ from theorem 62.39.

Referenced from 3 locations

Exercise 66.11 ¶

★☆☆ Write out the path induction in the proof of theorem 66.26 as an application of $J$ (definition 30.1), displaying the motive.

Referenced from 3 locations

Propositional truncation

$‖ A ‖$ is a proposition receiving a map $A \to ‖ A ‖$ , and every map from $A$ to a proposition factors through it.

Definition 66.33 — Propositional truncation ¶

The theory is extended by the type former $‖ A ‖$ with the rules below (premises compressed per convention 26.14; congruence and substitution rules as in definition 26.22).

Γ ⊢ A type

Γ ⊢ ‖ A ‖ type

Trunc-F

Γ ⊢ a : A

Γ ⊢ | a | : ‖ A ‖

Trunc-I

Γ ⊢ u : ‖ A ‖

Γ ⊢ v : ‖ A ‖

Γ ⊢ sq (u, v) : u =_{‖ A ‖} v

Trunc-Sq

Γ, t : ‖ A ‖ ⊢ C type

Γ ⊢ w : \prod_{t : ‖ A ‖} isProp (C)

Γ, x : A ⊢ c : C [| x | / t]

Γ ⊢ u : ‖ A ‖

Γ ⊢ {ind}_{‖ A ‖} (w, x . c, u) : C [u / t]

Trunc-E

Γ ⊢ a : A

Γ ⊢ {ind}_{‖ A ‖} (w, x . c, | a |) \equiv c [a / x] : C [| a | / t]

Trunc-C

In Trunc-E, $C$ is a family over $‖ A ‖$ and $w (t) : isProp (C (t))$ proves that each target fiber is a proposition. (Trunc-C carries the premises of Trunc-E.) The resulting signature is denoted ${HoTT}_{0} + ‖ - ‖$ : it contains exactly ${HoTT}_{0}$ and these five truncation rules.

Referenced from 7 locations

Remark 66.34 — A higher inductive type ¶

$sq (u, v) : u = v$ is a path constructor. To eliminate into a family of propositions, it is enough to specify the point case: any two candidate images of $sq (u, v)$ are equal because the target fiber is a proposition. Extensional truncation (definition 35.18) instead makes proof irrelevance judgmental; the present path is propositional.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Lemma 66.35 ¶

$‖ A ‖$ is a proposition, and if $A$ is a proposition, then $| - | : A \to ‖ A ‖$ is an equivalence.

Referenced from 5 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.35

Proof. $λ u . λ v . sq (u, v) : isProp (‖ A ‖)$ . If $A$ is a proposition, define $r : ‖ A ‖ \to A$ by $r (| a |) : = a$ using Trunc-E with the constant family $C : = A$ ; the rule applies because $A$ is a proposition. Conclude by lemma 66.7(2). ◻

Convention 66.36 — Untruncation ¶

When the goal of a proof is a proposition and a hypothesis $u : ‖ A ‖$ is available, we permit ourselves to say “we may assume $a : A$ ”: formally, the goal is obtained by Trunc-E applied to $u$ , the propositionhood witness of the goal, and the proof carried out under the assumption $a : A$ . Each use cites this convention.

Referenced from 9 locations

Truncation Levels, Propositions, and Logic

Theorem 66.37 — Universal property ¶

For every proposition $B$ , precomposition with $| - |$ is an equivalence $(‖ A ‖ \to B) ≃ (A \to B) .$

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.37 — Universal property

Proof. Both sides are propositions (theorem 66.16 at level $- 1$ ), and maps exist in both directions: precomposition, and $g \mapsto {rec}_{‖ A ‖} (g)$ by Trunc-E with constant family $B$ . Apply lemma 66.7(2). ◻

Example 195.38 — Truncation forgets, irreversibly ¶

$‖ 2 ‖$ is contractible ( $| tt |$ inhabits it; apply lemma 66.7(1)). There is no $g : ‖ 2 ‖ \to 2$ with $\prod_{x : 2} g (| x |) =_{2} x$ : from such a $g$ , $tt \overset{\sec_{tt}}{=} g (| tt |) \overset{{ap}_{g} (sq (| tt |, | ff |))}{=} g (| ff |) \overset{\sec_{ff}}{=} ff$ contradicting theorem 29.14. The data discarded by $| - |$ cannot be recovered by any function, even though $‖ 2 ‖$ is “true”.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Exercise 66.13 ¶

★★☆ Construct $‖ f ‖ : ‖ A ‖ \to ‖ B ‖$ from $f : A \to B$ , show functoriality up to identity, and show $‖ A \times B ‖ ≃ ‖ A ‖ \times ‖ B ‖$ .

Referenced from 3 locations

Exercise 66.14 ¶

★☆☆ Show $‖ ‖ A ‖ ‖ ≃ ‖ A ‖$ and $‖ 1 ‖ ≃ 1$ .

Referenced from 3 locations

Exercise 66.15 ¶

★★☆ State and prove the dependent universal property: for a family of propositions $Q$ over $‖ A ‖$ , precomposition $(\prod_{t : ‖ A ‖} Q (t)) \to (\prod_{a : A} Q (| a |))$ is an equivalence.

Referenced from 3 locations

Exercise 66.12 ¶

★★☆ Show that if $X$ merely has decidable equality, i.e. $\prod_{x, y : X} ‖ (x =_{X} y) + \neg (x =_{X} y) ‖$ , then $X$ is still a set. Hint: weak constancy is a proposition, so convention 66.36 applies before lemma 66.27.

Referenced from 3 locations

The logic of mere propositions

A logical connective must return a proposition. Products and function types preserve propositionhood, but $P + Q$ and $\sum_{x} P (x)$ need not; we therefore define disjunction and existence by truncating those two types.

Definition 66.39 — Logical translation ¶

For propositions $P, Q$ and a family of propositions $P (x)$ over $A$ ( $A$ arbitrary), define:

formula	translation	truncated?
$⊤$	$1$	no
$⊥$	$0$	no
$P \land Q$	$P \times Q$	no
$P \Rightarrow Q$	$P \to Q$	no
$P \Leftrightarrow Q$	$(P \to Q) \times (Q \to P)$	no
$\neg P$	$P \to 0$	no
$\forall x : A . P (x)$	$\prod_{x : A} P (x)$	no
$\exists x : A . P (x)$	$‖ \sum_{x : A} P (x) ‖$	yes
$P \lor Q$	$‖ P + Q ‖$	yes

Each right-hand side is a proposition: the untruncated rows by theorem 66.16, theorem 66.15 at level $- 1$ and example 195.12, the last two by lemma 66.35.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Remark 66.40 — Σ versus ¶

The untruncated $Σ$ and the truncated $\exists$ answer different questions and must be kept apart:

	$\sum_{x : A} P (x)$	$\exists x : A . P (x)$
kind	structure	property
witness	extracted by ${pr}_{1}$	available only via convention 66.36
eliminates into	arbitrary types	propositions only
“choice”	a theorem (example 195.41)	an axiom (definition 66.46)
proof relevance	inhabitants may differ	any two inhabitants equal

Case analysis on $\exists$ or $\lor$ is available exactly when the goal is a proposition (convention 66.36); this is the formal content of the informal phrase “there exists, but no particular witness is given”.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Example 195.41 — Untruncated ``choice'' is a theorem ¶

For families $A$ over $X$ and $P$ over $\sum_{x : X} A (x)$ , put $G : = \prod_{x : X} A (x)$ , and for an input $F$ put $g_{F} : = λ x . {pr}_{1} (F x)$ and $p_{F} : = λ x . {pr}_{2} (F x)$ . The term $λ F . (g_{F}, p_{F}) : (\prod_{x : X} \sum_{a : A (x)} P (x, a)) \to \sum_{g : G} \prod_{x : X} P (x, g x)$ re-associates data; nothing is chosen (cf. the discussion in chapter 35). The axiom of choice proper concerns the truncated existential.

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Definition 66.42 — Excluded middle ¶

Relative to a universe $U$ : $LEM : = \prod_{A : U} (isProp (A) \to A + \neg A), {LEM}_{\infty} : = \prod_{A : U} A + \neg A .$

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Theorem 66.43 — Univalence refutes untruncated excluded middle ¶

Already in ${HoTT}_{0}$ , $\neg {LEM}_{\infty}$ .

Referenced from 6 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.43 — Univalence refutes untruncated excluded middle

Proof. Suppose $f : \prod_{A : U} A + \neg A$ . Let $e : 2 ≃ 2$ be the swap equivalence, $e (tt) : = ff$ , $e (ff) : = tt$ (its own quasi-inverse by $2$ -induction, hence an equivalence by theorem 62.27), and $p : = ua (e) : 2 =_{U} 2$ . Dependent application gives ${apd}_{f} (p) : {tr}_{p}^{A \mapsto A + \neg A} (f (2)) = f (2) .$ We refute both cases of $c : = f (2) : 2 + \neg 2$ by coproduct induction, with motive $c^{'} \mapsto ({tr}_{p} (c^{'}) = c^{'}) \to 0$ . Case $inr (w)$ : already $w (tt) : 0$ . Case $inl (x)$ : by lemma 66.5(3) and the computation of transport along $ua$ (theorem 65.9), ${tr}_{p} (inl (x)) = inl ({tr}_{p}^{A \mapsto A} (x)) = inl (e (x))$ , so the hypothesis yields $inl (e (x)) = inl (x)$ , whence $e (x) = x$ by the path characterization of coproducts (theorem 62.37). But $e$ has no fixed point: $2$ -induction on $x$ reduces this to $ff \neq tt$ and $tt \neq ff$ (theorem 29.14). ◻

Remark 66.32 ¶

The global law ${LEM}_{\infty}$ would decide every path type and hence, by theorem 66.29, make every type a set. Univalence refutes that law by theorem 66.43. The proposition-restricted law $LEM$ gives only merely decidable equality for an arbitrary type and therefore does not provide the weakly constant endomap required by lemma 66.27.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Exercise 66.16 ¶

★★☆ Show $\neg \prod_{A : U} (‖ A ‖ \to A)$ . Apply a hypothetical function at $2$ and transport it along the universe loop $ua (e_{swap})$ , where $e_{swap}$ exchanges $tt$ and $ff$ , using the naturality calculation in theorem 66.43 to obtain a fixed point of Boolean swap.

Referenced from 3 locations

Corollary 66.44 — No global double negation ¶

$\neg \prod_{A : U} (\neg \neg A \to A)$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.44 — No global double negation

Proof. Given $h$ of the displayed type, $λ A . h (A + \neg A) (k_{A})$ inhabits ${LEM}_{\infty}$ , where $k_{A} : = λ n . n (inr (λ a . n (inl (a)))) : \neg \neg (A + \neg A)$ ; contradict theorem 66.43. ◻

Remark 66.45 — Consistency status ¶

The simplicial-set model validates univalence together with the proposition-restricted $LEM$ of definition 66.42, while other models refute that axiom. Thus it is consistent relative to the model assumptions and is not derivable from the preceding rules [Uni13][AG26].

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Definition 66.46 — Axiom of choice ¶

Let $X$ be a set, $A$ a family over $X$ with each $A (x)$ a set, and $P$ a family of propositions over pairs $x : X$ , $a : A (x)$ . The axiom of choice $AC$ asserts, for all such data: $(\prod_{x : X} ‖ \sum_{a : A (x)} P (x, a) ‖) \to ‖ \sum_{g : \prod_{x : X} A (x)} \prod_{x : X} P (x, g x) ‖ .$

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Lemma 66.47 — Equivalent family form ¶

$AC$ is equivalent to: for every set $X$ and family $Y$ of sets over $X$ , $(\prod_{x : X} ‖ Y (x) ‖) \to ‖ \prod_{x : X} Y (x) ‖ .$

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.47 — Equivalent family form

Proof. Both statements are propositions, so logical equivalence suffices (lemma 66.7(2)). The family form is the instance $P : = λ x . λ a . 1$ of $AC$ up to the equivalence $\sum_{a : A (x)} 1 ≃ A (x)$ . Conversely put $Y (x) : = \sum_{a : A (x)} P (x, a)$ . This is a set by theorem 66.15, so the family form gives $‖ \prod_{x : X} Y (x) ‖$ . Propositional-truncation elimination into the desired truncated conclusion applies; a section $s : \prod_{x : X} Y (x)$ is sent to $| (λ x . {pr}_{1} (s (x)), λ x . {pr}_{2} (s (x))) | .$ These maps prove both implications and hence the equivalence. ◻

Remark 66.48 ¶

The simplicial-set model validates univalence together with $AC$ , while other models refute choice; hence $AC$ is relatively consistent and is not derivable [Uni13]. The hypothesis that $X$ be a set is essential by theorem 66.50.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Let $X : = \sum_{A : U} ‖ 2 = A ‖$ , the connected type of two-element types. Its loop corresponding to Boolean swap witnesses the failure of higher choice and the non-propositionality of quasi-inverses.

Lemma 66.49 — The type of two-element types ¶

Let $X : = \sum_{A : U} ‖ 2 =_{U} A ‖$ (a type in the next universe, definition 29.1) and $x_{0} : = (2, | refl |)$ . Then:

$X$ is connected: $\prod_{x : X} ‖ x_{0} =_{X} x ‖$ ;
$(x_{0} =_{X} x_{0}) ≃ (2 ≃ 2)$ , and this equivalence sends $refl$ to ${id}_{2}$ ;
each $x =_{X} y$ is a set (so $X$ is a $1$ -type);
$X$ is not a set.

Referenced from 11 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.49 — The type of two-element types

Proof. (1) Given $(A, u) : X$ , the goal is a proposition, so by convention 66.36 assume $p : 2 =_{U} A$ ; then lemma 66.20 (the second components live in propositions, lemma 66.35) turns $p$ into $x_{0} =_{X} (A, u)$ , and $| - |$ concludes.

(2) By lemma 66.20 and univalence (definition 65.6), $(x_{0} =_{X} x_{0}) ≃ (2 =_{U} 2) ≃ (2 ≃ 2)$ ; the composite is $r \mapsto idtoeqv ({ap}_{{pr}_{1}} (r))$ and sends $refl$ to ${id}_{2}$ by the computation rule of $idtoeqv$ .

(3) For $(A, u), (B, v) : X$ the path type is equivalent to $A ≃ B$ as in (2). Being a set is a proposition (theorem 66.22), so by convention 66.36 we may assume $2 = A$ and $2 = B$ ; then $A$ and $B$ are sets (corollary 66.30, corollary 66.14), $A \to B$ is a set (theorem 66.16), and $A ≃ B$ is a set by theorem 66.15, since $isEquiv$ is proposition-valued (corollary 66.23). Conclude by corollary 66.14.

(4) Let $q : x_{0} =_{X} x_{0}$ correspond under (2) to the swap equivalence $e$ . If $q = refl$ , then applying the function underlying (2) gives $e = {id}_{2}$ as equivalences, hence $e (tt) = tt$ by lemma 66.20 and $happly$ ; but $e (tt) \equiv ff$ , contradicting theorem 29.14. So $x_{0} =_{X} x_{0}$ has two distinct elements and is not a proposition; a set has only propositions as path types. ◻

Theorem 66.50 — No choice for arbitrary types ¶

Arbitrary indexing types do not satisfy the preceding family-choice lemma. Take $X, x_{0}$ from lemma 66.49 and put $\begin{aligned} Y (x) & : = x_{0} =_{X} x, \\ W & : = \prod_{x : X} ‖ Y (x) ‖, & S & : = \prod_{x : X} Y (x) . \end{aligned}$ The family $Y$ is set-valued, but $\neg (W \to ‖ S ‖) .$

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.50 — No choice for arbitrary types

Proof. Each $Y (x)$ is a set by lemma 66.49(3), and $\prod_{x : X} ‖ Y (x) ‖$ holds by (1). Suppose the implication held; its conclusion gives $‖ \prod_{x : X} x_{0} =_{X} x ‖$ . The goal $0$ is a proposition, so assume $C : \prod_{x : X} x_{0} =_{X} x$ (convention 66.36); then $(x_{0}, C)$ contracts $X$ , so $X$ is a proposition (lemma 66.7(1), theorem 66.10), hence a set — contradicting lemma 66.49(4). ◻

Corollary 66.51 — Unique choice ¶

Let $P$ be a family of propositions over $A$ . Then $(\prod_{x : A} ‖ P (x) ‖) \to \prod_{x : A} P (x),$ with no truncation in the conclusion and no hypothesis on $A$ .

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Proof of Corollary 66.51 — Unique choice

Proof. For each $x$ , the map $‖ P (x) ‖ \to P (x)$ exists because $P (x)$ is a proposition (lemma 66.35). ◻

Exercise 66.17 ¶

★☆☆ Complete the proof of lemma 66.47.

Referenced from 3 locations

Exercise 66.18 ¶

★☆☆ Show that $LEM$ is equivalent to the proposition-restricted law of double negation $\prod_{A : U} (isProp (A) \to \neg \neg A \to A)$ .

Referenced from 3 locations

Exercise 66.19 ¶

★☆☆ Show that $A + \neg A$ is a proposition whenever $A$ is, and conclude that $LEM$ itself is a proposition.

Referenced from 3 locations

Exercise 66.20 ¶

★☆☆ Show that if $P, Q$ are propositions with $\neg (P \times Q)$ , then $P \lor Q ≃ P + Q$ .

Referenced from 3 locations

$n$ -truncations

Truncation generalizes to every level: $‖ A ‖_{n}$ is the universal $n$ -type receiving a map from $A$ .

Definition 66.52 — n-truncation ¶

For each level $n \geq - 1$ (a rule schema per remark 66.3), the theory is extended by:

Γ ⊢ A type

Γ ⊢ ‖ A ‖_{n} type

Trunc_n-F

Γ ⊢ a : A

Γ ⊢ | a |_{n} : ‖ A ‖_{n}

Trunc_n-I

Γ ⊢ A type

Γ ⊢ h_{A} : is - n - type (‖ A ‖_{n})

Trunc_n-T

Γ, t : ‖ A ‖_{n} ⊢ C type

Γ ⊢ w : \prod_{t : ‖ A ‖_{n}} is - n - type (C)

Γ, x : A ⊢ c : C [| x |_{n} / t]

Γ ⊢ u : ‖ A ‖_{n}

Γ ⊢ {ind}_{‖ A ‖_{n}} (w, x . c, u) : C [u / t]

Trunc_n-E

Γ ⊢ a : A

Γ ⊢ {ind}_{‖ A ‖_{n}} (w, x . c, | a |_{n}) \equiv c [a / x] : C [| a |_{n} / t]

Trunc_n-C

For $n = - 2$ one puts $‖ A ‖_{- 2} : = 1$ . We write $π_{0} (A) : = ‖ A ‖_{0}$ , the set of connected components. The resulting signature is ${HoTT}_{0} + {‖ - ‖_{n}}_{n \geq - 1}$ ; no additional HIT schema is implicit in that name.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Remark 66.53 ¶

At $n = - 1$ the schema is inter-derivable with definition 66.33: $sq$ yields the witness of $is - (- 1) - type$ by theorem 66.9, and conversely. As with $‖ - ‖$ , no computation rule for the truncatedness witness $h_{A}$ is imposed. A full higher-inductive construction uses hub-and-spoke constructors attached along $S^{n + 1}$ [Uni13]. Theorem 7.3.12 of that source is instead the path-space equivalence used below.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Theorem 66.54 — Universal property ¶

For $n \geq - 1$ and every $n$ -type $B$ , precomposition with $| - |_{n}$ is an equivalence $(‖ A ‖_{n} \to B) ≃ (A \to B) .$

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.54 — Universal property

Proof. The candidate inverse sends $g : A \to B$ to ${rec}_{‖ A ‖_{n}} (g)$ , obtained from Trunc $_{n}$ -E with constant family $B$ and $w : = λ t . h_{B}$ . One composite is $g$ up to $funext$ , judgmentally on points by Trunc $_{n}$ -C. For the other, given $h : ‖ A ‖_{n} \to B$ , the family $t \mapsto {rec}_{‖ A ‖_{n}} (h \circ | - |_{n}) (t) =_{B} h (t)$ consists of $n$ -types (corollary 66.11), so Trunc $_{n}$ -E applies, and on points both sides compute to $h (| x |_{n})$ ; conclude by $funext$ (theorem 65.18). These two homotopies make the displayed precomposition map a quasi-inverse equivalence by theorem 62.27. ◻

Lemma 66.55 ¶

If $n \geq - 1$ and $A$ is an $n$ -type, then $| - |_{n} : A \to ‖ A ‖_{n}$ is an equivalence.

Referenced from 3 locations

Proof of Lemma 66.55

Proof. Theorem 66.54 with $B : = A$ yields $r : ‖ A ‖_{n} \to A$ with $r \circ | - |_{n} \sim id$ ; the composite $| - |_{n} \circ r$ is homotopic to the identity by Trunc $_{n}$ -E into the path family $t \mapsto | r (t) |_{n} =_{} t$ , whose fibers are $n$ -types (corollary 66.11), with $refl$ on points. Thus $r$ is a quasi-inverse of $| - |_{n}$ ; apply theorem 62.27. ◻

Theorem 66.56 — Path spaces of truncations ¶

For $n \geq - 1$ and $x, y : A$ , $‖ x =_{A} y ‖_{n} ≃ (| x |_{n + 1} =_{‖ A ‖_{n + 1}} | y |_{n + 1}) .$

Referenced from 5 locations

Proof of Theorem 66.56 — Path spaces of truncations

Proof. The inverse cannot be defined while both endpoints are fixed at constructor images. Generalize them. Put ${Type}_{n} : = \sum_{X : U} is - n - type (X) .$ By theorem 66.25, ${Type}_{n}$ is an $(n + 1)$ -type. Double $(n + 1)$ -truncation elimination therefore defines $\hat{P} : ‖ A ‖_{n + 1} \to ‖ A ‖_{n + 1} \to {Type}_{n},$ with constructor equation $\hat{P} (| x |_{n + 1}, | y |_{n + 1}) : = (‖ x = y ‖_{n}, h_{x = y}),$ where $h_{x = y}$ is the truncation witness. Write $P (u, v) : = {pr}_{1} (\hat{P} (u, v))$ ; each $P (u, v)$ is an $n$ -type by the second component.

Double elimination on $u, v$ , followed at constructor endpoints by $n$ -truncation elimination, defines ${decode}_{u, v} : P (u, v) \to (u = v), {decode}_{| x |_{n + 1}, | y |_{n + 1}} (| p |_{n}) : = {ap}_{| - |_{n + 1}} (p) .$ The eliminations are permitted because $u = v$ is an $n$ -type. A second elimination defines the reflexive code $r : \prod_{u : ‖ A ‖_{n + 1}} P (u, u), r (| x |_{n + 1}) : = | {refl}_{x} |_{n} .$ Transporting this code defines the other map: ${encode}_{u, v} (q) : = {tr}_{q}^{z \mapsto P (u, z)} (r (u)) : P (u, v) .$

For $q : u = v$ , identity induction reduces $decode (encode (q)) = q$ to $decode (r (u)) = {refl}_{u}$ . This is an identity type between paths in the $(n + 1)$ -type $‖ A ‖_{n + 1}$ , hence an $(n - 1)$ -type. Truncation elimination on $u$ is therefore allowed, and at $u \equiv | x |_{n + 1}$ both sides compute to ${ap}_{| - |_{n + 1}} ({refl}_{x}) \equiv refl$ .

For $c : P (u, v)$ , the other goal $encode (decode (c)) = c$ is an identity type in the $n$ -type $P (u, v)$ , hence an $(n - 1)$ -type. Eliminate $u$ and $v$ , then eliminate $c : ‖ x = y ‖_{n}$ to $c \equiv | p |_{n}$ . Identity induction on $p$ reduces ${tr}_{{ap}_{| - |_{n + 1}} (p)}^{z \mapsto P (| x |_{n + 1}, z)} (| {refl}_{x} |_{n}) = | p |_{n}$ to reflexivity. Thus $encode$ and $decode$ are quasi-inverses; theorem 62.27 gives the displayed equivalence. This is the local encode–decode proof of HoTT Book Theorem 7.3.12 [Uni13]. ◻

Example 195.58 — Connected components ¶

$π_{0} (A)$ is a set, and by theorem 66.56 its equalities are the truncated path types: $(| x |_{0} =_{π_{0} (A)} | y |_{0}) ≃ ‖ x =_{A} y ‖$ . A type is connected if $π_{0} (A)$ is contractible; lemma 66.49(1) says exactly that the type of two-element types is connected (cf. exercise 66.23).

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Exercise 66.21 ¶

★★☆ For $- 1 \leq m \leq n$ construct an equivalence $‖ ‖ A ‖_{n} ‖_{m} ≃ ‖ A ‖_{m}$ .

Referenced from 3 locations

Exercise 66.22 ¶

★★☆ Show that $‖ - ‖_{n}$ is functorial and preserves finite products: $‖ A \times B ‖_{n} ≃ ‖ A ‖_{n} \times ‖ B ‖_{n}$ .

Referenced from 3 locations

Exercise 66.23 ¶

★☆☆ Show that $A$ is connected if and only if $‖ A ‖ \times \prod_{x, y : A} ‖ x =_{A} y ‖$ holds.

Referenced from 4 locations

Quasi-inverses are not propositions

Contractible fibers make $isEquiv (f)$ a proposition. By contrast, $qinv (f)$ contains a chosen inverse and two chosen homotopies; for suitable $f$ , those choices carry nontrivial loop data.

Recall from definition 62.23 that, for $f : A \to B$ , $qinv (f) : = \sum_{g : B \to A} (g \circ f \sim {id}_{A}) \times (f \circ g \sim {id}_{B}) .$ Theorem 62.27, Proposition 62.24 provide maps $qinv (f) \to isEquiv (f)$ and $isEquiv (f) \to qinv (f)$ ; and $isEquiv (f)$ is a proposition (corollary 66.23). Were $qinv (f)$ also a proposition, the two notions would be equivalent for every $f$ (lemma 66.7(2)); theorem 66.62 rules this out.

Lemma 66.59 ¶

If $qinv (f)$ is inhabited for $f : A \to B$ , then $qinv (f) ≃ \prod_{x : A} x =_{A} x$ .

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.59

Proof. Step 1: reduction to the identity. Since $qinv (f)$ is inhabited, $f$ underlies an equivalence $e : A ≃ B$ . The based type of equivalences $\sum_{B^{'} : U} A ≃ B^{'}$ is contractible: by univalence (definition 65.6) the fiberwise map $idtoeqv : (A =_{U} B^{'}) \to (A ≃ B^{'})$ is a fiberwise equivalence, so lemma 62.31 makes the total space equivalent to $\sum_{B^{'} : U} A =_{U} B^{'}$ , which is contractible by lemma 66.5(4). Hence $(A, {id}_{A}) = (B, e)$ in this type. Define the family $P (B^{'}, e^{'}) : = qinv ({pr}_{1} (e^{'})) ≃ \prod_{x : A} x =_{A} x .$ Transporting $P (A, {id}_{A})$ along the displayed path reduces the claim to $f : = {id}_{A}$ .

Step 2: computation at the identity. Using $funext$ (theorem 65.18) in both homotopy components, $qinv ({id}_{A}) ≃ \sum_{g : A \to A} (g =_{} id) \times (g =_{} id) ≃ \sum_{u : \sum_{g : A \to A} g =_{} id} {pr}_{1} (u) =_{} id$ by re-association of $Σ$ (a definitional isomorphism, chapter 27). The inner base is contractible with center $(id, refl)$ (lemma 66.5(4)), so by lemma 195.26 the whole is equivalent to $id =_{} id$ , and by $funext$ again to $\prod_{x : A} x =_{A} x$ . ◻

Lemma 66.60 — Extending a central loop ¶

Let $A$ be a type with $a : A$ and $q : a =_{A} a$ such that

$a =_{A} a$ is a set;
$\prod_{x : A} ‖ a =_{A} x ‖$ ;
$q$ is central: $\prod_{p : a =_{A} a} p \cdot q =_{} q \cdot p$ .

Then there is $f : \prod_{x : A} x =_{A} x$ with $f (a) = q$ .

Referenced from 3 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.60 — Extending a central loop

Proof. First, every $x =_{A} y$ is a set: being a set is a proposition (theorem 66.22), so by (2) and convention 66.36 we may assume $p : a =_{A} x$ and $p^{'} : a =_{A} y$ ; then $r \mapsto p \cdot r \cdot p^{' - 1}$ is an equivalence $(x =_{A} y) ≃ (a =_{A} a)$ . Its quasi-inverse sends $s$ to $p^{- 1} \cdot s \cdot p^{'}$ , and one composite is $p^{- 1} \cdot (p \cdot r \cdot p^{' - 1}) \cdot p^{'} \overset{associativity and inverse laws}{=} r;$ the reverse composite is the same calculation with $p, p^{'}$ reversed. Hence (1) concludes by corollary 66.14.

The direct construction cannot eliminate the witness supplied by (2): the tempting clause $f (x) \overset{?}{=} p^{- 1} \cdot q \cdot p (p : ‖ a =_{A} x ‖)$ is ill typed because $p$ is truncated, while the proposed codomain $x =_{A} x$ is only known to be a set, not a proposition. The repair is to retain, together with a candidate loop, the assertion that every untruncated witness gives that same loop. This strengthened target is a proposition and therefore admits truncation elimination.

For $x : A$ define $B (x) : = \sum_{r : x =_{A} x} \prod_{s : a =_{A} x} r =_{} s^{- 1} \cdot q \cdot s .$ Each fiber over $r$ is a proposition ( $Π$ over path types of the set $x =_{A} x$ ; theorem 66.16), so $B (x)$ is a subtype of $x =_{A} x$ and lemma 66.20 applies to its elements. $B (x)$ is a proposition: this claim is itself a proposition (theorem 66.22), so assume $p : a =_{A} x$ ; given $(r, h), (r^{'}, h^{'}) : B (x)$ , we have $h (p) \cdot h^{'} (p)^{- 1} : r =_{} r^{'}$ , and lemma 66.20 lifts it to $(r, h) = (r^{'}, h^{'})$ . $B (x)$ is inhabited for every $x$ : again a proposition (just shown), so assume $p : a =_{A} x$ and put $r : = p^{- 1} \cdot q \cdot p$ ; for $s : a =_{A} x$ , whiskering by $p^{- 1}$ and $s$ and the groupoid laws reduce the required $p^{- 1} \cdot q \cdot p = s^{- 1} \cdot q \cdot s$ to $q \cdot (p \cdot s^{- 1}) = (p \cdot s^{- 1}) \cdot q$ , an instance of centrality (3) at the loop $p \cdot s^{- 1}$ .

Finally set $f (x) : = {pr}_{1} (b (x))$ , where $b : \prod_{x : A} B (x)$ is the section just constructed. At $x : = a$ the second component gives $f (a) = {refl}^{- 1} \cdot q \cdot refl = q$ by the unit laws. ◻

Lemma 66.61 — Automorphisms of ¶

Every $e : 2 ≃ 2$ is equal to ${id}_{2}$ or to the swap equivalence, and consequently any two elements of $2 ≃ 2$ commute under composition.

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Lemma 66.61 — Automorphisms of

Proof. By corollary 66.23 it suffices to identify the underlying map with $id$ or swap. Case on $e (tt)$ and $e (ff)$ ( $2$ -induction): the two “constant” cases are impossible, since an equivalence is injective and $tt \neq ff$ (theorem 29.14); in the remaining cases $funext$ identifies $e$ ’s map with $id$ or swap pointwise. Commutation: for $e, e^{'} \in {id, swap}$ , if either is $id$ the composites agree judgmentally, and if both are swap the two composites send $tt$ to $tt$ and $ff$ to $ff$ ; Boolean induction and $funext$ identify each with ${id}_{2}$ . ◻

Theorem 66.62 — Quasi-inversion is not a proposition ¶

There exist types $A, B$ and $f : A \to B$ such that $qinv (f)$ is not a proposition.

Referenced from 4 locations

Truncation Levels, Propositions, and Logic

Proof of Theorem 66.62 — Quasi-inversion is not a proposition

Proof. Take $A : = B : = X$ , the type of two-element types of lemma 66.49, and $f : = {id}_{X}$ . The triple $({id}_{X}, (λ x . {refl}_{x}, λ x . {refl}_{x}))$ inhabits $qinv ({id}_{X})$ . By lemma 66.59 it suffices to show that $\prod_{x : X} x =_{X} x$ is not a proposition (corollary 66.14).

Apply lemma 66.60 with $a : = x_{0}$ and $q$ the loop corresponding to swap. Hypothesis (1) is lemma 66.49(3); (2) is lemma 66.49(1). For centrality (3): the equivalence $h : (x_{0} =_{X} x_{0}) ≃ (2 ≃ 2)$ of lemma 66.49(2) sends concatenation to composition — ${ap}_{{pr}_{1}}$ preserves $\cdot$ (lemma 66.5(2)) and $idtoeqv (r \cdot s) = idtoeqv (s) \circ idtoeqv (r)$ by path induction — so for $p : x_{0} =_{X} x_{0}$ , $h (p \cdot q) = h (q) \circ h (p) = h (p) \circ h (q) = h (q \cdot p)$ by lemma 66.61, and injectivity of the equivalence $h$ gives $p \cdot q = q \cdot p$ .

We obtain $f_{1} : \prod_{x : X} x =_{X} x$ with $f_{1} (x_{0}) = q$ . If $\prod_{x : X} x =_{X} x$ were a proposition, then $f_{1} = λ x . refl$ , and $happly$ at $x_{0}$ would give $q = refl$ , contradicting lemma 66.49(4). ◻

Remark 66.63 — The resolution ¶

$qinv (f)$ contains chosen loop data and therefore need not be a proposition. In contrast, $isEquiv (f) : = \prod_{b : B} isContr ({fib}_{f} (b))$ is a proposition by corollary 66.23. This is why equivalences are defined by contractible fibers.

Referenced from 2 locations

Truncation Levels, Propositions, and Logic

Exercise 66.24 ¶

★☆☆ Complete the case analysis in lemma 66.61, including the injectivity argument for equivalences.

Referenced from 3 locations

Exercise 66.25 ¶

★★☆ Define bi-invertibility $biinv (f) : = (\sum_{g : B \to A} g \circ f \sim id) \times (\sum_{h : B \to A} f \circ h \sim id)$ . Show $biinv (f) \to qinv (f)$ and $qinv (f) \to biinv (f)$ , and prove that $biinv (f)$ is a proposition. Hint: when inhabited, each factor is contractible.

Referenced from 3 locations

Exercise 66.26 ¶

★☆☆ Show $‖ qinv (f) ‖ ≃ isEquiv (f)$ .

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 195.27, then complete exercise 195.28.

Exercise 195.27 ¶

★★☆ For a map $f : A \to P$ with $P$ a proposition, reconstruct its unique factor through $‖ A ‖$ . Repeat for a set-valued map out of the set truncation and identify exactly which path constructor establishes well-definedness.

Referenced from 4 locations

Exercise 195.28 ¶

★★★ Practical project.finite-truncation-auditor Implement in Agda or Kappa finite witnesses for contractible types, propositions, and sets. Preserve the invariant that every reported level includes explicit equality witnesses for the preceding level. Classify empty, singleton, Boolean, and a three-element set; reject Boolean as a proposition. Mutation test: deleting the distinct-Boolean check must fail the expected classification suite.

Referenced from 5 locations

Bibliographic notes

The stratification of types by truncation level is due to Voevodsky, who introduced “h-levels” (numbered from $0$ at contractibility; our indexing from $- 2$ , following [Uni13], aligns level $n$ with homotopy $n$ -types). The material of §§ 66.1–66.2 follows Chapters 3 and 7 of [Uni13] and Part II of [Rij25]; both sources also develop the closure properties assigned here as exercises. That propositions in the sense of definition 66.4 recover the propositions-as-types reading of Martin-Löf [ML84, ML96] at the level where proofs are unique is the perspective of [AG26], §2.7, whose treatment of squash types in extensional type theory is our definition 35.18; remark 66.34 contrasts the two. Hedberg’s theorem (theorem 66.29) appeared in his 1998 paper on coherence for Martin-Löf type theory; the collapse-lemma proof given here follows the account in [Uni13], §7.2, where the generalizations of axiom K to higher levels may also be found. Kraus, Escardó, Coquand and Altenkirch analyzed weakly constant maps and the strength of lemma 66.27 in detail. The refutation of untruncated excluded middle (theorem 66.43) is due to Coquand (cf. [Uni13], Theorem 3.2.2, of which our proof is the coproduct-transport variant); the failure of choice for non-set bases (theorem 66.50) is [Uni13], Lemma 3.8.5. The consistency of $LEM$ and $AC$ with univalence rests on the simplicial-set model of Kapulkin and Lumsdaine after Voevodsky; see the notes to Chapter 3 of [Uni13]. Propositional truncation descends from the squash types of NuPRL and the bracket types of Awodey and Bauer; its formulation as a higher inductive type, and the $n$ -truncations of § 66.6, follow [Uni13], §§3.7 and 7.3, and [Rij25]. The theorem that quasi-inversion is not a proposition (theorem 66.62) is Theorem 4.1.3 of [Uni13]; the type of two-element types used in its proof is the Eilenberg–Mac Lane space $K (Z / 2, 1)$ , and any $K (G, 1)$ for nontrivial abelian $G$ would serve. The well-behaved proposition-valued notions of equivalence (half-adjoint, bi-invertible, contractible fibers) are compared at length in [Uni13], Chapter 4, and [Rij25].

The hierarchy of truncation levels

Closure properties

Sets, axiom K, and Hedberg’s theorem

Propositional truncation

The logic of mere propositions

𝑛n-truncations

Quasi-inverses are not propositions

Suggested first pass.

Bibliographic notes

$n$ -truncations