ncatlab.org

univalence axiom (changes) in nLab

Showing changes from revision #108 to #109: Added | Removed | Changed

Context

Type theory

natural deduction metalanguage, practical foundations

judgement
hypothetical judgement, sequent
- antecedents ⊢\vdash consequent, succedents

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

calculus of constructions

syntax object language

theory, axiom
proposition/type (propositions as types)
definition/proof/program (proofs as programs)
theorem

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

logic	set theory (internal logic of)	category theory	type theory
proposition	set	object	type
predicate	family of sets	display morphism	dependent type
proof	element	generalized element	term/program
cut rule		composition of classifying morphisms / pullback of display maps	substitution
introduction rule for implication		counit for hom-tensor adjunction	lambda
elimination rule for implication		unit for hom-tensor adjunction	application
cut elimination for implication		one of the zigzag identities for hom-tensor adjunction	beta reduction
identity elimination for implication		the other zigzag identity for hom-tensor adjunction	eta conversion
true	singleton	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	empty set	initial object	empty type
proposition, truth value	subsingleton	subterminal object/(-1)-truncated object	h-proposition, mere proposition
logical conjunction	cartesian product	product	product type
disjunction	disjoint union (support of)	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	function set (into subsingleton)	internal hom (into subterminal object)	function type (into h-proposition)
negation	function set into empty set	internal hom into initial object	function type into empty type
universal quantification	indexed cartesian product (of family of subsingletons)	dependent product (of family of subterminal objects)	dependent product type (of family of h-propositions)
existential quantification	indexed disjoint union (support of)	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
logical equivalence	bijection set	object of isomorphisms	equivalence type
	support set	support object/(-1)-truncation	propositional truncation/bracket type
		n-image of morphism into terminal object/n-truncation	n-truncation modality
equality	diagonal function/diagonal subset/diagonal relation	path space object	identity type/path type
completely presented set	set	discrete object/0-truncated object	h-level 2-type/set/h-set
set	set with equivalence relation	internal 0-groupoid	Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
	equivalence class/quotient set	quotient	quotient type
induction		colimit	inductive type, W-type, M-type
higher induction		higher colimit	higher inductive type
-		0-truncated higher colimit	quotient inductive type
coinduction		limit	coinductive type
	preset		type without identity types
	set of truth values	subobject classifier	type of propositions
domain of discourse	universe	object classifier	type universe
modality		closure operator, (idempotent) 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

homotopy levels

semantics

Equality and Equivalence

equivalence

principle of equivalence

univalence

equation

Universes

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…

models: topological, simplicial, localic, …

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.

Extensionality principles like function extensionality, propositional extensionality (where XX and YY 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:E→Bp\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). 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 TypeType 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 1Type_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).

Definition

We work in a dependent type theory with identity types, function types, dependent product types, 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 UU; these include

definitional isomorphism types
various notions of (weak) equivalence types
- the type of functions with contractible fibers
- 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
type of UU-small equivalences, given a type universe UU and a definition of equivalence above

Let us assume an arbitrary notion of equivalence type ≃ 0\simeq_0. Every Russell universe UU is a reflexive graph with the graph type family R(A,B)R(A, B) defined as R(A,B)≔A≃ 0BR(A, B) \coloneqq A \simeq_0 B and the function idtofam(A,B)\mathrm{idtofam}(A, B) is defined as

idtofam(A,B)≔idtoequiv(A,B)\mathrm{idtofam}(A, B) \coloneqq \mathrm{idtoequiv}(A, B)

Similarly, every Tarski universe UU with universal type family TT is a reflexive graph with the graph type family R(A,B)R(A, B) defined as R(A,B)≔T(A)≃ 0T(B)R(A, B) \coloneqq T(A) \simeq_0 T(B) and the function idtofam(A,B)\mathrm{idtofam}(A, B) is defined as

idtofam(A,B)≔transport T(A,B)\mathrm{idtofam}(A, B) \coloneqq \mathrm{transport}^T(A, B)

And finally, every Tarski universe UU with type of terms TT and function typeof:T→U\mathrm{typeof}:T \to U is a reflexive graph with the graph type family R(A,B)R(A, B) defined as

R(A,B)≔(∑ t:TtypeOf(t)= UA)≃(∑ t:TtypeOf(t)= UB)R(A, B) \coloneqq \left(\sum_{t:T} \mathrm{typeOf}(t) =_U A\right) \simeq \left(\sum_{t:T} \mathrm{typeOf}(t) =_U B\right)

and the function idtofam(A,B)\mathrm{idtofam}(A, B) is defined as

idtofam(A,B)≔transport ∑ t:TtypeOf(t)= U(−)(A,B)\mathrm{idtofam}(A, B) \coloneqq \mathrm{transport}^{\sum_{t:T} \mathrm{typeOf}(t) =_U (-)}(A, B)

Now, let us assume an arbitrary notion of equivalence type ≃\simeq. A Russell or Tarski universe is univalent if it is univalent as a reflexive graph, or equivalently, if one of the following equivalent conditions by the fundamental theorem of identity types hold:

That for each x:Ax:A the type of elements y:Ay:A such that R(x,y)R(x, y) is a contractible type.

x:A⊢ua(x):isContr(∑ y:AR(x,y))x:A \vdash \mathrm{ua}(x):\mathrm{isContr}\left(\sum_{y:A} R(x, y)\right)
That there is a family of equivalences

x:A,y:A⊢ua(x,y):(x= Ay)≃R(x,y)x:A, y:A \vdash \mathrm{ua}(x, y):(x =_A y) \simeq R(x, y)
That R(x,y)R(x, y) is an identity system.
That for each x:Ax:A and y:Ay:A, the function idtofam(x,y)\mathrm{idtofam}(x, y) is an equivalence of types

x:A,y:A,⊢ua(x,y):isEquiv(idtofam(x,y))x:A, y:A, \vdash \mathrm{ua}(x, y):\mathrm{isEquiv}(\mathrm{idtofam}(x, y))
That idtofam(x,y)\mathrm{idtofam}(x, y) is a retraction (This is due to Daniel Licata in Licata 16)

x:A,y:A⊢ua(x,y):R(x,y)→(x= Ay)x:A, y:A \vdash \mathrm{ua}(x, y):R(x, y) \to (x =_A y)
x:A,y:A,r:R(x,y)⊢G(x,y):idtofam(x,y,ua(x,y,r))= R(x,y)rx:A, y:A, r:R(x, y) \vdash G(x, y):\mathrm{idtofam}(x, y, \mathrm{ua}(x, y, r)) =_{R(x, y)} r
That R(x,y)R(x, y) with the function idtofam(x,y)\mathrm{idtofam}(x, y) satisfies the universal property of the unary sum of x= Ayx =_A y.

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

Traditional homotopy type theory uses the type of functions with contractible fibers for both ≃\simeq and RR, while Mike Shulman’s model of higher observational type theory uses the type of UU-small one-to-one correspondences for RR and the type of definitional isomorphisms for ≃\simeq.

Stricter versions of univalence

There are stricter versions of univalence, where we replace the equivalence of types between the identity type A= UBA =_U B and the type of equivalences of the universe A≃BA \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 UU, 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:UA:U and B:UB:U, one could judge that (A= UB)≡(A≃B)type(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 UU, 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:UA:U and B:UB:U, (A= UB)≡(A≃B)true(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:𝒱U:\mathcal{V} with T:𝒯(U)→𝒱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:𝒯(U)A:\mathcal{T}(U) and B:𝒯(U)B:\mathcal{T}(U), there is an identification ua(A,B):(T(A)= UT(B))= 𝒱(T(A)≃ 𝒱T(B))\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.

Rules for judgmentally univalent universes

With judgmentally univalent Tarski universes (U,T)(U, T), identities p:A= UBp:A =_U B are equivalences of types AA and BB. Namely, given function types and the isEquiv type family, one could add rules to the type theory which says that A= UBA =_U B behaves as an equivalence type:

Introduction rules:

Γ⊢A:UΓ⊢B:UΓ,x:T[A/X]⊢f:T[B/X]Γ⊢y:isEquiv(f)Γ⊢equiv(f,y):A= UB\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:

Γ⊢A:UΓ⊢B:UΓ,x:T[A/X]⊢f:T[B/X]Γ,z:A= UB⊢CtypeΓ,x:T[A/X],f:T[B/X],y:isEquiv(f)⊢c:C[equiv(f,y)/z]Γ,z:A= UB⊢ind A= UB C(c):C\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:

Γ⊢A:UΓ⊢B:UΓ,x:T[A/X]⊢f:T[B/X]Γ,z:A= UB⊢CtypeΓ,x:T[A/X],f:T[B/X],y:isEquiv(f)⊢c:C[equiv(f,y)/z]Γ,x:T[A/X],f:T[B/X],y:isEquiv(f)⊢β A= UB C(c):ind A= UB C(c)[equiv(f,y)/z]= C[equiv(f,y)/z]c\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:

Γ⊢A:UΓ⊢B:UΓ,x:T[A/X]⊢f:T[B/X]Γ,z:A= UB⊢CtypeΓ,x:T[A/X],f:T[B/X],y:isEquiv(f)⊢c:C[equiv(f,y)/z]Γ,z:A= UB⊢u:CΓ,x:T[A/X],f:T[B/X],y:isEquiv(f)⊢i in(u):u[equiv(f,y)/z]= C[in(x,y)/z]cΓ,e:A= UB⊢η A= UB C(c):u[e/z]= C[e/z]ind A= UB C(c)[e/z]\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 versions of univalence

In the context of function extensionality, Ian Orton and Andrew Pitts showed here that the univalence axiom can be simplified to the following special cases:

unit:A=∑ a:A1unit : A = \sum_{a:A} 1
flip:(∑ a:A∑ b:BC(a,b))=(∑ b:B∑ a:AC(a,b))flip : (\sum_{a:A} \sum_{b:B} C(a,b)) = (\sum_{b:B} \sum_{a:A} C(a,b))
contract:IsContr(A)→(A=1)contract: IsContr(A) \to (A=1)
unit β:coe(unit(a))=(a,⋆)unit_\beta : coe(unit(a)) = (a,\star)
flip β:coe(flip(a,b,c))=(b,a,c)flip_\beta : coe(flip(a,b,c)) = (b,a,c).

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

A=unit∑ a:A1=contract∑ a:A∑ b:Bfa=b=flip∑ b:B∑ a:Afa=b=contract∑ b:B1=unitB 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 βunit_\beta and flip βflip_\beta to compute that coe(ua(f))(a)=f(a)coe(ua(f))(a) = f(a), hence by function extensionality coe(ua(f))=fcoe(ua(f)) = f.

This is weaker than univalence because in the absense of function extensionality, it is no longer possible to prove univalence from this set of axioms.

In addition, unlike the definitions above, this definition of univalence cannot be generalized to reflexive graphs.

Internal univalence

Suppose the Tarski universe UU has

internal identity types
Id U:∏ A:UT(A)×T(A)→U\mathrm{Id}^U:\prod_{A:U} T(A) \times T(A) \to U
internal dependent product types
Π U(x:(−)).(−)(x):(U×∏ A:UT(A)→U)→U\Pi_U (x:(-)).(-)(x):\left(U \times \prod_{A:U} T(A) \to U\right) \to U
internal dependent sum types
Σ U(x:(−)).(−)(x):(U×∏ A:UT(A)→U)→U\Sigma_U (x:(-)).(-)(x):\left(U \times \prod_{A:U} T(A) \to U\right) \to U

We assume the weakest notion of Tarski universe, where the type reflection T(A)T(A) of each A:UA: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≃ U inBA \simeq_U^\mathrm{in} B, internal to the universe UU, which comes with a canonical equivalence of types

canonical ≃(A,B):T(A≃ U inB)≃(T(A)≃T(B))\mathrm{canonical}_\simeq(A, B):T(A \simeq_U^\mathrm{in} B) \simeq (T(A) \simeq T(B))

This implies that the equivalence T(A)≃T(B)T(A) \simeq T(B) is UU-small, and transport being an equivalence then implies that in any universe UU which is closed under function types, dependent product types, and dependent sum types, for all A:UA:U and B:UB:U, the identity type A= UBA =_U B is UU-small.

The internal univalence axiom states that the canonical function

idtointernalequiv(A,B):(A= UB)→T(A≃ U inB)\mathrm{idtointernalequiv}(A, B):(A =_U B) \to T(A \simeq_U^\mathrm{in} B)

is an equivalence of types

idtoequiv(A,B):(A= UB)≃T(A≃ U inB)\mathrm{idtoequiv}(A, B):(A =_U B) \simeq T(A \simeq_U^\mathrm{in} B)

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

i(p):canonical ≃(A,B)(idtoequiv(A,B)(p))= T(A)≃T(B)trans T(A,B)(p)i(p):\mathrm{canonical}_\simeq(A, B)(\mathrm{idtoequiv}(A, B)(p)) =_{T(A) \simeq T(B)} \mathrm{trans}^{T}(A, B)(p)

for all identifications p:A= UBp:A =_U B. By the J rule it is enough to show that canonical ≃(A,A)\mathrm{canonical}_\simeq(A, A) maps the identity equivalence of T(A≃ U inA)T(A \simeq_U^\mathrm{in} A) to the identity equivalence in T(A)≃T(A)T(A) \simeq T(A). Since the identity equivalence in T(A≃ U inA)T(A \simeq_U^\mathrm{in} A) is just the identity function canonical ≃ −1(A,A)(λx.x)\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.

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

corresponds to a morphism E→BE \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×B→Bp_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:B→B×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×B→B×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 b∈B↪B 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 I→Eq(E). \hat q : B^I \to Eq(E) \,.

The fibration E→BE \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:B→Eq(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 E→BE \to B any fibration (Kan fibration) between fibrant objects (Kan complexes), consider first the simplicial set

[E×B,B×E] B×B∈sSet/ 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 1→E 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 1→E b 2E_{b_1} \to E_{b_2}.

Let then

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

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

The fibration E→BE \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).

Univalence and axiom K

In this section we assume that the universe is a Tarski universe. Axiom K states that for all A:UA:U the type T(A)T(A) is a set. This means the type reflection of the internal equivalences T(A≃ UB)T(A \simeq_U B) is an h-set, and the univalence axiom then implies that UU 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 UU has internal univalent Tarski universes V:UV:U where the type T(V)T(V) has terms A:T(V)A:T(V) such that T V(A)T_V(A) is an h-set which is not an h-proposition, such as the booleans type. As a result, T(V)T(V) can be proven to not be a set, causing axiom K for UU to be inconsistent with the existence of V:UV:U and univalence.

Univalence and excluded middle

The univalence axiom is consistent with excluded middle. This is because the principle of excluded middle as traditionally defined in mathematics is about propositions or (-1)-truncated types.

Γ⊢AtypeΓ⊢lem A:isProp(A)→(A∨(A→∅))\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{lem}_A:\mathrm{isProp}(A) \to (A \vee (A \to \emptyset))}

The semantics of dependent type theory with excluded middle and universes satisfying the univalence axiom are boolean $(\infty, 1)$-toposes.

However, there is a global choice axiom which is inconsistent with univalence:

Γ⊢AtypeΓ⊢gc A:A+(A→∅)\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 choice principle is a much stronger axiom than excluded middle, being of comparable strength to a choice operator and implying that every type is an h-set; hence inconsistent with the univalence axiom.

Canonicity and homotopy 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), 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.

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 𝒰 0→A×𝒰 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.

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

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

inductively defined by

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

is an equivalence of types for all types AA and BB,

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

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

ΓctxΓ,Atype,Btype⊢ua(A,B):isEquiv(λp:A=B.idtoequiv(A,B,p))\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:

ΓctxΓ⊢ua:ΠA.ΠB.isEquiv(λp:A=B.idtoequiv(A,B,p))\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.

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
contrary to univalence is the axiom UIP
directed univalence axiom
identity type between types

References

For more references see also at homotopy type theory.

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](https://global.oup.com/academic/product/twenty-five-years-of-constructive-type-theory-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](https://doi.org/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](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.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