|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
of all homotopy types
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 , then between two types we also have an identity type . 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 of some sort is commonly said to be universal if every other bundle of the same sort is a pullback of 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 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 ).
Let and be types. There is a canonically defined map from the identity type of paths (in Type) between them to the function type 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 to the identity equivalence of .
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.)
Let be a locally cartesian closed model category in which all objects are cofibrant.
Consider then the diagonal morphism in as an object of . We would like to define a morphism
And since the composite pullback along either composite
is the identity, both and are isomorphic to ; thus here we can take the identity morphism.
Now, using the path object factorization in
by an acyclic cofibration followed by a fibration, we obtain a fibrant replacement of in the slice model category .
This lift is the interpretation of the path induction that deduces a map on all paths from one on just the identity paths .
Finally, let be the subobject on the weak equivalences (…), and observe that and factor through this to give a morphism
The fibration is univalent in if this morphism is a weak equivalence. By the 2-out-of-3 property, of course, it is equivalent to ask that be a weak equivalence.
Notice that the vertices of this simplicial set over a fixed pair of vertices in form the set of morphisms between the fibers in .
correspond bijectively to the horizontal morphisms in
in , which are precisely morphisms .
By a similar consideration, one sees that the diagonal morphism in , regarded as an object , comes with a canonical morphism
The fibration is univalent, precisely when this morphism is a weak equivalence.
This appears originally as Voevodsky, def. 3.4
The univalence axiom implies function extensionality.
A commented version of a formal proof of this fact can be found in (Bauer-Lumsdaine).
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.
contrary to univalence is the axiom UIP
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
A guided walk through the formal proof that univalence implies functional extensionality is at
On the issue of strict pullback of the univalent universe see
The computational interpretation of univalence / canonicity is discussed 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.