Homotopy Type Theory univalent universe > history (Rev #10, changes)

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


In higher observational type theory

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

R:A UBΔR:id U(A,B)P:id U(A,B)P:A UBR:A UBΔRR\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 UU is univalent if for all A,B:UA,B:U, the map

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

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

(A= UB)(A UB). (A=_U B) \simeq (A \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)(x_0:X) be any pointed type, and (𝒰,El)(\mathcal{U}, El) be a universe (with rules as I set out a couple of emails ago). Then X×𝒰X \times \mathcal{U} is again a universe, admitting all the same constructors as 𝒰\mathcal{U}: take

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

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

Now if 𝒰\mathcal{U} is univalent, and XX has non-trivial π 0\pi_0 (e.g. X=S 1X=S^1), then 𝒰(X×𝒰\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 𝒰 0𝒰 1\mathcal{U}_0 \rightarrow \mathcal{U}_1, we can consider 𝒰 0A×𝒰 1\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.

Mike Shulman added:

[N]ot only is X×𝒰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

Revision on June 9, 2022 at 17:00:03 by Anonymous?. See the history of this page for a list of all contributions to it.