nLab
univalence axiom

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Equality and Equivalence

Universes

Homotopy theory

Contents

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 universe Type, so that types can be considered as points of TypeType, then between two types we also have an identity type Paths Type(X,Y)Paths_{Type}(X,Y). The univalence axiom says that these two notions of “sameness” for types are the same. Morally, this says that Type behaves like an object classifier.

The name univalence (due to Voevodsky) comes from the following reasoning. A fibration or bundle p:EBp\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 pp 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). The univalence axiom then says that the canonical fibration over TypeType is univalent, for every fibration with small fibers is an essentially unique pullback of this one (while those with large fibers are not, they are pullbacks of the next higher Type 1Type_1).

Definition

We state univalence first in (intensional) type theory and then in its categorical semantics.

In the type theory

Let XX and YY be types. There is a canonically defined map from the identity type (X=Y)(X = Y) of paths (in Type) between them to the function type (XY)(X \stackrel{\simeq}{\to} Y) of equivalences in homotopy type theory between them. It can be defined by path induction, i.e. the eliminator for the identity types, by specifying that it takes the identity path 1 X:(X=X)1_X \colon (X=X) to the identity equivalence of XX.

Univalence: For any two types X,YX,Y, this map (X=Y)(XY)(X=Y)\to (X\simeq Y) is an equivalence.

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 (the Univalent Foundations Project.)

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:BE(b):Type b : B \vdash E(b) : Type

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

Then the dependent function type

b 1,b 2:B(E(b 1)E(b 2)):Type b_1, b_2 : B \vdash ( E(b_1) \to E(b_2)) : Type

is interpreted as the internal hom [,] 𝒞/ B×B[-,-]_{\mathcal{C}/_{B \times B}} in the slice category 𝒞/ B×B\mathcal{C}/_{B \times B} after extending EE to the context B×BB \times B by pulling back along the two projections p 1,p 2:B×BBp_1, p_2 : B \times B \to B, respectively. Hence this is interpreted as

[p 1 *E,p 2 *E] 𝒞/ B×B[E×B,B×E] 𝒞/ B×B𝒞/ B×B. [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 Δ B:BB×B\Delta_B : B \to B \times B in 𝒞\mathcal{C} as an object of 𝒞/ B×B\mathcal{C}/_{B \times B}. We would like to define a morphism

q:Δ B[E×B,B×E] 𝒞/ B×B. q \colon \Delta_B \to [E \times B , B \times E]_{\mathcal{C}/_{B \times B}} \,.

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

Δ B× 𝒞/ B×BE×BB×E \Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to B \times E

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

Δ B× 𝒞/ B×BE×BΔ B× 𝒞/ B×BB×E. \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Δ BB×Bπ 1B B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_1} B
BΔ BB×Bπ 2B B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_2} B

is the identity, both Δ B× 𝒞/ B×BE×B\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B and Δ B× 𝒞/ B×BB×E\Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E are isomorphic to EE; thus here we can take the identity? morphism.

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

B B I Δ B B×B \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 Δ B\Delta_B in the slice model category 𝒞 B×B\mathcal{C}_{B \times B}.

Since also [E×B,B×E] 𝒞/ B×B[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 q^\hat q in the diagram in 𝒞/ B×B\mathcal{C}/_{B \times B}

B q [E×B,B×E] 𝒞/ B×B q^ B I B×B=* 𝒞/ B×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 γB I\gamma \in B^I from one on just the identity paths id bBB Iid_b \in B \hookrightarrow B^I.

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

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

The fibration EBE \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:BEq(E)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 EXE \to X any fibration (Kan fibration) between fibrant objects (Kan complexes), consider first the simplicial set

[E×B,B×E] B×BsSet/ B×B [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×BsSet/_{B \times B}.

Notice that the vertices of this simplicial set over a fixed pair (b 1,b 2):*B×B(b_1, b_2) : * \to B \times B of vertices in BB form the set of morphisms E b 1E b 2E_{b_1} \to E_{b_2} between the fibers in sSetsSet.

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

* [E×B,B×E] B×B (b 1,b 2) B×B \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

E b 1×{b 2} {b 1}×E b 2 B×B \array{ E_{b_1} \times \{b_2\} &&\to&& \{b_1\} \times E_{b_2} \\ & \searrow && \swarrow \\ && B \times B }

in sSetsSet, which are precisely morphisms E b 1E b 2E_{b_1} \to E_{b_2}.

Let then

Eq(E)[E×B,B×E] B×BsSet/ B×B 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 Δ B:BB×B\Delta_B : B \to B \times B in sSetsSet, regarded as an object BsSet/ B×BB \in sSet/_{B \times B}, comes with a canonical morphism

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

The fibration EBE \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 12, 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).

Canonicity

It is currently open whether the univalence axiom enjoys canonicity in general, but for the special case of 1-truncated homotopy types (groupoids) (and two nested univalent universes and function extensionality), a “homotopical” sort of canonicity has been shown in (Shulman 12, section 13. Thus, in univalent homotopy 1-type theory with two universes, every term of type of the natural numbers is propositionally equal to a numeral.

The construction in (Shulman 12, section 13) uses Artin gluing of a suitable type-theoretic fibration category with the category Set and Grpd, respectively, effectively inducing canonicity from these categories. By (Shulman 12, remark 13.13) for this construction to generalize to untruncated univalent type theory, one seems to need a sufficiently strict global sections functor with values in some model for infinity-groupoids.

Notice that this sort of canonicity does not yet imply computational effectiveness?, which would require also an algorithm to extract that numeral from the given term. There may be such an algorithm, but so far attempts to extract one from the proof (or to give a constructive version of the proof, which would imply the existence of an algorithm) have not succeeded.

It is also a propositional canonicity, as opposed to the judgmental canonicity which many traditional type theories? enjoy. Another approach to canonicity for 1-truncated univalence can be found in (Harper-Licata), which involves modifying the type theory by adding more judgmental equalities, resulting in a judgmental canonicity. However, no algorithm for computing canonical forms has yet been given for this approach either.

Another approach to solving canonicity is to build a model for homotopy type theory inside a theory which is known to be constructive, such as ordinary (univalence-free) intensional type theory. Then one could induce canonicity, with an algorithm, from the latter to the former. This is the direction of the work of (Coquand-Huber 13), which models univalent homotopy type theory in constructive cubical sets, or the truncated form in constructive truncated simplicial sets. One might also try to construct the Hoffman-Streicher groupoid model in a constructive framework; Awodey and Bauer have done some work in this direction with an impredicative universe of h-sets.

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

References

Perhaps the earliest occurrence of the univalence axiom is in section 5.4 of

under the name “universe extensionality”. They formulate almost the modern univalence axiom; the only difference is the lack of a coherent definition of equivalence. The univalence axiom in its modern form was introduced and promoted by Vladimir Voevodsky around 2005. (?)

A quick survey is for instance in

An exposition is at

An accessible account of Voevodsky’s proof that the universal Kan fibration in simplicial sets is univalent is at

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

The HoTT-Coq code is at

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

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

This discusses canonicity of univalence in its section 13. Another approach to showing canonicity is (via cubical sets) in

On the issue of strict pullback of the univalent universe see

  • Univalent Foundations Mailing List, Quotients, March 2013

The computational interpretation of univalence / canonicity is discussed in

  • 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 Takeuti-Gandy Interpretation (pdf)

  • Thierry Coquand (with Marc Bezem and Simon Huber), Computational content of the Axiom of Univalence, September 2013 (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

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 Tarskian type universes, see there). Constructions of such a model in some very special cases are in Shulman12 above, and also in

For more references see homotopy type theory.

Revised on June 5, 2014 03:32:26 by Urs Schreiber (92.68.97.89)