natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
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 $Type$, then between two types we also have an identity type $Paths_{Type}(X,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) 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 $Type$ is univalent: 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_1$). 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).
We work in a dependent type theory with identity types, function types, dependent product types, product types, and dependent sum types.
While traditionally in dependent type theory, Russell universes $U$ are considered to be distinct from Tarski universes $(U, T)$, in this article, we define a Russell universe to be a Tarski universe $(U, \!\,)$ whose type reflector type family is represented by a zero-width whitespace character $\!\,$ instead of some other symbol $T$. Thus, we can use the more general notion of Tarski universe throughout the article.
Given a universe $U$, there are multiple notions of equivalence of $U$-small types which can be used in the definition of univalence, such as functions with contractible fibers and one-to-one correspondences.
In any dependent type theory, given types $A$ and $B$ and a function $f:A \to B$, $f$ is an equivalence if for all $b:B$, the fiber of $f$ at $b$ is contractible:
Now, let $(U, T)$ is a Tarski universe. The univalence axiom states that the transport function $\mathrm{trans}^T(A, B)$, defined by identification elimination which take the reflexive identification $\mathrm{refl}_U(A):A =_U A$ to the identity equivalence $\mathrm{id}_{T(A)}:T(A) \simeq T(A)$, is an equivalence of types for all $A:U$ and $B:U$
If $(U, \!\,)$ is a Russell universe, transport across the zero-width whitespace character type family $\!\,$ is typically written as $\mathrm{idtoequiv}(A, B)$:
In any dependent type theory with a Tarski universe $(U, T)$, we define a correspondence $R:T(A) \times T(B) \to U$ to be a one-to-one correspondence as:
and we define the type of one-to-one correspondences from $A$ to $B$ in $U$ as
A universe $U$ is univalent if for all $A:U$ and $B:U$, the canonical map
from the identity type $A =_U B$ to the type of one-to-one correspondences $A \simeq_U B$, defined by identification elimination which take the reflexive identification $\mathrm{refl}_U(X):X =_U X$ to the identity one-to-one correspondence $\Delta_X:X \simeq X$, is an equivalence of types
In this section, we abbreviate each of the above notions of equivalence ($A \simeq_U B$ or $T(A) \simeq T(B)$) as $A \simeq B$.
The univalence axiom proper says that the canonical map $coe:(X=Y)\to (X\simeq Y)$ is an equivalence. However, there are several seemingly-weaker (and therefore often easier to verify) statements that are equivalent to this, such as:
For any type $X$, the type $\sum_{Y:U} (X\simeq Y)$ is contractible. This follows since then the map on total spaces from $\sum_{Y:U} (X=Y)$ to $\sum_{Y:U} (X\simeq Y)$ induced by $coe$ is an equivalence, hence a fiberwise equivalence $(X=Y) \simeq (X\simeq Y)$.
For any $X,Y:U$ we have a map $ua:(X\simeq Y) \to (X=Y)$ such that $coe(ua(f)) = f$. This exhibits $X\simeq Y$ as a retract of $X=Y$, hence $\sum_{Y:U} (X\simeq Y)$ as a retract of the contractible type $\sum_{Y:U} (X=Y)$, so it is contractible. This was observed by Dan Licata.
Ian Orton and Andrew Pitts showed here that assuming function extensionality, this can be further simplified to the following special cases:
The proof constructs $ua(f): A=B$ (for $f:A\simeq B$) as the composite
and uses $unit_\beta$ and $flip_\beta$ to compute that $coe(ua(f))(a) = f(a)$, hence by function extensionality $coe(ua(f)) = f$.
There are also stricter versions 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 some notion of equality, such as judgmental equality, propositional equality, and typal equality.
In any dependent type theory with judgmental equality, given a type universe $U$, one could replace the equivalence of types in the definition of univalence with a judgmental equality of types. This results in judgmental univalence, which states that for all small types $A:U$ and $B:U$, one could judge that $(A =_U B) \equiv (A \simeq B) \; \mathrm{type}$.
Similarly, in the context of any logic over type theory with propositional equality, given a type universe $U$, one could replace the equivalence of types in the definition of univalence with a propositional equality of types. This results in propositional univalence, which states that for all small types $A:U$ and $B:U$, $(A =_U B) \equiv (A \simeq B) \; \mathrm{true}$.
Finally, if we are working inside a Tarski universe $(\mathcal{V}, \mathcal{T})$, then given an internal Tarski universe $U:\mathcal{V}$ with $T:\mathcal{T}(U) \to \mathcal{V}$, one could replace the equivalence of types in the definition of univalence with a typal equality of types. This results in typal univalence, which states that for all small types $A:\mathcal{T}(U)$ and $B:\mathcal{T}(U)$, there is an identification $\mathrm{ua}(A, B):(T(A) =_U T(B)) =_{\mathcal{V}} (T(A) \simeq_{\mathcal{V}} T(B))$.
Each of these imply the usual versions of univalence either through the structural rules for judgmental equality and propositional equality, or through identification elimination, transport, and action on identifications for typal equality.
We shall call these forms of univalence Shulman univalence because it first appeared in Mike Shulman‘s model of higher observational type theory.
Given a type universe $U$, there is a canonical function
for all $A:U$ and $B:U$.
Suppose we are working in a dependent type theory with judgmental equality of terms $\equiv$. Then $U$ is judgmentally Shulman univalent if for all $A:U$ and $B:U$ there is a function $\mathrm{ua}(A, B):(A \simeq B) \to (A =_U B)$ such that for all equivalences $R:A \simeq B$, one could judge that $\mathrm{idtoequiv}(A, B)(\mathrm{ua}(A, B)(R)) \equiv R$.
Now, suppose we are working in the framework of logic over type theory, where our dependent type theory has propositional equality of terms $\equiv$. Then $U$ is propositionally Shulman univalent if there is a function $\mathrm{ua}(A, B):(A \simeq B) \to (A =_U B)$ for all $A:U$ and $B:U$ such that for all equivalences $R:A \simeq B$, the proposition $\mathrm{idtoequiv}(A, B)(\mathrm{ua}(A, B)(R)) \equiv R$ is true.
Suppose the Tarski universe $U$ has
We assume the weakest notion of Tarski universe, where the type reflection $T(A)$ of each $A:U$ is only equivalent to the external type, since (judgmentally, propositionally, typally) strict Tarski universes are weakly Tarski universes, because the judgmental equality and propositional equality imply equivalence of types by the structural rules for judgmental and propostional equality, and typal equality in a type universe of types imply equivalence of types by identification elimination, transport, and action on identifications.
This allows us to define the internal type of equivalences $A \simeq_U^\mathrm{in} B$, internal to the universe $U$, which comes with a canonical equivalence of types
This implies that the equivalence $T(A) \simeq T(B)$ is $U$-small, and transport being an equivalence then implies that in any universe $U$ which is closed under function types, dependent product types, and dependent sum types, for all $A:U$ and $B:U$, the identity type $A =_U B$ is $U$-small.
The internal univalence axiom states that the canonical function
is an equivalence of types
This is not definable for strongly predicative type universes, since strongly predicative type universes are by definition not closed under dependent product types.
In addition, the internal and external versions of univalence imply each other. In order to show that the two axioms imply each other, we need to show that there is an identification
for all identifications $p:A =_U B$. By the J rule it is enough to show that $\mathrm{canonical}_\simeq(A, A)$ maps the identity equivalence of $T(A \simeq_U^\mathrm{in} A)$ to the identity equivalence in $T(A) \simeq T(A)$. Since the identity equivalence in $T(A \simeq_U^\mathrm{in} A)$ is just the identity function $\mathrm{canonical}_\simeq^{-1}(A, A)(\lambda x.x)$ the above statement is always true. Thus, if the universe is closed under identity types, dependent product types, and dependent sum types the two univalence axioms imply each other and both define the same notion of univalent universe.
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
corresponds to a morphism $E \to B$ in $\mathcal{C}$ that is a fibration between fibrant objects.
Then the dependent function 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
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
in $\mathcal{C}/_{B \times B}$. By the defining (product $\dashv$ internal hom)-adjunction, it suffices to define a morphism
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
And since the composite pullback along either composite
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}$
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}$
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
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.
(…)
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
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
correspond bijectively to the horizontal morphisms in
in $sSet$, which are precisely morphisms $E_{b_1} \to E_{b_2}$.
Let then
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
The fibration $E \to B$ is univalent, precisely when this morphism is a weak equivalence.
This appears originally as Voevodsky, def. 3.4
(…)
See (Shulman 12, UF 13)
(…)
The univalence axiom implies function extensionality.
A commented version of a formal proof of this fact can be found in (Bauer-Lumsdaine).
In this section we assume that the universe is a Tarski universe. Axiom K states that for all $A:U$ the type $T(A)$ is a set. This means the type reflection of the internal equivalences $T(A \simeq_U B)$ is an h-set, and the univalence axiom then implies that $U$ is an h-groupoid.
It is frequently stated that the univalence axiom and axiom K are inconsistent with each other. However, this is only true if the Tarski universe $U$ has internal univalent Tarski universes $V:U$ where the type $T(V)$ has terms $A:T(V)$ such that $T_V(A)$ is an h-set which is not an h-proposition, such as the booleans type. As a result, $T(V)$ can be proven to not be a set, causing axiom K for $U$ to be inconsistent with the existence of $V:U$ and univalence.
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), homotopy 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. A proof of the full result has been announced by Christian Sattler and Krzysztof Kapulkin (Sattler 19).
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.
Canonicity has been proved for cubical type theory.
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.
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.
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.
contrary to univalence is the axiom UIP
directed univalence axiom?
The earliest occurrence of the univalence axiom is due to:
under the name “universe extensionality”. These authors formulate almost the modern univalence axiom; the only difference is the lack of a coherent definition of equivalence.
The univalence axiom has famously come to be attributed to Vladimir Voevodsky, though early documentation is hard to come by.
The first technical understanding of univalence in simplicial sets seems to be due to:
(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 accounts by Voevodsky’s hand date from 2010, but the un-iniated may have trouble recognizing the univalence axiom here:
Vladimir Voevodsky, Section 4 of: Univalent Foundations Project, 2010 (pdf)
Vladimir Voevodsky, The equivalence axiom and univalent models of type theory (Talk at CMU on February 4, 2010) (arXiv:1402.5556)
Later in:
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 clean and comprehensive discussion finally appears in the textbook:
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:
Exposition and survey:
Peter Aczel, On Voevodsky’s univalence axiom (pdf)
Mike Shulman, Homotopy type theory, IV (blog post)
An accessible account of Voevodsky’s proof (following Bousfield 06) that the universal Kan fibration in simplicial sets is univalent:
A quick elegant proof of the object classifier/universal associated infinity-bundle in simplicial sets/$\infty$-groupoids is in
See also
A guided walk through the formal proof that univalence implies functional extensionality is at
Some details regarding the univalence axiom for weakly Tarski universes appeared on MathOverflow in:
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
A proof of canonicity is presented in the talk
On the issue of strict pullback of the univalent universe see
The computational interpretation of univalence / canonicity is discussed in
Dan Licata, Robert Harper, Computing with Univalence (2012) (pdf)
Robert Harper, Daniel Licata, Canonicity for 2-dimensional type theory (2011) (pdf)
Daniel LicataThe 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)
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 (pdf)
Marc Bezem, Thierry Coquand, Simon Huber, The univalence axiom in cubical sets (arXiv:1710.10941)
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 Tarski universes, see there and type universes). Constructions of such a model in some very special cases are in Shulman12 above, and also in
Michael Shulman, The univalence axiom for elegant Reedy presheaves, arXiv:1307.6248.
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:
For more references see homotopy type theory.
Last revised on November 21, 2022 at 01:07:43. See the history of this page for a list of all contributions to it.