Chapter 193Core route

Univalence

A path $p : A = B$ transports elements of $A$ to $B$ . Transport in the universal family is an equivalence, so every such path determines an equivalence $A ≃ B$ . Univalence is the assertion that every equivalence arises uniquely in this way. The inverse comparison turns equivalences into paths and thereby computes transport and yields function extensionality.

From identifications to equivalences

We use the path, fiber, contractibility, equivalence, and homotopy notation introduced in chapter 62. For $e : A ≃ B$ , application $e (a)$ means application of its underlying map. The one new abbreviation is ${tr}_{p}^{(X \mapsto X)} : A \to B$ for transport in the universal family along $p : A =_{U_{i}} B$ .

A type $X$ is a proposition when $isProp (X) : = \prod_{x : X} \prod_{y : X} (x =_{X} y)$ is inhabited. This chapter uses the predicate before the general truncation hierarchy is developed, so the definition is fixed here at its first use.

Lemma 65.2 — Calculus of contractibility ¶

Let $X$ be a type.

(Singletons.) For $a : A$ , the types $\sum_{y : A} (a =_{A} y)$ and $\sum_{y : A} (y =_{A} a)$ are contractible.
(Contractible types are propositions.) If $X$ is contractible, then $x =_{X} y$ is inhabited for all $x, y : X$ ; moreover each path type $x =_{X} y$ is itself contractible.
(Inhabited propositions are contractible.) If $X$ is inhabited and any two elements of $X$ are identified, then $X$ is contractible.
(Retracts.) If there are $s : Y \to X$ , $r : X \to Y$ and $H : r \circ s \sim {id}_{Y}$ , and $X$ is contractible, then $Y$ is contractible.
(Identities.) For every type $A$ , the identity map ${id}_{A} : = λ x . x$ is an equivalence.
(Maps of contractible types.) If $X$ and $Y$ are contractible, every map $f : X \to Y$ is an equivalence.

Referenced from 23 locations

Univalence

Proof of Lemma 65.2 — Calculus of contractibility

Proof. (i) The center is $(a, {refl}_{a})$ ; the contraction $\prod_{y : A} \prod_{p : a =_{A} y} ((a, {refl}_{a}) =_{} (y, p))$ has generic endpoint $y$ , so identity induction (definition 30.1) applies with clause ${refl}_{(a, {refl}_{a})}$ . The mirrored singleton is symmetric.

(ii) Let $c$ be the center and $γ_{x} : c =_{X} x$ the contraction; put $σ_{x, y} : = γ_{x}^{- 1} \cdot γ_{y}$ . Every $p : x =_{X} y$ is identified with $σ_{x, y}$ : by identity induction it suffices to inhabit ${refl}_{x} =_{} γ_{x}^{- 1} \cdot γ_{x}$ , the inverse of the inverse law theorem 30.20(ii). Thus $x =_{X} y$ has center $σ_{x, y}$ and the contraction just constructed.

(iii) Take the inhabitant as center, the assumed identifications as contraction.

(iv) The center is $r (c)$ ; for $y : Y$ , ${ap}_{r} (γ_{s (y)})$ followed by $H (y)$ gives $r (c) = r (s (y)) = y$ .

(v) ${fib}_{{id}_{A}} (y) \equiv \sum_{x : A} (x =_{A} y)$ is a mirrored singleton, contractible by (i).

(vi) Fix $y : Y$ . The fiber ${fib}_{f} (y)$ is inhabited: pair the center $c$ of $X$ with the identification $f (c) =_{Y} y$ supplied by (ii). Any two elements $(x, p), (x^{'}, p^{'})$ are identified: by theorem 62.30 it suffices to give $q : x =_{X} x^{'}$ — from (ii) — and to identify ${tr}_{q}^{(f (-) =_{Y} y)} (p)$ with $p^{'}$ ; both live in $f (x^{'}) =_{Y} y$ , which is contractible by (ii) applied to $Y$ , so (ii) identifies them. Conclude by (iii). ◻

Lemma 65.3 — Coercion is an equivalence ¶

For $A, B : U_{i}$ and $p : A =_{U_{i}} B$ , the transport ${tr}_{p}^{(X \mapsto X)} : A \to B$ is an equivalence.

Referenced from 3 locations

Univalence

Proof of Lemma 65.3 — Coercion is an equivalence

Proof. The endpoints of $p$ are generic, so identity induction applies: at $p \equiv {refl}_{A}$ we have ${tr}_{{refl}_{A}}^{(X \mapsto X)} \equiv {id}_{A}$ by the computation rule of transport (definition 30.1), an equivalence by lemma 65.2(v). ◻

Construction 65.4 — The comparison map ¶

For $A, B : U_{i}$ , the comparison map from type identity to equivalence is ${idtoeqv}_{A, B} : (A =_{U_{i}} B) ⟶ (A ≃ B), {idtoeqv}_{A, B} (p) : = ({tr}_{p}^{(X \mapsto X)}, w_{p}),$ where $w_{p} : isEquiv ({tr}_{p}^{(X \mapsto X)})$ is the witness of lemma 65.3. Its underlying map at ${refl}_{A}$ computes judgmentally: ${pr}_{1} ({idtoeqv}_{A, B} ({refl}_{A})) \equiv {id}_{A}$ .

Referenced from 4 locations

Univalence

Remark 65.5 — Universe bookkeeping ¶

By definition 29.1, $A =_{U_{i}} B$ is a type in $U_{i + 1}$ while $A ≃ B$ is a type in $U_{i}$ . Thus univalence makes an identity type of $U_{i}$ equivalent to a small type. The construction uses only these displayed levels and the explicit inclusions of definition 29.1, not a cumulativity rule.

Referenced from 2 locations

Univalence

Exercise 65.1 ¶

★☆☆ Define a map $(A =_{U_{i}} B) \to (A ≃ B)$ directly by identity induction, with clause $({id}_{A}, w)$ at ${refl}_{A}$ , where $w$ witnesses lemma 65.2(v). Show that it is homotopic to ${idtoeqv}_{A, B}$ of construction 65.4.

Referenced from 3 locations

Exercise 65.2 ¶

★★☆ Show that equivalences compose: if $f : A \to B$ and $g : B \to C$ are equivalences, so is $g \circ f$ . Hint: show that ${fib}_{g \circ f} (c)$ is a retract of $\sum_{w : {fib}_{g} (c)} {fib}_{f} ({pr}_{1} (w))$ , then apply lemma 65.2.

Referenced from 3 locations

The univalence axiom

Univalence adds a witness that each ${idtoeqv}_{A, B} : (A = B) \to (A ≃ B)$ is an equivalence.

Definition 65.6 — Univalence ¶

A univalent universe $U_{i}$ is a universe for which, for all $A, B : U_{i}$ , the map ${idtoeqv}_{A, B}$ of construction 65.4 is an equivalence. The univalence axiom adjoins to the base, for every level $i$ , a constant witnessing the univalence of $U_{i}$ :

Γ ⊢ A : U_{i}

Γ ⊢ B : U_{i}

Γ ⊢ {univalence}_{A, B} : isEquiv ({idtoeqv}_{A, B})

The constant is subject to no computation rule. The theory ${HoTT}_{0}$ is the base of chapter 26–chapter 30 extended by UA. No higher-inductive rule belongs to this signature.

Referenced from 15 locations

Write ${HoTT}_{0}^{[0]}$ for the single-universe fragment using $U_{0}$ and the one instance of UA at that universe. This notation is deliberately weaker than the all-level scheme ${HoTT}_{0}$ .

Theorem 65.7 — Consistency ¶

If ZFC with two strongly inaccessible cardinals is consistent, then ${HoTT}_{0}^{[0]}$ is consistent: there is no closed term of type $0$ .

Referenced from 4 locations

Univalence

Proof of Theorem 65.7 — Consistency

Proof. Kapulkin and Lumsdaine construct, from inaccessible cardinals $β < α$ , a contextual-category model in simplicial sets whose internal universe classifies the $β$ -small Kan fibrations; $α$ bounds the ambient small simplicial sets. Their Theorem 3.4.2 validates UA for that universe, and Corollary 3.4.3 derives the stated relative consistency [KL21]. The empty type is interpreted by the empty simplicial set, which has no global point. The construction and its soundness proof are the imported theorem package; no fact about simplicial sets is used in the syntactic arguments below. ◻

Remark 193.7 — Boundary of the model import ¶

The theorem covers one internal univalent universe, not the all-level scheme ${HoTT}_{0}$ . Kapulkin and Lumsdaine explicitly leave a finite or countable tower to a further construction with correspondingly many size bounds. Thus the results below are syntactic consequences of the displayed instance of UA; they do not enlarge the relative-consistency theorem. The inaccessible cardinals belong to this classical model construction, not to the statement of univalence itself. Cubical models validate a computing form of univalence in a different constructive metatheory [CCHM18, ABC^+21].

Referenced from 2 locations

Univalence

Construction 65.8 — The map and its computation laws ¶

Let $U_{i}$ be univalent and $A, B : U_{i}$ . By UA the fiber of ${idtoeqv}_{A, B}$ over any $e : A ≃ B$ is contractible; its center is a pair which we name the univalence map and its comparison path: $ua (e) : A =_{U_{i}} B, β_{e} : idtoeqv (ua (e)) =_{A ≃ B} e;$ moreover, for every $p : A =_{U_{i}} B$ there is $η_{p} : p =_{A =_{U_{i}} B} ua (idtoeqv (p))$ .

Referenced from 9 locations

Proof of Construction 65.8 — The map and its computation laws

Proof. Only $η_{p}$ requires argument. The fiber ${fib}_{idtoeqv} (idtoeqv (p))$ contains both the center $(ua (idtoeqv (p)), β_{idtoeqv (p)})$ and the element $(p, refl)$ ; being contractible, it identifies them (lemma 65.2(ii)), and ${ap}_{{pr}_{1}}$ of that identification gives $η_{p}$ up to inversion. ◻

Theorem 65.9 — Transport along ¶

Let $U_{i}$ be univalent.

For every $e : A ≃ B$ and $a : A$ , ${tr}_{ua (e)}^{(X \mapsto X)} (a) =_{B} e (a) .$
For every family $B : A \to U_{i}$ , every $p : x =_{A} y$ and $u : B (x)$ , ${tr}_{p}^{B} (u) =_{B (y)} idtoeqv ({ap}_{B} (p)) (u) .$
Consequently, if ${ap}_{B} (p) =_{B (x) =_{U_{i}} B (y)} ua (e)$ for some $e : B (x) ≃ B (y)$ , then ${tr}_{p}^{B} (u) =_{B (y)} e (u)$ .

Referenced from 11 locations

Proof of Theorem 65.9 — Transport along

Proof. (i) Apply ${ap}_{{pr}_{1}}$ to $β_{e}$ to identify the underlying maps ${tr}_{ua (e)}^{(X \mapsto X)}$ and ${pr}_{1} (e)$ in $A \to B$ , then apply ${ap}_{f \mapsto f (a)}$ .

(ii) By identity induction on $p$ : at $p \equiv {refl}_{x}$ both sides are judgmentally $u$ , since ${tr}_{refl}^{B} (u) \equiv u$ , ${ap}_{B} ({refl}_{x}) \equiv {refl}_{B (x)}$ and ${pr}_{1} (idtoeqv (refl)) \equiv id$ .

(iii) Chain (ii), $ap$ of the assumed identification, and (i). ◻

Proposition 65.10 — Equivalent forms of univalence ¶

For a universe $U_{i}$ the following are equivalent.

$U_{i}$ is univalent.
For every $A : U_{i}$ the type $\sum_{X : U_{i}} (A ≃ X)$ is contractible.
(Equivalence induction.) For every $A : U_{i}$ and every family $P (X, e)$ of types indexed by $X : U_{i}$ and $e : A ≃ X$ , every $u : P (A, {id}_{A})$ extends to $f : \prod_{X : U_{i}} \prod_{e : A ≃ X} P (X, e)$ with $f (A) ({id}_{A}) =_{P (A, {id}_{A})} u$ .

Referenced from 6 locations

Univalence

Proof of Proposition 65.10 — Equivalent forms of univalence

Proof. (i) $\Rightarrow$ (ii). The type $\sum_{X : U_{i}} (A =_{U_{i}} X)$ is a singleton, contractible by lemma 65.2(i). The maps $(X, e) \mapsto (X, ua (e)), (X, p) \mapsto (X, idtoeqv (p))$ exhibit $\sum_{X : U_{i}} (A ≃ X)$ as a retract of it: the composite sends $(X, e)$ to $(X, idtoeqv (ua (e)))$ , identified with $(X, e)$ by ${ap}_{w \mapsto (X, w)} (β_{e})$ . Conclude by lemma 65.2(iv).

(ii) $\Rightarrow$ (iii). Let $c$ be the center of $C : = \sum_{X : U_{i}} (A ≃ X)$ , $γ$ its contraction, and $c_{0} : = (A, {id}_{A})$ . For any $(X, e)$ set $π_{(X, e)} : = γ_{c_{0}}^{- 1} \cdot γ_{(X, e)} : c_{0} =_{C} (X, e)$ and define $f (X) (e) : = {tr}_{π_{(X, e)}}^{P^{'}} (u)$ , where $P^{'}$ is $P$ regarded as a family over $C$ . At $(X, e) : = c_{0}$ the transport is along the loop $γ_{c_{0}}^{- 1} \cdot γ_{c_{0}}$ , identified with ${refl}_{c_{0}}$ by theorem 30.20(ii); transporting this identification yields $f (A) ({id}_{A}) =_{P (A, {id}_{A})} u$ , since ${tr}_{refl}^{P^{'}} (u) \equiv u$ .

(iii) $\Rightarrow$ (i). Apply equivalence induction to the family $P (X, e) : = A =_{U_{i}} X$ with base element ${refl}_{A}$ . This produces $u_{X} : (A ≃ X) \to A =_{U_{i}} X$ with $u_{A} ({id}_{A}) = {refl}_{A}$ . Equivalence induction again gives $idtoeqv (u_{X} (e)) = e$ : at $(A, {id}_{A})$ both sides compute to the identity equivalence. Conversely, identity induction on $p : A =_{U_{i}} X$ gives $u_{X} (idtoeqv (p)) = p$ , with reflexivity as the base case. Thus $u_{X}$ is a quasi-inverse of ${idtoeqv}_{A, X}$ ; theorem 62.27 proves that the latter is an equivalence. ◻

Remark 65.11 — Why contractible fibers, and not quasi-inverses ¶

For univalence, the witness that a map is an equivalence must itself be a proposition. Contractible fibers have this property (lemma 65.19). A quasi-inverse instead contains a chosen inverse and two chosen homotopies. For $f : = {id}_{A}$ , its defining type contains the two independent fields $g \sim {id}_{A}$ and $g \sim {id}_{A}$ , even after fixing $g : = {id}_{A}$ . Replacing $isEquiv$ by $qinv$ would make these choices part of the axiom rather than require a proposition-valued witness. Half-adjoint and bi-invertible maps give propositional alternatives equivalent to $isEquiv$ [Uni13][AG26].

Referenced from 2 locations

Univalence

Exercise 65.4 ¶

★★☆ Reconstruct (iii) $\Rightarrow$ (i) in proposition 65.10 without reading its proof. By equivalence induction construct ${ua}^{'} : \prod_{X : U_{i}} (A ≃ X) \to (A =_{U_{i}} X)$ with ${ua}^{'} (A) (id) = refl$ ; show $idtoeqv \circ {ua}^{'} (X) \sim id$ by equivalence induction and ${ua}^{'} (X) \circ idtoeqv \sim id$ by identity induction. These two homotopies make ${ua}^{'} (X)$ a quasi-inverse of ${idtoeqv}_{A, X}$ ; finish with theorem 62.27.

Referenced from 3 locations

Function extensionality from univalence

Recall from chapter 30 the pointwise application map, defined by identity induction: ${happly}_{f, g} : (f =_{\prod_{x : A} B} g) ⟶ (f \sim g), {happly}_{f, f} ({refl}_{f}) \equiv λ x . {refl}_{f x} .$ The reverse map cannot be obtained by identity induction on a homotopy $H : \prod_{x : A} f (x) =_{} g (x)$ : its outer constructor is $Π$ , not an identity constructor, so there is no path on which $J$ can act. Instead, the proof makes every fiber of ${happly}_{f, g}$ contractible. Its key local step recovers a fiberwise equivalence from an equivalence of total maps; univalence then makes the relevant post-composition map an equivalence.

Definition 65.12 — Extensionality principles ¶

Let $A : U_{i}$ and $B : A \to U_{i}$ .

Function extensionality holds for $A, B$ if ${happly}_{f, g}$ is an equivalence for all $f, g : \prod_{x : A} B x$ . We then write $funext : (f \sim g) \to (f =_{\prod_{x : A} B x} g)$ for the resulting inverse, sending $H$ to the first component of the center of ${fib}_{{happly}_{f, g}} (H)$ .
Weak function extensionality holds for $A$ if for every family $P : A \to U_{i}$ , $(\prod_{x : A} isContr (P x)) \to isContr (\prod_{x : A} P x) .$

Referenced from 3 locations

Univalence

Lemma 65.13 — Fiberwise fibers are retracts of total fibers ¶

Let $R, S : A \to U_{i}$ and let $h_{x} : R (x) \to S (x)$ be a fiberwise map, with total map $tot (h) : \sum_{x : A} R (x) \to \sum_{x : A} S (x), tot (h) ((x, u)) : = (x, h_{x} (u)) .$ Then for every $x : A$ and $v : S (x)$ , the fiber ${fib}_{h_{x}} (v)$ is a retract of ${fib}_{tot (h)} ((x, v))$ . In particular, if $tot (h)$ is an equivalence, then so is every $h_{x}$ .

Referenced from 3 locations

Univalence

Proof of Lemma 65.13 — Fiberwise fibers are retracts of total fibers

Proof. The section is $s ((u, q)) : = ((x, u), {ap}_{w \mapsto (x, w)} (q))$ . For the retraction, consider $((y, u), \bar{s})$ with $\bar{s} : (y, h_{y} (u)) =_{} (x, v)$ . By theorem 62.30, $\bar{s}$ corresponds to a pair of $p : y =_{A} x$ and $\bar{q} : {tr}_{p}^{S} (h_{y} (u)) =_{S (x)} v$ ; by based identity induction on $p$ (chapter 30) it suffices to define the retraction when $p \equiv {refl}_{x}$ , where $\bar{q} : h_{x} (u) =_{S (x)} v$ , and we set $r : = (u, \bar{q})$ . The composite $r \circ s$ is homotopic to the identity: by identity induction on $q$ both sides reduce to $(u, refl)$ , using that the correspondence of theorem 62.30 sends $refl$ to $(refl, refl)$ .

If $tot (h)$ is an equivalence its fibers are contractible, and lemma 65.2(iv) transfers contractibility along the retract; hence each ${fib}_{h_{x}} (v)$ is contractible. ◻

Lemma 65.14 — Post-composition with an equivalence ¶

Let $U_{i}$ be univalent, $X, Y : U_{i}$ and $e : X ≃ Y$ . For every type $Z$ the map $(e \circ -) : (Z \to X) ⟶ (Z \to Y), h \mapsto λ z . e (h z),$ is an equivalence.

Referenced from 3 locations

Univalence

Proof of Lemma 65.14 — Post-composition with an equivalence

Proof. By equivalence induction (proposition 65.10(iii)) applied to the family $P (Y, e) : = isEquiv (e \circ -)$ , it suffices to treat $e : = {id}_{X}$ . Then $λ h . λ z . h z \equiv {id}_{Z \to X}$ by the $η$ -rule of $Π$ (definition 27.2), an equivalence by lemma 65.2(v). ◻

Lemma 65.15 — Projection of a contractible family ¶

Let $P : A \to U_{i}$ with $\prod_{x : A} isContr (P x)$ . Then ${pr}_{1} : (\sum_{x : A} P (x)) \to A$ is an equivalence.

Referenced from 3 locations

Univalence

Proof of Lemma 65.15 — Projection of a contractible family

Proof. Fix $x : A$ ; we show ${fib}_{{pr}_{1}} (x)$ is a retract of the contractible type $P (x)$ and conclude by lemma 65.2(iv). Take $s (((y, u), p)) : = {tr}_{p}^{P} (u), r (u) : = ((x, u), {refl}_{x}) .$ For the homotopy $r \circ s \sim id$ , based identity induction on $p : y =_{A} x$ reduces to $p \equiv {refl}_{x}$ , where $r (s (((x, u), refl))) \equiv ((x, {tr}_{refl}^{P} (u)), refl) \equiv ((x, u), refl)$ . ◻

Theorem 65.16 — Univalence implies weak function extensionality ¶

If $U_{i}$ is univalent, then weak function extensionality holds for every $A : U_{i}$ and every family $P : A \to U_{i}$ .

Referenced from 3 locations

Univalence

Proof of Theorem 65.16 — Univalence implies weak function extensionality

Proof. Suppose $\prod_{x : A} isContr (P x)$ . The projection ${pr}_{1}$ is an equivalence (lemma 65.15), hence by lemma 65.14 post-composition with it, $α : = λ h . λ x . {pr}_{1} (h x) : (A \to \sum_{x : A} P (x)) ⟶ (A \to A)$ is an equivalence, so its fiber over ${id}_{A}$ is contractible. We exhibit $\prod_{x : A} P (x)$ as a retract of ${fib}_{α} ({id}_{A})$ and conclude by lemma 65.2(iv). Define $φ (f) : = (λ x . (x, f x), {refl}_{{id}_{A}}), ψ ((h, p)) : = λ x . {tr}_{happly (p) (x)}^{P} ({pr}_{2} (h x)) .$ The term $φ (f)$ is well typed because $α (λ x . (x, f x)) \equiv λ x . {pr}_{1} (x, f x) \equiv λ x . x \equiv {id}_{A}$ by the computation rule of $Σ$ (definition 27.9). The round trip computes judgmentally: $ψ (φ (f)) \overset{happly, Σ - β}{\equiv} λ x . {tr}_{{refl}_{x}}^{P} (f x) \overset{t r a n s p o r t - β}{\equiv} λ x . f x \overset{Π - η}{\equiv} f,$ so the retraction homotopy is $λ f . {refl}_{f}$ . ◻

Theorem 65.17 — Weak function extensionality implies function extensionality ¶

If weak function extensionality holds (definition 65.12(ii)), then for all $f, g : \prod_{x : A} B x$ the map ${happly}_{f, g}$ is an equivalence. Univalence is not used in the proof.

Referenced from 4 locations

Univalence

Proof of Theorem 65.17 — Weak function extensionality implies function extensionality

Proof. Fix $f$ and regard ${happly}_{f, g}$ as a fiberwise map, over $g : \prod_{x : A} B x$ , from the family $g \mapsto (f =_{} g)$ to the family $g \mapsto (f \sim g)$ . By lemma 65.13 it suffices to show that the total map $tot ({happly}_{f}) : \sum_{g : \prod_{x : A} B x} (f =_{} g) ⟶ \sum_{g : \prod_{x : A} B x} (f \sim g)$ is an equivalence; by lemma 65.2(vi) it suffices that both totals are contractible. The left one is a singleton (lemma 65.2(i)). For the right one, consider $\begin{aligned} ϱ : & (\prod_{x : A} \sum_{u : B x} (f x =_{B x} u)) ⟶ \sum_{g : \prod_{x : A} B x} (f \sim g), \\ ϱ (K) : = & (λ x . {pr}_{1} (K x), λ x . {pr}_{2} (K x)) . \end{aligned}$ It has section $ς ((g, H)) : = λ x . (g x, H x)$ . The composite $ϱ \circ ς$ is judgmentally the identity, by the computation rules of $Σ$ and the $η$ -rule of $Π$ . The domain of $ϱ$ is a dependent product of singletons, contractible by weak function extensionality and lemma 65.2(i); hence the right total is contractible by lemma 65.2(iv). ◻

Theorem 65.18 — Univalence implies function extensionality ¶

Let $U_{i}$ be univalent, $A : U_{i}$ , $B : A \to U_{i}$ . Then function extensionality holds for $A, B$ : for all $f, g : \prod_{x : A} B x$ , the map ${happly}_{f, g}$ is an equivalence, and hence $f =_{\prod_{x : A} B x} g ≃ (f \sim g)$ .

Referenced from 21 locations

Proof of Theorem 65.18 — Univalence implies function extensionality

Proof. Theorem 65.16 gives weak function extensionality for families over $A$ in $U_{i}$ ; the families used in the proof of theorem 65.17, namely $x \mapsto \sum_{u : B x} (f x =_{B x} u)$ , lie in $U_{i}$ because $U_{i}$ is closed under $Σ$ and identity types (definition 29.1). Apply theorem 65.17. ◻

With function extensionality in hand, the basic predicates of this chapter become propositions, and $ua$ becomes functorial.

Lemma 65.19 — Propositionality of the basic predicates ¶

Assume function extensionality. Use $isProp (X)$ as fixed at the beginning of the chapter.

If $P : A \to U_{i}$ is a family of propositions, then $\prod_{x : A} P (x)$ is a proposition.
$isContr (X)$ is a proposition.
$isEquiv (f)$ is a proposition, for every $f : A \to B$ .
If $e, e^{'} : A ≃ B$ and ${pr}_{1} (e) =_{A \to B} {pr}_{1} (e^{'})$ , then $e =_{A ≃ B} e^{'}$ .

Referenced from 8 locations

Univalence

Proof of Lemma 65.19 — Propositionality of the basic predicates

Proof. (i) For $f, g : \prod_{x : A} P (x)$ apply $funext$ to $λ x . h_{x} (f x) (g x)$ , where $h_{x}$ witnesses $isProp (P (x))$ .

(ii) Let $w, w^{'} : isContr (X)$ ; in particular $X$ is contractible, so by lemma 65.2(ii) every path type of $X$ is contractible. Write $w = (c, γ)$ , $w^{'} = (c^{'}, γ^{'})$ . By theorem 62.30 it suffices to identify $c$ with $c^{'}$ — by lemma 65.2(ii) — and then the transported contraction with $γ^{'}$ . After transporting $γ$ along $c = c^{'}$ , both $transport (γ)$ and $γ^{'}$ inhabit $\prod_{x : X} (c^{'} =_{X} x)$ . Each factor $c^{'} = x$ is contractible, so (i) identifies these two contractions.

(iii) $isEquiv (f)$ is a product of the propositions $isContr ({fib}_{f} (b))$ ; apply (i) and (ii).

(iv) By theorem 62.30 it suffices to transport the $isEquiv$ -witness along the given identification and identify the result with that of $e^{'}$ ; both live in $isEquiv ({pr}_{1} (e^{'}))$ , a proposition by (iii). ◻

Exercise 65.3 ¶

★☆☆ Show that ${refl}_{A} =_{A =_{U_{i}} A} ua ({id}_{A})$ , where ${id}_{A}$ carries the witness of lemma 65.2(v). Hint: instantiate $η_{p}$ of construction 65.8 at $p : = {refl}_{A}$ and use ${pr}_{1} (idtoeqv ({refl}_{A})) \equiv {id}_{A}$ together with lemma 65.19(iv).

Referenced from 3 locations

Exercise 65.5 ¶

★★☆ (Licata’s reduction.) Assume function extensionality. Suppose given, for all $A, B : U_{i}$ , only a map $u : (A ≃ B) \to (A =_{U_{i}} B)$ and a family of identifications $\prod_{e : A ≃ B} {tr}_{u (e)}^{(X \mapsto X)} =_{A \to B} {pr}_{1} (e)$ . Show that $U_{i}$ is univalent. Hint: verify that the retract argument of proposition 65.10(i) $\Rightarrow$ (ii) needs only this data, granted lemma 65.19.

Referenced from 4 locations

Corollary 65.20 — Functoriality of ¶

Let $U_{i}$ be univalent, $A, B, C : U_{i}$ , $e : A ≃ B$ , $e^{'} : B ≃ C$ . Then

${refl}_{A} =_{} ua ({id}_{A})$ ;
$ua (e) \cdot ua (e^{'}) =_{} ua (e^{'} \circ e)$ , where $e^{'} \circ e$ is the composite equivalence of proposition 62.28;
$ua (e)^{- 1} =_{} ua (e^{- 1})$ , where $e^{- 1}$ is the inverse equivalence of proposition 62.28.

Referenced from 5 locations

Univalence

Proof of Corollary 65.20 — Functoriality of

Proof. (i) Instantiate $η_{p}$ from construction 65.8 at $p : = {refl}_{A}$ . Since $idtoeqv ({refl}_{A}) \equiv {id}_{A}$ , its inverse has the stated orientation. For (ii), first note the transport law ${tr}_{p \cdot q}^{(X \mapsto X)} =_{A \to C} {tr}_{q}^{(X \mapsto X)} \circ {tr}_{p}^{(X \mapsto X)}$ for $p : A =_{U_{i}} B$ , $q : B =_{U_{i}} C$ : by identity induction on $q$ it reduces, using $p \cdot refl \equiv p$ (theorem 30.20(i)) and the $η$ -rule of $Π$ , to $refl$ . Now put $p : = ua (e)$ , $q : = ua (e^{'})$ . By theorem 65.9(i) and the transport law, the underlying maps of $idtoeqv (p \cdot q)$ and of $e^{'} \circ e$ are identified; by lemma 65.19(iv), $idtoeqv (p \cdot q) =_{A ≃ C} e^{'} \circ e$ . With $η$ from construction 65.8, $ua (e^{'} \circ e) \overset{{ap}_{ua}}{=} ua (idtoeqv (p \cdot q)) \overset{η_{p \cdot q}}{=} p \cdot q .$ For (iii), put $p : = ua (e)$ . Identity induction gives $idtoeqv (p^{- 1}) = idtoeqv (p)^{- 1}$ . Combine this with $β_{e}$ from construction 65.8 and the fact that inversion preserves paths of equivalences to obtain $idtoeqv (p^{- 1}) = e^{- 1}$ . Applying $ua$ and then $η_{p^{- 1}}$ gives $ua (e^{- 1}) = p^{- 1}$ , which is the asserted equality after symmetry. ◻

Exercise 65.6 ¶

★★☆ Assume function extensionality. Establish the propositional computation laws $happly (funext (H)) =_{} H$ and $funext (happly (p)) =_{} p$ , and show $funext (λ x . {refl}_{f x}) =_{} {refl}_{f}$ .

Referenced from 3 locations

Exercise 65.7 ¶

★★☆ For an equivalence $e : A ≃ B$ construct the inverse equivalence $e^{- 1} : B ≃ A$ whose underlying map sends $b$ to the first component of the center of ${fib}_{{pr}_{1} (e)} (b)$ , and show $e^{- 1} \circ e \sim {id}_{A}$ and $e \circ e^{- 1} \sim {id}_{B}$ .

Referenced from 3 locations

Exercise 65.8 ¶

★☆☆ Prove corollary 65.20(iii). Hint: by lemma 65.19(iv) it suffices to identify the underlying maps of $idtoeqv (ua (e)^{- 1})$ and $e^{- 1}$ ; use corollary 65.20(ii) with $e^{'} : = e^{- 1}$ and cancel.

Referenced from 3 locations

Univalence refutes the uniqueness of identity proofs

The groupoid fragment of corollary 54.36 cannot derive $K$ ; univalence refutes it outright in ${HoTT}_{0}$ . The refutation runs through $2$ and its two self-equivalences.

Lemma 65.21 — Path spaces of ¶

Let $not : 2 \to 2$ be defined by $2$ -recursion (definition 28.7) so that $not (tt) \equiv ff$ and $not (ff) \equiv tt$ .

$(tt =_{2} ff) \to 0$ is inhabited.
For every $b : 2$ and every $p : b =_{2} b$ , $p =_{} {refl}_{b}$ .
$not$ is an equivalence.

Referenced from 10 locations

Proof of Lemma 65.21 — Path spaces of

Proof. We follow the encode–decode pattern (theorem 62.35). By double $2$ -recursion into $U_{0}$ — large elimination, definition 29.1 — define $code : 2 \to 2 \to U_{0}$ with $code (tt, tt) \equiv 1, code (ff, ff) \equiv 1, code (tt, ff) \equiv 0, code (ff, tt) \equiv 0,$ and $c : \prod_{b : 2} code (b, b)$ by induction with $c (tt) : = ⋆$ , $c (ff) : = ⋆$ . Set ${encode}_{b, b^{'}} : (b =_{2} b^{'}) \to code (b, b^{'}), encode (p) : = {tr}_{p}^{code (b, -)} (c (b)) .$ (i) ${encode}_{tt, ff}$ lands in $code (tt, ff) \equiv 0$ . (This internalizes theorem 29.14.)

(ii) Define ${decode}_{b, b^{'}} : code (b, b^{'}) \to (b =_{2} b^{'})$ by double induction: ${decode}_{tt, tt} : = λ u . {refl}_{tt}$ , ${decode}_{ff, ff} : = λ u . {refl}_{ff}$ , and ${rec}_{0}$ in the off-diagonal cases. Identity induction shows $decode (encode (p)) = p$ for all $p : b =_{2} b^{'}$ : at $p \equiv {refl}_{b}$ , $encode (refl) \equiv c (b)$ , and $2$ -induction on $b$ reduces $decode (c (b))$ to ${refl}_{b}$ judgmentally. Now fix $p : b =_{2} b$ and induct on $b$ . For $b \equiv tt$ : $encode (p) : 1$ , so $encode (p) \equiv ⋆$ by the $η$ -rule of $1$ (chapter 27), whence $p = decode (encode (p)) \equiv decode (⋆) \equiv {refl}_{tt}$ . The case $b \equiv ff$ is symmetric.

(iii) We show ${fib}_{not} (b)$ contractible for each $b$ , by induction on $b$ ; we treat $b \equiv tt$ , the other case being symmetric. The center is $(ff, {refl}_{tt})$ , well typed since $not (ff) \equiv tt$ . For the contraction, take $(b^{'}, p)$ and induct on $b^{'}$ . If $b^{'} \equiv ff$ then $p : tt =_{2} tt$ , so $p = refl$ by (ii), and ${ap}_{q \mapsto (ff, q)}$ of that identification concludes. If $b^{'} \equiv tt$ then $p : ff =_{2} tt$ , and ${rec}_{0}$ applied to (i) at $p^{- 1}$ concludes. ◻

Theorem 65.22 — Univalence refutes UIP ¶

Write $isSet (X) : = \prod_{x : X} \prod_{y : X} isProp (x =_{X} y) .$ If $U_{0}$ is univalent, then $isSet (U_{0}) ⟶ 0$ is inhabited. Consequently the theory ${HoTT}_{0}$ of definition 65.6 becomes inconsistent upon adding either a UIP axiom for $U_{0}$ or the rule $K$ of definition 30.28; in particular univalence and equality reflection (definition 35.1) are jointly inconsistent (cf. theorem 35.9).

Referenced from 9 locations

Proof of Theorem 65.22 — Univalence refutes UIP

Proof. Suppose $h : isSet (U_{0})$ . Let $e_{not} : 2 ≃ 2$ be $not$ with the witness of lemma 65.21(iii), and let ${id}_{2}$ carry the witness of lemma 65.2(v). Put $p : = ua ({id}_{2}), q : = ua (e_{not}) : 2 =_{U_{0}} 2 .$ Then $h$ yields $α : p =_{} q$ , and ${ap}_{r \mapsto {tr}_{r}^{(X \mapsto X)} (tt)} (α)$ gives ${tr}_{p}^{(X \mapsto X)} (tt) =_{2} {tr}_{q}^{(X \mapsto X)} (tt)$ . By theorem 65.9(i), ${tr}_{p}^{(X \mapsto X)} (tt) = id (tt) \equiv tt$ and ${tr}_{q}^{(X \mapsto X)} (tt) = not (tt) \equiv ff$ . Concatenating, $tt =_{2} ff$ , and lemma 65.21(i) produces the element of $0$ .

For the consequences: a UIP axiom for $U_{0}$ inhabits $isSet (U_{0})$ directly; the rule $K$ derives it; and equality reflection derives UIP by theorem 35.9(i). ◻

Corollary 65.23 ¶

In ${HoTT}_{0}$ the universe $U_{0}$ is not a set. In particular the type $2 =_{U_{0}} 2$ has two elements that cannot be identified: $ua ({id}_{2})$ and $ua (e_{not})$ .

Referenced from 2 locations

Univalence

Proof of Corollary 65.23

Proof. An identification $r : ua ({id}_{2}) = ua (e_{not})$ would, by congruence of $p \mapsto {tr}_{p}^{(X \mapsto X)} (tt)$ , equate the identity action on $tt$ with the negation action. By theorem 65.9, this gives $tt =_{2} ff$ , contradicting lemma 65.21(i). ◻

Proposition 193.24 — The two Boolean automorphisms ¶

Evaluation at $tt$ is an equivalence $(2 ≃ 2) ≃ 2 .$ Its inverse sends $tt$ to ${id}_{2}$ and $ff$ to $e_{not}$ . Consequently, when $U_{0}$ is univalent, $(2 =_{U_{0}} 2) ≃ 2$ .

Referenced from 4 locations

Proof of Proposition 193.24 — The two Boolean automorphisms

Proof. Let $e : 2 ≃ 2$ . Induct on $e (tt)$ . If $e (tt) = tt$ , then $e (ff) = ff$ : the other Boolean value would contradict injectivity of the underlying equivalence and lemma 65.21(i). Function extensionality and Boolean induction therefore identify the underlying map of $e$ with the identity. The equivalence witnesses are propositions by lemma 65.19(iii), so $e = {id}_{2}$ . If $e (tt) = ff$ , repeat the Boolean induction with $tt$ and $ff$ exchanged; function extensionality gives $e = e_{not}$ . These two cases prove the inverse law for the displayed decoder; its other composite computes on both Boolean constructors. The last equivalence is the composite of this one with univalence $(2 = 2) ≃ (2 ≃ 2)$ . ◻

Remark 65.24 — The tower does not stop ¶

The Boolean automorphism proves exactly that $U_{0}$ is not a set. It does not by itself determine the truncation level of $U_{1}$ or of higher universes: that would require information about higher automorphism types. No iterated nontruncation claim is used below.

Referenced from 2 locations

Univalence

Remark 65.25 — Internal versus external refutation ¶

The groupoid model proves that UIP is not derivable from the intensional fragment $T_{G}$ (corollary 54.36). In ${HoTT}_{0}$ , univalence proves the internal negation $UIP \to 0$ (theorem 65.22). The semantic independence result and the internal refutation therefore have different hypotheses.

Referenced from 2 locations

Univalence

Exercise 65.9 ¶

★☆☆ Complete the characterization begun in lemma 65.21: show $encode (decode (u)) = u$ for all $u : code (b, b^{'})$ , and conclude $(b =_{2} b^{'}) ≃ code (b, b^{'})$ .

Referenced from 3 locations

Exercise 65.10 ¶

★☆☆ Show $ua (e_{not}) =_{} {refl}_{2} \to 0$ . Hint: transport $tt$ and use theorem 65.9, lemma 65.21.

Referenced from 3 locations

Exercise 65.11 ¶

★★☆ Reconstruct proposition 193.24. In each Boolean case, display the injectivity contradiction that fixes the image of $ff$ before using function extensionality.

Referenced from 3 locations

Propositional univalence

Restricting univalence to propositions yields a markedly weaker principle. An abstract univalent universe of propositions is compatible with UIP, but the ordinary set model does not make the concrete subuniverse $U_{0}^{prop}$ univalent. For propositions, implications in both directions determine an equivalence; propositional univalence therefore identifies proposition codes from $P \leftrightarrow Q$ , whereas full univalence identifies arbitrary types from $A ≃ B$ .

Definition 65.26 — Propositions and universes of propositions ¶

Using the predicate $isProp$ fixed at the start of the chapter, write $U_{i}^{prop} : = \sum_{X : U_{i}} isProp (X), A \leftrightarrow B : = (A \to B) \times (B \to A) .$ A universe of propositions is a pair of a type $Ω$ and a map $dec : Ω \to U_{i}^{prop}$ ; it is univalent if $\prod_{x : Ω} \prod_{y : Ω} (dec (x) \leftrightarrow dec (y)) \to (x =_{Ω} y)$ is inhabited (where $dec (x)$ abbreviates the underlying type), and adequate if there is $enc : U_{i}^{prop} \to Ω$ with $dec (enc (A)) \leftrightarrow A$ for every $A$ .

Referenced from 5 locations

Univalence

Lemma 65.27 — Propositions are sets ¶

If $isProp (X)$ is inhabited, then every path type $x =_{X} y$ of $X$ is a proposition, and it is contractible as soon as $X$ is inhabited; in particular $isSet (X)$ .

Referenced from 4 locations

Univalence

Proof of Lemma 65.27 — Propositions are sets

Proof. Let $h : isProp (X)$ and fix $x : X$ . For any $p : y =_{X} z$ , the dependent action $apd$ (chapter 30) of the map $h (x) : \prod_{w : X} (x =_{X} w)$ on $p$ gives ${tr}_{p}^{(x =_{X} -)} (h (x) (y)) = h (x) (z),$ while transport in the family $w \mapsto x =_{X} w$ computes as post-concatenation: by identity induction on $p$ , ${tr}_{p}^{(x =_{X} -)} (q) = q \cdot p$ . Hence $h (x) (y) \cdot p = h (x) (z)$ , so $p = h (x) (y)^{- 1} \cdot h (x) (z)$ by the groupoid laws (theorem 30.20). The right-hand side does not depend on $p$ : any two elements of $y =_{X} z$ are identified, i.e. the path type is a proposition. If $X$ is inhabited then so is each $y =_{X} z$ (by $h$ ), hence contractible by lemma 65.2(iii). ◻

Lemma 193.29 — Propositionality of being a proposition ¶

Assume function extensionality. For every type $X$ , the type $isProp (X)$ is a proposition.

Referenced from 4 locations

Univalence

Proof of Lemma 193.29 — Propositionality of being a proposition

Proof. Let $h, k : isProp (X)$ . Function extensionality twice reduces $h = k$ to $h (x) (y) = k (x) (y)$ for arbitrary $x, y : X$ . The witness $h$ makes $X$ a proposition, so lemma 65.27 makes the path type $x = y$ a proposition. Hence its two elements $h (x) (y)$ and $k (x) (y)$ are equal. ◻

Proposition 65.28 — Univalence implies propositional univalence ¶

Let $U_{i}$ be univalent and let $A, B : U_{i}$ be propositions with $(f, g) : A \leftrightarrow B$ . Then:

$f$ is an equivalence;
$A =_{U_{i}} B$ is inhabited, by $ua$ of (i);
granting theorem 65.18, the pair $(U_{i}^{prop}, id)$ is a univalent universe of propositions in the sense of definition 65.26.

Referenced from 5 locations

Proof of Proposition 65.28 — Univalence implies propositional univalence

Proof. (i) Fix $b : B$ ; we show ${fib}_{f} (b)$ is an inhabited proposition, hence contractible (lemma 65.2(iii)). It is inhabited by $(g (b), h_{B} (f (g (b))) (b))$ , where $h_{B} : isProp (B)$ . Given $(a, p), (a^{'}, p^{'}) : {fib}_{f} (b)$ , we have $h_{A} (a) (a^{'}) : a =_{A} a^{'}$ , and by theorem 62.30 it remains to identify the transport of $p$ with $p^{'}$ inside $f (a^{'}) =_{B} b$ — a path type of the inhabited proposition $B$ , contractible by lemma 65.27, so lemma 65.2(ii) concludes. (ii) Apply $ua$ . For (iii), apply theorem 62.30 to two pairs $(A, h_{A}), (B, h_{B}) : U_{i}^{prop}$ . Part (ii) supplies the path $A = B$ whenever the underlying propositions are interprovable. The remaining fiber equality compares the transported proof $h_{A}$ with $h_{B}$ ; it is unique by lemma 193.29. Conversely a path of pairs gives maps both ways by transport. Thus the canonical comparison for the subuniverse is an equivalence. ◻

Proposition 65.29 — Propositional univalence is weaker ¶

Work over the intensional base with universes.

In the set model (definition 48.30), the statement that $(U_{0}^{prop}, id)$ is univalent is interpreted by the empty set: the set model refutes it.
Nevertheless, the base together with funext, UIP, and the existence of a univalent and adequate universe of propositions (definition 65.26) at every level is consistent relative to the set-model assumptions of convention 48.28.

Hence propositional univalence, in its abstract form, is compatible with UIP, while full univalence is not (theorem 65.22).

Referenced from 3 locations

Univalence

Proof of Proposition 65.29 — Propositional univalence is weaker

Proof. (i) In the set model, $U_{0}^{prop}$ is interpreted as the set of all subsingleton sets in the first Grothendieck universe. The distinct singleton sets ${⋆}$ and ${{⋆}}$ are interprovable — there are functions both ways — but not equal, so the interpreted univalence statement has no elements.

(ii) Interpret the abstract universe of propositions by $Ω : = {⊤, ⊥}$ with $dec (⊤) : = {⋆}$ and $dec (⊥) : = \emptyset$ . Univalence holds by case analysis: interprovable values of $dec$ force equal elements of $Ω$ , since there is no function ${⋆} \to \emptyset$ . Adequacy: send $\emptyset$ to $⊥$ and every singleton to $⊤$ . The set model validates funext and UIP (definition 48.30, corollary 90.7). Details in [AG26], §5.1. ◻

Remark 65.30 — The comparison ¶

Each row names the theory in which its identity types are characterized.

principle	characterizes $=_{}$ of	with UIP	set model
funext (theorem 65.18)	$Π$ -types	consistent	valid
UIP / $K$ in $T_{G}$ (corollary 54.36)	identity types	—	valid
prop. univalence (abstract)	$Ω$	consistent	valid
univalence (definition 65.6)	$U_{i}$	inconsistent	refuted

Two structural differences explain why propositional univalence is so much simpler to state than definition 65.6: for propositions, $A \leftrightarrow B$ is already equivalent to $A ≃ B$ (proposition 65.28(i)), and a mere map $(dec (x) \leftrightarrow dec (y)) \to (x =_{Ω} y)$ already forces the canonical comparison to be an equivalence. Indeed, the map back to identity fits into $(x =_{Ω} y) \overset{idtoeqv}{\to} (dec (x) ≃ dec (y)) ⟶ (x =_{Ω} y) .$ The second composite is the identity on equivalences because equivalence witnesses are propositions; the induced retract on total spaces makes $idtoeqv$ an equivalence. This is Licata’s reduction.

Referenced from 2 locations

Univalence

Resizing and the subobject classifier. Adequacy in definition 65.26 says that a single type $Ω$ indexes, up to interprovability, the propositions of every $U_{i}$ ; iterated over levels this is the principle of propositional resizing, an impredicativity axiom. A univalent, adequate, resizing $Ω$ is the type-theoretic form of the subobject classifier of an elementary topos [Jac99]. Resizing is independent of univalence; large classes of models of UA validate it, but it is not a theorem of ${HoTT}_{0}$ .

Exercise 65.12 ¶

★★☆ Assume function extensionality. Show that if $A$ and $B$ are propositions then $A \leftrightarrow B$ and $A ≃ B$ are propositions, and that $(A ≃ B) \to (A \leftrightarrow B), e \mapsto (e . to, e . from),$ is an equivalence.

Referenced from 3 locations

Exercise 65.13 ¶

★☆☆ Prove proposition 65.28(iii): interprovable elements of $U_{i}^{prop}$ are identified as elements of the subuniverse. Hint: theorem 62.30 reduces the problem to (ii) and lemma 193.29.

Referenced from 3 locations

The computation problem

Let $ω : = {tr}_{ua (e_{not})}^{(X \mapsto X)} (tt) : 2 .$ The transport rule reduces only along reflexivity, so no root rule reduces $ω$ ; nevertheless theorem 65.9 proves $ω = ff$ .

Proposition 65.31 — Failure of canonicity ¶

Under the metatheoretic consistency assumption of theorem 65.7, consider the closed term $ω$ above in ${HoTT}_{0}^{[0]}$ , with $e_{not}$ as in theorem 65.22. No root computation rule applies to $ω$ , while the type $ω =_{2} ff$ is inhabited. Moreover $ω ≢ tt$ . No claim that $ω ≢ ff$ is made without a normalization theorem for the full signature.

Referenced from 2 locations

Univalence

Proof of Proposition 65.31 — Failure of canonicity

Proof. By theorem 65.9(i) the type $ω =_{2} ff$ is inhabited by a closed term. If $ω \equiv tt$ were derivable, conversion (definition 26.22) would make the same term inhabit $tt =_{2} ff$ , and lemma 65.21(i) would produce a closed term of $0$ , contradicting theorem 65.7. Finally, the only root rule for transport is its reflexivity equation, and $ua (e_{not})$ is headed by the inert univalence constant rather than $refl$ . Thus $ω$ is root-stuck. Propositional equality with $ff$ is compatible with either outcome of the unresolved judgmental comparison. ◻

If the intensional base had a sound and complete normalization function, the usual inert-constant argument would also separate $ω$ from every constructor-headed Boolean. Replace each equation-free added constant by a variable; normalization then preserves its neutral head, which cannot equal a constructor-headed normal form. Chapter 49 proves closed-Boolean canonicity for its local $Π / 2$ fragment and imports a normalization theorem for a separate cumulative signature. It proves no open normalization theorem even for the local fragment, and neither result covers the universe, $Σ$ , $N$ , and identity signature used here. This conditional diagnostic therefore gives no additional judgmental inequality in ${HoTT}_{0}^{[0]}$ .

Remark 65.32 — What is and is not lost ¶

For every finite iterate in exercise 65.15, the transport theorem computes a propositional equality with its Boolean result. What fails is head reduction: extracting that result requires the propositional calculation rather than evaluation. Deciding the remaining judgmental comparisons requires normalization for the full ${HoTT}_{0}$ signature.

Referenced from 2 locations

Univalence

Remark 65.33 — The way forward ¶

Axiomatic univalence proves the propositional result $ω = ff$ but has no head-reduction rule for $ω$ . Any extension that makes this transport evaluate must add computation rules absent from ${HoTT}_{0}$ .

Referenced from 2 locations

Univalence

Exercise 65.14 ¶

★☆☆ Exhibit a closed term of $ω =_{2} ff$ in ${HoTT}_{0}$ , writing out the applications of construction 65.8 and theorem 65.9(i) involved.

Referenced from 3 locations

Exercise 65.15 ¶

★★☆ Let $ω_{n}$ be the result of transporting $tt$ along the $n$ -fold concatenation $ua (e_{not}) \cdot \dots \cdot ua (e_{not})$ . Using corollary 65.20, prove $ω_{n} =_{2} tt$ for even $n$ and $ω_{n} =_{2} ff$ for odd $n$ .

Referenced from 4 locations

Suggested first pass.

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

Exercise 193.16 ¶

★★☆ Use the Boolean swap equivalence to construct the corresponding universe loop. Compute its action on both constructors from the $ua$ transport law, and use the result to reproduce the contradiction with UIP.

Referenced from 4 locations

Exercise 193.17 ¶

★★★ Practical project.univalence-transport-simulator Implement in Agda or Kappa a finite-set equivalence evaluator and the transport action assigned to its formal $ua$ path. Preserve bijectivity and endpoint types. On the two-element set, identity must fix both values and swap must exchange them; composing swap twice must print identity. Mutation test: omit inverse verification and ensure a non-bijection is then accepted, so the correct suite catches the defect.

Referenced from 5 locations

Bibliographic notes

The univalence axiom is due to Voevodsky (2009–2010), who formulated it after identifying the contractible-fibers notion of equivalence and who established its model in simplicial sets; the model was written up in detail by Kapulkin and Lumsdaine. Voevodsky attributed the word “univalent” in part to a Russian translation of Boardman and Vogt in which faithful was rendered as univalentnyj; see [AG26], Remark 5.2.4, for the story and for the reading of univalence as a not-quite universal property of the universe. Our presentation follows the HoTT Book [Uni13], §§2.10 and 4.9, and Rijke’s textbook [Rij25], whose “fundamental theorem of identity types” systematizes the retract arguments of §§ 65.1–65.3; the equivalent forms of proposition 65.10 appear there as the characterization of univalence, and the reduction of exercise 65.5 was observed by Licata. The proof that univalence implies function extensionality (theorem 65.18) is Voevodsky’s; we followed the route through weak function extensionality of [Uni13], §4.9, in Rijke’s streamlined form. The refutation of UIP (theorem 65.22) is folklore dating to the first days of the subject. The groupoid interpretation of Hofmann and Streicher [HS98] refutes UIP semantically. Its discrete universe in theorem 54.34 is not univalent; a univalent universe would have to retain equivalences as paths. Propositional univalence, its abstraction over universes of propositions, and the set-model comparison of proposition 65.29 follow [AG26], §5.1; the topos-theoretic reading of a univalent $Ω$ as subobject classifier is classical [Jac99]. The computational deficiency of axiomatic univalence (§ 65.6) was recognized immediately and drove the designs of part V: observational equality [AM06, AMS07, PT22], the cubical theories in which univalence is a theorem [CCHM18, ABC^+21] with canonicity and normalization [Ang19, SA21], and the gluing methods by which such metatheorems are proved [Coq19, Ste21].