nLab univalence axiom

Idea

In intensional type theory, identity types behave like path space objects; this viewpoint is called homotopy type theory. This induces furthermore a notion of homotopy fibers, hence of homotopy equivalences between types.

On the other hand, if type theory contains a type universe $U$, so that types can be considered as points of $U$, then between two types we also have an identity type $X =_U Y$. The univalence axiom says that these two notions of “sameness” for types are the same.

Extensionality principles like function extensionality, propositional extensionality (where $X$ and $Y$ are h-propositions), and univalence (“typal extensionality”) are naturally regarded as a stronger form of identity of indiscernibles. In particular, the consistency of univalence means that in Martin-Löf type theory without univalence, one cannot define any predicate that provably distinguishes isomorphic types; thus isomorphic types are “externally indiscernible”, and univalence incarnates that principle internally by making them identical.

The name univalence (due to Voevodsky, see Voevodsky 14 for etymology) comes from the following reasoning. A fibration or bundle $p\colon E\to B$ of some sort is commonly said to be universal if every other bundle of the same sort is a pullback of $p$ in a unique way (up to homotopy). Less commonly, a bundle is said to be versal if every other bundle is a pullback of it in some way, not necessarily unique. By contrast, a bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy). In the language of (∞,1)-category theory, a univalent bundle is an object classifier.

The univalence axiom does not literally say that anything is univalent in this sense. However, it is equivalent to saying that the canonical fibration over $U$ is univalent: every fibration with $U$-small fibers is an essentially unique pullback of this one. For a description of this equivalence, see section 4.8 of the HoTT Book (syntactically) and Gepner-Kock (semantically).

Univalence is a commonly assumed axiom in homotopy type theory, and is central to the proposal (Voevodsky) that this provides a natively homotopy theoretic foundation of mathematics (see at univalent foundations for mathematics).

Definition

We work in a dependent type theory with identity types, dependent product types, and dependent sum types.

There are multiple notions of equivalence types in dependent type theory, which can be used for a definition of univalence for a type universe $U$; these include

• the type of functions with contractible fibers;
• the type of functions with left and right homotopy inverses;
• the type of spans with contractible fibers;
• the type of multivalued partial functions which are single-valued and total and have contractible fibers;
• the type of one-to-one correspondences.

Let us assume an abstract family of equivalence types $\simeq$ with the property that for each type $A$ we have an identity equivalence $\mathrm{idequiv}(A) : A \simeq A$.

Fix a Tarski universe in the sense of a type $U$ with a type family $A : U \vdash T(A) \; \mathrm{type}$. There is a reflexive graph whose type of vertices is $U$, whose type of edges from $A : U$ to $B : U$ is

$$E(A,B) \coloneqq (T(A) \simeq T(B)),$$

and whose reflexivity map $r : (A : U) \to E(A,A)$ sends $A$ to $\mathrm{idequiv}(T(A))$. The reflexivity map induces, for $A,B : U$, a function

$$\mathrm{idtoequiv}(A, B) : (A =_U B) \to E(A,B)$$

defined using identity elimination with $\mathrm{idtoequiv}(A, A)(\mathrm{refl}_A) \coloneqq r(A)$.

The Tarski universe $(U,T)$ is univalent if the induced $(U,E,r)$ is a univalent as a reflexive graph, i.e., if one of the following conditions (equivalent by the fundamental theorem of identity types) holds:

1. For each $A:U$ the type of elements $B:A$ such that $E(A, B)$ is a contractible type.

   $$A:U \vdash \mathrm{ua}(A):\mathrm{isContr}\left(\sum_{B:U} E(A, B)\right)$$

2. For each $A:U$ and $B:U$, the function $\mathrm{idtoequiv}(A, B)$ is an equivalence of types

   $$A:U, B:U, \vdash \mathrm{ua}(A, B):\mathrm{isEquiv}(\mathrm{idtoequiv}(A, B))$$

3. There is a family of equivalences

   $$A:U, B:U \vdash \mathrm{ua}(A, B):(A =_U B) \simeq E(A, B)$$

4. $E$ is an identity system.

5. For each $A:U$ and $B:U$, the function $\mathrm{idtoequiv}(A, B)$ is a retraction:

   $$A:U, B:U \vdash \mathrm{ua}(A, B):E(A, B) \to (A =_U B)$$
   $$A:U, B:U, e:E(A, B) \vdash \mathrm{ua}\beta(A,B,e):\mathrm{idtoequiv}(A,B)(\mathrm{ua}(A,B)(e)) =_{E(A, B)} e$$

   (This is due to Daniel Licata in Licata 16.)

6. The family $E$ with its reflexivity map satisfies the universal property of the weak identity type $A =_U B$.

See fundamental theorem of identity types for proofs that these definitions are the same.

Decomposition

Assuming function extensionality, Ian Orton and Andrew Pitts (Orton and Pitts 19) showed that the univalence axiom can be simplified to the following special cases:

• $unit : A = \sum_{a:A} 1$
• $flip : (\sum_{a:A} \sum_{b:B} C(a,b)) = (\sum_{b:B} \sum_{a:A} C(a,b))$
• $contract: IsContr(A) \to (A=1)$
• $unit_\beta : coe(unit(a)) = (a,\star)$
• $flip_\beta : coe(flip(a,b,c)) = (b,a,c)$.

The proof constructs $ua(f): A=B$ (for $f:A\simeq B$) as the composite

$$A \overset{unit}{=} \sum_{a:A} 1 \overset{contract}{=} \sum_{a:A} \sum_{b:B} f a=b \overset{flip}{=} \sum_{b:B} \sum_{a:A} f a = b \overset{contract}{=} \sum_{b:B} 1 \overset{unit}{=} B$$

and uses $unit_\beta$ and $flip_\beta$ to compute that $coe(ua(f))(a) = f(a)$, hence by function extensionality $coe(ua(f)) = f$.

In the absence of function extensionality, this set of axioms is conjectured to be weaker than univalence. In addition, unlike the definitions above, this definition of univalence cannot be generalized to reflexive graphs.

Resizing the identity types

Due to the usual univalence axiom, we know that it is consistent to resize the identity types of a universe $U$ to be $U$-small.

Resizing the identity types allows for one more version of univalence, where we replace the equivalence of types between the identity type $A =_U B$ and the type of equivalences of the universe $A \simeq B$ in the univalence axioms with the identity type of the universe $U$, resulting in the statement that for all small types $A:U$ and $B:U$, there is an identification

$$\mathrm{ua}(A, B):(T(A) =_U T(B)) =_{U} (T(A) \simeq T(B))$$

This implies the usual version of univalence either through identification elimination, transport, and action on identifications for the identity type. On the other hand, the usual version of univalence implies this version of univalence by repeated applications of univalence.

Stricter variants of univalence

There are a few variants of univalence that are stricter than the usual axiom of univalence in that they use judgmental equalities and thus have to be expressed as (possibly multiple) inference rules instead of an axiom.

Using definitional isomorphism

There is a variant of univalence called definitional univalence or judgmental univalence, which says that for $x:A$ and $y:A$, the function $\mathrm{idtoequiv}(x, y)$ inductively defined in the previous section is a definitional isomorphism instead of an equivalence of types.

Unlike the case for the usual typal variant of univalence, where one can use an element of an equivalence type, we cannot use definitional isomorphisms as elements of definitional isomorphism types to express definitional univalence, because the large recursion principle of the interval type together with definitional isomorphism types implies equality reflection, which contradicts univalence.

Mike Shulman's model of higher observational type theory uses the type of $U$-small one-to-one correspondences for $R$ in definitional univalence.

Using judgmental equality of types

There is another variant of univalence where we replace the equivalence of types between the identity type $A =_U B$ and the type of equivalences of the universe $A \simeq B$ in the univalence axioms with judgmental equality of types, resulting in the statement that for all small types $A:U$ and $B:U$, one could judge that $(A =_U B) \equiv (A \simeq B) \; \mathrm{type}$. This implies the usual version of univalence through the structural rules for judgmental equality. The interpretation of such a univalent universe is that identifications of universes are equivalences of types.

Such univalent Tarski universes $(U, T)$ can be defined directly using inference rules instead of a judgmental equality, which say that identities $p:A =_U B$ are equivalences of types $A$ and $B$. Namely, given function types and the isEquiv type family, one could add rules to the type theory which says that $A =_U B$ behaves as an equivalence type:

Introduction rules:

$$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U \quad \Gamma, x:T[A/X] \vdash f:T[B/X] \quad \Gamma \vdash y:\mathrm{isEquiv}(f)}{\Gamma \vdash \mathrm{equiv}(f, y):A =_U B}$$

Elimination rules:

$$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U \quad \Gamma, x:T[A/X] \vdash f:T[B/X] \quad \Gamma, z:A =_U B \vdash C \; \mathrm{type} \quad \Gamma, x:T[A/X], f:T[B/X], y:\mathrm{isEquiv}(f) \vdash c:C[\mathrm{equiv}(f, y)/z]}{\Gamma, z:A =_U B \vdash \mathrm{ind}_{A =_U B}^C(c):C}$$

Computation rules:

$$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U \quad \Gamma, x:T[A/X] \vdash f:T[B/X] \quad \Gamma, z:A =_U B \vdash C \; \mathrm{type} \quad \Gamma, x:T[A/X], f:T[B/X], y:\mathrm{isEquiv}(f) \vdash c:C[\mathrm{equiv}(f, y)/z]}{\Gamma, x:T[A/X], f:T[B/X], y:\mathrm{isEquiv}(f) \vdash \beta_{A =_U B}^C(c):\mathrm{ind}_{A =_U B}^C(c)[\mathrm{equiv}(f, y)/z] =_{C[\mathrm{equiv}(f, y)/z]} c}$$

Uniqueness rules:

$$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U \quad \Gamma, x:T[A/X] \vdash f:T[B/X] \quad \Gamma, z:A =_U B \vdash C \; \mathrm{type} \quad \Gamma, x:T[A/X], f:T[B/X], y:\mathrm{isEquiv}(f) \vdash c:C[\mathrm{equiv}(f, y)/z] \quad \Gamma, z:A =_U B \vdash u:C \quad \Gamma, x:T[A/X], f:T[B/X], y:\mathrm{isEquiv}(f) \vdash i_\mathrm{in}(u):u[\mathrm{equiv}(f, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}{\Gamma, e:A =_U B \vdash \eta_{A =_U B}^C(c):u[e/z] =_{C[e/z]} \mathrm{ind}_{A =_U B}^C(c)[e/z]}$$

Weaker variants of univalence

Van den Berg (Van den Berg 20, Definition 2.13) gives a definition of univalent fibration in a path category which can be translated into type theory as follows:

$$A:U, B:U \vdash \mathrm{ua}(A, B): (A \simeq B) \to (A =_U B)$$

$$A:U, B:U, e : (A\simeq B), a: A \vdash \mathrm{ua}\beta(A,B,e,a) : \mathrm{coe}(\mathrm{ua}(A,B))(a) =_{B} e(a)$$

Notably, this variant of the univalence axiom can be unfolded and presented as a pair of inference rules in a type theory with only identity types, dependent sum types, and $U$. All uses of dependent product types can be replaced with hypothetical judgements.

Assuming dependent product types with function extensionality, this is equivalent to the univalence axiom (Licata 16). If function extensionality is not explicitly assumed, it is an open question whether it is equivalent to the univalence axiom (or equivalently, that it implies function extensionality). This is observed in Remark 4.6 of Swan 24. It is, however, equivalent to Orton and Pitts’ set of axioms.

In categorical semantics

Let $\mathcal{C}$ be a locally cartesian closed model category in which all objects are cofibrant.

By the categorical semantics of homotopy type theory, a dependent type

$$b : B \vdash E(b) \; \mathrm{type}$$

corresponds to a morphism $E \to B$ in $\mathcal{C}$ that is a fibration between fibrant objects.

Then the dependent function type

$$b_1, b_2 : B \vdash ( E(b_1) \to E(b_2)) \; \mathrm{type}$$

is interpreted as the internal hom $[-,-]_{\mathcal{C}/_{B \times B}}$ in the slice category $\mathcal{C}/_{B \times B}$ after extending $E$ to the context $B \times B$ by pulling back along the two projections $p_1, p_2 : B \times B \to B$, respectively. Hence this is interpreted as

$$[p_1^* E \, , \, p_2^* E]_{\mathcal{C}/_{B \times B}} \simeq [E \times B \, , \, B \times E]_{\mathcal{C}/_{B \times B}} \in \mathcal{C}/_{B \times B} \,.$$

Consider then the diagonal morphism $\Delta_B : B \to B \times B$ in $\mathcal{C}$ as an object of $\mathcal{C}/_{B \times B}$. We would like to define a morphism

$$q \colon \Delta_B \to [E \times B , B \times E]_{\mathcal{C}/_{B \times B}} \,.$$

in $\mathcal{C}/_{B \times B}$. By the defining (product $\dashv$ internal hom)-adjunction, it suffices to define a morphism

$$\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to B \times E$$

in $\mathcal{C}/_{B \times B}$. But now by the universal property of pullback, it suffices to define just in $\mathcal{C}_{/B}$ a morphism

$$\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to \Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E\,.$$

And since the composite pullback along either composite

$$B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_1} B$$

$$B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_2} B$$

is the identity, both $\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B$ and $\Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E$ are isomorphic to $E$; thus here we can take the identity morphism.

Now, using the path object factorization in $\mathcal{C}$

$$\array{ B &&\stackrel{\simeq}{\hookrightarrow}&& B^I \\ & {}_{\mathllap{\Delta_B}}\searrow && \swarrow_{\mathrlap{}} \\ && B \times B }$$

by an acyclic cofibration followed by a fibration, we obtain a fibrant replacement of $\Delta_B$ in the slice model category $\mathcal{C}_{B \times B}$.

Since also $[E \times B, B \times E]_{\mathcal{C}/_{B \times B}}$ is fibrant by the axioms on the locally cartesian closed model category $\mathcal{C}$, we have a lift $\hat q$ in the diagram in $\mathcal{C}/_{B \times B}$

$$\array{ B &\stackrel{q}{\to}& [E \times B, B \times E]_{\mathcal{C}/_{B \times B}} \\ \downarrow &{}^{\mathllap{\hat q}}\nearrow& \downarrow \\ B^I &\to& B \times B = *_{\mathcal{C}/_{B \times B}} } \,.$$

This lift is the interpretation of the path induction that deduces a map on all paths $\gamma \in B^I$ from one on just the identity paths $id_b \in B \hookrightarrow B^I$.

Finally, let $Eq(E) \hookrightarrow [E \times B , B \times E]_{\mathcal{C}/_{B \times B}}$ be the subobject on the weak equivalences (…), and observe that $q$ and $\hat q$ factor through this to give a morphism

$$\hat q : B^I \to Eq(E) \,.$$

The fibration $E \to B$ is univalent in $\mathcal{C}$ if this morphism is a weak equivalence. By the 2-out-of-3 property, of course, it is equivalent to ask that $q\colon B\to Eq(E)$ be a weak equivalence.

(…)

In simplicial sets

We specialize the general discussion above to the realization in $\mathcal{C} =$ sSet, equipped with the standard model structure on simplicial sets.

For $E \to B$ any fibration (Kan fibration) between fibrant objects (Kan complexes), consider first the simplicial set

$$[E \times B , B \times E]_{B \times B} \in sSet/_{B \times B}$$

defined as the internal hom in the slice category $sSet/_{B \times B}$.

Notice that the vertices of this simplicial set over a fixed pair $(b_1, b_2) : * \to B \times B$ of vertices in $B$ form the set of morphisms $E_{b_1} \to E_{b_2}$ between the fibers in $sSet$.

This is because – by the defining property of the internal hom in the slice and using that products in $sSet/_{B \times B}$ are pullbacks in $sSet$ – the horizontal morphisms of simplcial sets in

$$\array{ * &&\to&& [E \times B, B \times E]_{B \times B} \\ & {}_{\mathllap{(b_1,b_2)}}\searrow && \swarrow \\ && B \times B }$$

correspond bijectively to the horizontal morphisms in

$$\array{ E_{b_1} \times \{b_2\} &&\to&& \{b_1\} \times E_{b_2} \\ & \searrow && \swarrow \\ && B \times B }$$

in $sSet$, which are precisely morphisms $E_{b_1} \to E_{b_2}$.

Let then

$$Eq(E) \hookrightarrow [E \times B, B \times E]_{B \times B} \in sSet/_{B \times B}$$

be the full sub-simplicial set on those vertices that correspond to weak equivalences ((weak) homotopy equivalences).

By a similar consideration, one sees that the diagonal morphism $\Delta_B : B \to B \times B$ in $sSet$, regarded as an object $B \in sSet/_{B \times B}$, comes with a canonical morphism

$$B \to Eq(E) \,.$$

The fibration $E \to B$ is univalent, precisely when this morphism is a weak equivalence.

This appears originally as Voevodsky, def. 3.4

In simplicial presheaves

(…)

See (Shulman 15, UF 13)

(…)

Properties

Relation to function extensionality

The univalence axiom implies function extensionality.

A commented version of a formal proof of this fact can be found in (Bauer-Lumsdaine).

Relation to large elimination of the interval type

Mike Shulman proved in this MathOverflow post that given a type universe $U$, large elimination of the interval type for $U$-small types is equivalent to the univalence axiom for $U$.

Univalence and truncation levels

The univalence axiom can be used to deduce facts about the homotopy level of a univalent universe. For example (compare Theorem 7.1.11 in the HoTT Book):

Proposition

Let $n \ge -2$. If $A : U \vdash T(A) \; \mathrm{type}$ is a univalent Tarski universe such that $T(A)$ is an $n$-type for all $A : U$, then $U$ is an $(n+1)$-type.

In particular, if $U$ is any univalent universe, then the subtype $U^{\le n} \hookrightarrow U$ of $n$-types in $U$ is a univalent universe (see Rijke 22, Proposition 17.2.1) and an $(n+1)$-type.

Conversely, univalence can also imply lower bounds on the homotopy level of a universe. For example (Example 3.1.9 in the HoTT Book):

Proposition

Let $A : U \vdash T(A) \; \mathrm{type}$ be a univalent Tarski universe. If $U$ contains a type of booleans $\mathbf{2}$, then $U$ is not an h-set.

This follows from the fact that $\mathbf{2} \simeq \mathbf{2}$ is not an h-proposition; the role of $\mathbf{2}$ here can be played by any type with a non-trivial automorphism. Similarly, a univalent universe containing a circle type $S^1$ cannot be an h-groupoid, since $S^1 \simeq S^1$ is equivalent to $S^1 + S^1$.

Kraus and Sattler consider univalent universes containing other univalent universes and show:

Proposition

(Kraus–Sattler 15, Theorem 5.9) Let $U_i$ for $0 \le i \le n$ be a collection of univalent universes such that

• each $U_i$ is closed under dependent products, dependent sums, and identity types;
• each $U_{i+1}$ contains $U_i$ and all types in $U_i$;
• $U_0$ contains a type of booleans.

Then $U_n$ is not an $n$-type.

The above has consequences for the compatibility of univalence with uniqueness of identity proofs (UIP), or equivalently axiom K. By Proposition , UIP for all types is inconsistent with the existence of a univalent universe containing a type of booleans (or other type with a non-trivial automorphism). On the other hand, a type theory can consistently contain a univalent universe $U$ that satisfies UIP, in the sense that all types in $U$ are h-sets. The univalent universe in the Hofmann–Streicher groupoid model is of this kind, as is the subtype $U^{\le 0} \hookrightarrow U$ of h-sets in any univalent universe $U$.

Univalence and excluded middle

The principle of the excluded middle is consistent with the existence of any number of univalent universes. This is because the principle of excluded middle as traditionally defined in mathematics is about propositions or (-1)-truncated types.

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_A:\mathrm{isProp}(A) \to (A \vee (A \to \emptyset))}$$

Dependent type theory with excluded middle and universes satisfying the univalence axiom has semantics in boolean $(\infty, 1)$-toposes. A short proof of the excluded middle for the simplicial model can be found in Kapulkin–Lumsdaine 20.

However, there is a global choice axiom which is inconsistent with the existence of sufficiently non-trivial univalent universes (Escardó 12):

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{gc}_A:A + (A \to \emptyset)}$$

This is sometimes called “excluded middle” in the propositions as types interpretation of type theory, where the principle of excluded middle is reinterpreted so that types are used instead of mere propositions. But this principle is much stronger than the excluded middle for mere propositions, being of comparable strength to a choice operator and implying that every type is an h-set.

Canonicity and homotopy canonicity

If we extend Martin-Löf type theory with an axiom stating that a universe $U$ is univalent, we get a type theory which does not satisfy canonicity: there exist terms $\cdot \vdash N : \mathbb{N}$ in the empty context which are not judgmentally equal to any numeral. For example, if $\cdot \vdash e : \mathbb{N} \simeq \mathbb{N}$ is some equivalence (such as the identity equivalence), then $coe(ua(e))(0) : \mathbb{N}$ is such a term: although there is a typal equality $coe(ua(e))(0) = e(0)$, there is no judgmental equality. This can be shown using normalization for MLTT to compare the normal forms of $coe(ua(e))(0)$ and $e(0)$, treating judgments of the extended theory as judgments of MLTT with an extra hypothesis in the context stating that $U$ is univalent.

Despite this, it is possible to extend Martin-Löf type theory with univalent universes further to create a theory that does enjoy canonicity. Cubical type theories are examples of such theories which can support an infinite hierarchy of univalent universes; see cubical type theory for more details. An earlier canonicity result for a type theory with one univalent universe where every type is an h-groupoid was proven by Harper and Licata (Harper and Licata 12).

A separate question is whether Martin-Löf type theory extended with one or more univalent universes satisfies the weaker homotopy canonicity property. In 2019, Christian Sattler and Krzysztof Kapulkin announced a proof of this result; the proof has been described in talks (Sattler 19) but has not appeared publicly. Rafaël Bocquet gives a second proof of homotopy canonicity in a preprint (Bocquet 23). Earlier homotopy canonicity results for truncated versions of univalent type theory were shown by Shulman (Shulman 15, Section 13). Shulman 15, Theorem 13.7 shows that Martin-Löf type theory with

• one univalent universe $U_0$,
• a “strong homotopy” natural number type (not contained in $U_0$),
• function extensionality, and
• an axiom asserting that every type is an h-set

has homotopy canonicity. Shulman 15, Theorem 13.12 shows that Martin-Löf type theory with

• two nested univalent universes $U_0 : U_1$,
• a “strong homotopy” natural number type contained in $U_1$,
• function extensionality,
• an axiom asserting that every type is a h-groupoid

has homotopy canonicity. The proofs use Artin gluing of a suitable type-theoretic fibration category with the categories Set and Grpd, respectively, effectively inducing canonicity from these categories. By (Shulman 15, remark 13.13), for this construction to generalize to a univalent type theory without a global truncation axiom, one seems to need a sufficiently strict global sections functor with values in some model for infinity-groupoids. The proofs in Sattler 19 and Bocquet 23 address this problem in different ways.

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.

Mike Shulmanadded:

[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.

Univalence axiom without universes

In dependent type theory with type variables, presented using a single type judgment and with identity types between types, it is possible to state the univalence axiom without any type universes.

The univalence axiom states that the function

$$\mathrm{idtoequiv}(A, B):(A = B) \to (A \simeq B)$$

inductively defined by

$$\mathrm{idtoequiv}(A, A, \mathrm{refl}(A)) \coloneqq \mathrm{id}_A$$

is an equivalence of types for all types $A$ and $B$,

$$\mathrm{isEquiv}(\mathrm{idtoequiv}(A, B))$$

where $\mathrm{id}_A \coloneqq \lambda x:A.x$ is the identity function on the type $A$. This is given by the following axiom:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, A \; \mathrm{type}, B \; \mathrm{type} \vdash \mathrm{ua}(A, B):\mathrm{isEquiv}(\lambda p:A = B.\mathrm{idtoequiv}(A, B, p))}$$

In impredicative polymorphism, this is also given by the following axiom:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{ua}:\Pi A.\Pi B.\mathrm{isEquiv}(\lambda p:A = B.\mathrm{idtoequiv}(A, B, p))}$$

Unlike the other presentation of dependent type theory in terms of universes, in this presentation of dependent type theory with a type judgment and type variables, it is consistent to assume both the univalence axiom and an axiom of set truncation like UIP or axiom K, since here there is no universe, provided one doesn’t have any higher types, such as the circle type.

There is one other version of univalence, where we replace the equivalence of types between the identity type $A = B$ and the type of equivalences of the universe $A \simeq B$ in the univalence axioms with the identity type, resulting in the statement that for all small types $A$ and $B$, there is an identification $\mathrm{ua}(A, B):(A = B) = (A \simeq B)$.

This implies the usual version of univalence either through identification elimination, transport, and action on identifications for the identity type.

Related concepts

• resizing axiom

• univalent foundations

• univalent type theory

• extensionality

  • Univalence is closely related to the “completeness” condition in the theory of Segal spaces/semi-Segal spaces. See complete Segal space/_complete semi-Segal space.

  • propositional extensionality

• equivalence induction

• contrary to univalence is the axiom UIP

• directed univalence axiom

• axiom of relativity

• identity type between types

References

For more references see also at homotopy type theory.

History

Arguably, the earliest occurrence of a version of the univalence axiom is due – under the name “universe extensionality” – to:

• Martin Hofmann, Thomas Streicher, Section 5.4 of: The groupoid interpretation of type theory, in: Giovanni Sambin et al. (eds.), Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19-21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36 (1998) 83-111 [ISBN:9780198501275, ps, pdf]

Strictly speaking, univalence for propositions has a much longer pedigree, this that can and does hold even in set-level foundations, but this is the earliest version of univalence that goes beyond what is possible there. However, their universe extensionality axiom is stated only for h-sets, and would be incorrect if naively generalized to higher types. The correct statement that works for higher types requires a better definition of equivalences in homotopy type theory (see there for details), which Voevodsky was the first to give.

For comments on the early history see also:

• Thorsten Altenkirch, Martin Hofmann’s contributions to type theory: Groupoids and univalence, Mathematical Structures in Computer Science 31 9 (2021) 953-957 [doi:10.1017/S0960129520000316]

It is this notion of equivalence in homotopy type theory which was fixed in

• Vladimir Voevodsky, p. 8, 10-11 of: Univalent Foundations Project (2010) [pdf, pdf]

ever since the univalence axiom is widely attributed to Voevodsky. Earlier documentation of the univalence axiom in modern form is hard to come by:

The first technical understanding of (the semantics of) univalence in simplicial sets seems to be due to:

• Aldridge Bousfield, email to VV from 01 May 2006 10:10:30 CDT $[$screenshot$]$

(which 6 years later came to be written up as Kapulkin, Lumsdaine & Voevodsky12 and another 10 years later was published as Kapulkin & Lumsdaine 2021).

The first mentioning by Voevodsky of the term “univalence” by email is 3.5 years later, from Dec. 30 2009 (according to Grayson, Oct. 2017).

The earliest recorded statement of the univalence axiom by Voevodsky’s hand date may be Voevodsky (2010), p. 11

see also:

• Vladimir Voevodsky, The equivalence axiom and univalent models of type theory (Talk at CMU on February 4, 2010) (arXiv:1402.5556)

• Vladimir Voevodsky, Univalent foundations – new type-theoretic foundations of mathematics, talk at IHP 2014 (pdf)

Later in:

• Vladimir Voevodsky, The Origins and Motivations of Univalent Foundations, IAS Institute Letter Summer 2014

appears the claim that:

have been working on the ideas that led to the discovery of univalent models since 2005 and gave the first public presentation on this subject at Ludwig-Maximilians-Universität München in November 2009.

A comprehensive discussion finally appears in the textbook:

• Univalent Foundations Project, p. 4 & Sec. 2.10 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

Voevodsky’s (Bousfield’s) original idea for the universal Kan fibration as a model for a univalent universe in simplicial sets/$\infty$-groupoids was eventually published as:

• Chris Kapulkin, Peter LeFanu Lumsdaine, The Simplicial Model of Univalent Foundations (after Voevodsky), Journal of the European Mathematical Society 23 (2021) 2071–2126 $[$arXiv:1211.2851, doi:10.4171/jems/1050$]$

Exposition and survey

• Peter Aczel, On Voevodsky’s Univalence Axiom, talk at Third European Set Theory Conference (2011) [pdf, pdf]

  (in view of the structure identity principle)

• Mike Shulman, Homotopy type theory, IV [blog post]

Additional definition of univalent universes appeared in section 17.1 of

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press [arXiv:2212.11082]

Variants

On a superficially weaker but equivalent statement of univalence (also recorded in Orton and Pitts 19, Theorem 3.5):

• Dan Licata, weak univalence with “beta” implies full univalence (2016) [web]

On a reduction of the univalence axiom to special cases:

• Ian Orton, Andrew M. Pitts, Decomposing the Univalence Axiom, in 23rd International Conference on Types for Proofs and Programs (TYPES 2017), Leibniz International Proceedings in Informatics (LIPIcs) 104 (2019) 6:1–6:19 [arXiv:1712.04890, doi:10.4230/LIPIcs.TYPES.2017.6]

On a possibly weaker variant of univalence:

• Benno van den Berg, Section 2.3 in Univalent polymorphism, Annals of Pure and Applied Logic 171 (2020) 102793 [arXiv:1803.10113, doi:10.1016/j.apal.2020.102793]

• Andrew Swan, Section 4 in A categorical formulation of Kraus’ paradox (2024) [arXiv:2403.17961]

Some details regarding the univalence axiom for weakly Tarski universes appeared on MathOverflow in:

• Madeleine Birchfield, Valery Isaev, Univalence for weakly Tarski universes, MathOverflow, [web]

Some discussion about the univalence axiom in dependent type theory with type variables occurs in:

• Dependent Type Theory vs Polymorphic Type Theory, Category Theory Zulip [web]

Semantics

An accessible account of Voevodsky’s proof (following Bousfield 06) that the universal Kan fibration in simplicial sets is univalent:

• Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Univalence in simplicial sets [arXiv:1203.2553]

A quick elegant proof of the object classifier/universal associated infinity-bundle in simplicial sets/$\infty$-groupoids is in

• Ieke Moerdijk (notes by Chris Kapulkin), Fiber bundles and univalence [pdf]

A study of the semantic side of univalence in (infinity,1)-toposes, as well as further cases of locally cartesian closed (infinity,1)-categories is in

• David Gepner, Joachim Kock, Univalence in locally cartesian closed infinity-categories, Forum Mathematicum 29 3 (2016) 617–652 [arXiv:1208.1749, doi:10.1515/forum-2015-0228]

This does not yet show that the univalence axiom in its usual form holds in the internal type theory of (infinity,1)-toposes, however, due to the lack of a (known) sufficiently strict model for the object classifier. (But it works with Tarski universes, see there and type universes). Constructions of such a model in some very special cases are in Shulman12 below, and also in

• Michael Shulman, The univalence axiom for elegant Reedy presheaves, Homology, Homotopy and Applications 17 2 (2015) 81–106 [arXiv:1307.6248, doi:10.4310/HHA.2015.v17.n2.a6]

• Denis-Charles Cisinski, Univalent universes for elegant models of homotopy types [arXiv:1406.0058]

Finally, full proof that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes [arXiv:1904.07004)]

On the issue of strict pullback of the univalent universe see

• Univalent Foundations Mailing List, Quotients, March 2013

On an interpretation of a univalent universe at the strength of finite order arithmetic:

• Colin McLarty, A univalent universe in finite order arithmetic [arXiv:1412.6714]

Properties

Coexistence of univalence with the excluded middle for mere propositions:

• Chris Kapulkin, Peter LeFanu Lumsdaine, The Law of Excluded Middle in the Simplicial Model of Type Theory, Theory and Applications of Categories 35 40 (2020) 1546–1548 [arXiv:2006.13694, doi:10.70930/tac/ykx24t1x]

Incompatibility of univalence with the excluded middle for all types (not only mere propositions) follows from:

• Martín Escardó, Rice’s Theorem for the Martin-Lof universe (2012) [Agda, mailing list discussion]

On lower bounds on the truncation levels of univalent universes:

• Nicolai Kraus, Christian Sattler, Higher Homotopies in a Hierarchy of Univalent Universes, ACM Transactions on Computational Logic 16 2 (2015) 1–12 [arXiv:xxxx.yyyyy, doi:10.1145/2729979]

Proof assistants

Implementation of univalence in proof assistants:

in Agda:

• Martín Escardó, Voevodsky’s univalence axiom, §3.11 in: Introduction to Univalent Foundations of Mathematics with Agda [arXiv:1911.00580, webpage]

cubical Agda:

• 1lab, Univalence

in Coq:

• HoTT/HoTT theories/Types/Universe.v

• HoTT/HoTT theories/UnivalenceAxiom.v

A guided walk through the formal proof that univalence implies functional extensionality is at

• Andrej Bauer, Peter LeFanu Lumsdaine, Oberwolfach HoTT-Coq tutorial

Application of univalence to proof transfer:

• Cyril Cohen, Enzo Crance, Assia Mahboubi, Trocq: Proof Transfer for Free, With or Without Univalence, in: Programming Languages and Systems. ESOP 2024, Lecture Notes in Computer Science 14576, Springer (2024) [arXiv:2310.14022, doi:10.1007/978-3-031-57262-3_10]

Canonicity and computational interpretations

A discussion of univalence in categories of diagrams over an inverse category with values in a category for which univalence is already established is discussed in

• Michael Shulman, Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science 25 (2015) 1203–1277 [arXiv:1203.3253, doi:10.1017/S0960129514000565]

This discusses homotopy canonicity of univalence in its section 13. A proof of homotopy canonicity was presented in

• Christian Sattler (with Chris Kapulkin), Homotopy Canonicity, Talk at HoTT-UF (2019) [abstract, program]

Another proof of homotopy canonicity is the subject of

• Rafaël Bocquet, Strict Rezk completions of models of HoTT and homotopy canonicity (2023) [arXiv:2311.05849]

Bocquet’s introduction includes a sketch of Sattler and Kapulkin’s proof strategy.

Another approach to showing canonicity is (via cubical sets) in

• Marc Bezem, Thierry Coquand, Simon Huber, A model of type theory in cubical sets, in 19th International Conference on Types for Proofs and Programs (TYPES 2013), Leibniz International Proceedings in Informatics (LIPIcs) 26 (2014) 107–128 [doi:10.4230/LIPIcs.TYPES.2013.107, pdf, Haskell code, discussion]

• Marc Bezem, Thierry Coquand, Simon Huber, The univalence axiom in cubical sets, Journal of Automated Reasoning 63 (2019) 159–171 [arXiv:1710.10941, doi:10.1007/s10817-018-9472-6]

The computational interpretation of univalence / canonicity is discussed in

• Dan Licata (with Robert Harper), Computing with Univalence, talk at Workshop on Higher Dimensional Algebra, Categories and Types (2012) [abstract (archived), slides]

• Robert Harper, Daniel Licata, Canonicity for 2-dimensional type theory, in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL) (2012) 337–348 [doi:10.1145/2103656.2103697, pdf]

• Daniel Licata, The computational interpretation of HoTT (in 2D), talk at UF-IAS-2012 [video]

• Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011 [pdf]

• Bruno Barras, Thierry Coquand, Simon Huber, A Generalization of the Takeuti-Gandy Interpretation, Mathematical Structures in Computer Science 25 Special Issue 5 (2015) 1071–1099 [pdf, doi:10.1017/S0960129514000504]

and realized in cubical type theory in

• Thierry Coquand (with Marc Bezem and Simon Huber), Computational content of the Axiom of Univalence, September 2013 [pdf]

• Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, in 21st International Conference on Types for Proofs and Programs (TYPES 2015), Leibniz International Proceedings in Informatics (LIPIcs) 69 (2018) 5:1–5:34 [arxiv:1611.02108, hal-01378906, doi:10.4230/LIPIcs.TYPES.2015.5]

Proof of the univalence axiom from large elimination of the interval type relativizing to the type universe:

• How to formulate the univalence axiom without universes? (web)