Homotopy Type Theory univalent universe (changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

Theunivalence axiom for a universe $U$ states that for all $A,B:U$, the map

$(A=_U B) \to (A\simeq B)$

Definition

In higher observational type theory

A universe $U$ is univalent if for all $A,B:U$ there are rules

$\frac{R:A \simeq_U B}{\Delta R:\mathrm{id}_U(A, B)} \qquad \frac{P:\mathrm{id}_U(A, B)}{\nabla P:A \simeq_U B} \qquad \frac{R:A \simeq_U B}{\nabla \Delta R \equiv R}$

In homotopy type theory

A universe $U$ is univalent if for all $A,B:U$, the map

$(A=_U B) \to (A\simeq_U B)$

defined by path induction, is an equivalence. So we have

 (A=_U B) \simeq (A \simeq \simeq_U B).

A univalent universe inside a non-univalent universe

In a post to the Homotopy Type Theory Google Group, Peter LeFanu Lumsdaine wrote:

Let $(x_0:X)$ be any pointed type, and $(\mathcal{U}, El)$ be a universe (with rules as I set out a couple of emails ago). Then $X \times \mathcal{U}$ is again a universe, admitting all the same constructors as $\mathcal{U}$: take

$El(x,A) = El(A)$,
$(x,A) +_\mathcal{U} (y,B) = (x_0, A +_\mathcal{U} B)$,

and so on; that is, constructor operations on $(X \times \mathcal{U})$ are constantly $x_0$ on the first component, and mirror those of $\mathcal{U}$ on the second component.

Now if $\mathcal{U}$ is univalent, and $X$ has non-trivial $\pi_0$ (e.g. $X=S^1$), then $\mathcal{U} \rightarrow (X \times \mathcal{U}$) gives a univalent universe sitting inside a non-univalent one (again, with the rules as I set out earlier).

Slightly more generally, given any cumulative pair of universes $\mathcal{U}_0 \rightarrow \mathcal{U}_1$, we can consider $\mathcal{U}_0 \rightarrow A \times \mathcal{U}_1$; this shows we can additionally have the smaller universe represented by an element of the larger one.

[N]ot only is $X \times \mathcal{U}$ not univalent, it’s not even “univalent on the image of $\mathcal{U}$”, as was the case for the example in the groupoid model that I mentioned.

category: axioms, type theory

Last revised on April 29, 2022 at 14:27:05. See the history of this page for a list of all contributions to it.