nLab equivalence of types

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

Contents

Idea

In (dependent) type theory and in particular in homotopy type theory, two types DD, CC are called (homotopy-)isomorphic

[Rittri (1989), Cosmo (1995, §1.8), Hofmann & Streicher (1998, §5.4), Kapulkin & Lumsdaine (2012, 2021, Def. 3.1.1), but see below]

or equivalent [UFP13, §4] (for fine-print see the definitions below) if there exists a transformation DCD \to C which may be inverted (up to the relevant re-indentifications), hence if any program operating on data of type AA may be transformed into a program operating on data of type BB, and vice versa (see practical examples referenced below).

Alternatively, a function DCD \to C may be called a bijection if all its pre-images are essentially unique, namely if all its fiber types are contractible types. In the categorical semantics this is called a weak homotopy equivalence, whence this term is also used for the type-theoretic notion [Voevodsky (2010), p. 8, 10].

These two notions are in fact equivalent [UFP13, around Thm. 4.4.5].

In the special case of 0-truncated types (h-sets), hence in dependent type theories with axiom K or the axiom imposing uniqueness of identity proofs, the notion of type equivalence corresponds essentially to the notion of bijection or one-to-one correspondence in set theory.

In the special case of 1-truncated types (h-groupoids), type equivalence corresponds essentially to the notion of equivalence of groupoids in category theory.

In full homotopy type theory the categorical semantics of type equivalence is homotopy equivalence and that of type bijection is weak homotopy equivalence. That these notions coincide corresponds to the categorical semantics of types being as co-/fibrant objects, on which weak homotopy equivalences coincide with homotopy equivalences (by the Whitehead theorem).

Finally, the notion of equivalence/bijection of types is a priori different from that of identification of types in the type universe. To assert that the two notions do agree after all is to impose the univalence axiom.

Definitions

In dependent type theory, a type AA is a contractible type if it comes with an element a:Aa:A and a family of identities x:Ac(x):a= Axx:A \vdash c(x):a =_A x indicating that aa is a center of contraction. A type family x:AB(x)x:A \vdash B(x) is uniquely quantified if the dependent sum type x:AB(x)\sum_{x:A} B(x) is a contractible type. In dependent type theory with identity types and dependent sum types, an equivalence between types AA and BB could be defined as

  • a function with contractible fibers, a family of elements x:Af(x):Bx:A \vdash f(x):B for which the type family x:Af(x)= Byx:A \vdash f(x) =_B y is uniquely quantified for all y:By:B
  • a span (C;z:Cg(z):A;z:Ch(z):B)(C; z:C \vdash g(z):A; z:C \vdash h(z):B) for which the type family z:Cg(z)= Axz:C \vdash g(z) =_A x is uniquely quantified for all x:Ax:A and the type family z:Ch(z)= Byz:C \vdash h(z) =_B y is uniquely quantified for all y:By:B
  • a multivalued partial function (x:AP(x);x:A,p:P(x)f(x,p):B)(x:A \vdash P(x); x:A, p:P(x) \vdash f(x, p):B) for which the dependent type P(x)P(x) is a contractible type for all x:Ax:A and the type family x:A p:P(x)f(x,p)= Byx:A \vdash \sum_{p:P(x)} f(x, p) =_B y is uniquely quantified for all y:By:B
  • a one-to-one correspondence, a correspondence x:A,y:BR(x,y)x:A, y:B \vdash R(x, y) for which the type family y:BR(x,y)y:B \vdash R(x, y) is uniquely quantified for all x:Ax:A and the type family x:AR(x,y)x:A \vdash R(x, y) is uniquely quantified for all y:By:B
  • an element of the equivalence type f:ABf:A \simeq B, in dependent type theories with equivalence types given directly by rules.
  • a bi-invertible function or homotopy isomorphism, a family of elements x:Af(x):Bx:A \vdash f(x):B with families of elements y:Bg(y):Ay:B \vdash g(y):A and y:Bh(y):Ay:B \vdash h(y):A and families of identities x:AG(x):g(f(x))= Axx:A \vdash G(x):g(f(x)) =_A x and y:BH(y):f(h(y))= Byy:B \vdash H(y):f(h(y)) =_B y.
  • a coherently invertible function or half adjoint equivalence, a family of elements x:Af(x):Bx:A \vdash f(x):B with a family of elements y:Bg(y):Ay:B \vdash g(y):A and families of identities x:AG(x):g(f(x))= Axx:A \vdash G(x):g(f(x)) =_A x; y:BH(y):f(g(y))= Byy:B \vdash H(y):f(g(y)) =_B y; and x:AK(x):ap f(H(x))= g(f(x))= AxG(f(x))x:A \vdash K(x):\mathrm{ap}_f(H(x)) =_{g(f(x)) =_A x} G(f(x)).
  • a quasi-invertible function or homotopy equivalence, a family of elements x:Af(x):Bx:A \vdash f(x):B with a family of elements y:Bg(y):Ay:B \vdash g(y):A and families of identities x:AG(x):g(f(x))= Axx:A \vdash G(x):g(f(x)) =_A x and y:BH(y):f(g(y))= Byy:B \vdash H(y):f(g(y)) =_B y.
  • A function f:ABf:A \to B which satisfies copy induction, which makes the type BB satisfy the universal property of a copy of AA.

The isEquiv type family and equivalence types

As (eventually to be) discussed in the Properties-section below, the evident types formed by these definitions are co-inhabited: we have a function from any one of them to any of the others. Moreover, at least if we assume function extensionality, the evident types of “homotopy isomorphisms” and of functions with contractible fibers are equivalent and are h-propositions. This is only true for the evident type of homotopy equivalences if we assume axiom K or uniqueness of identity proofs (as discussed below); in dependent type theories without either axiom, the isEquiv type family is not in general a mere proposition for homotopy equivalences. However, often the most convenient way to show that ff is an equivalence is by exhibiting it as a term of the type of homotopy equivalences.

Rules for isEquiv

Given types AA and BB and function f:ABf:A \to B, ff is an equivalence of types if ff has a quasi-inverse function and BB satisfies the universal property of a copy type of AA with copy function f:ABf:A \to B. This means that one could define the family of h-propositions f:ABisEquiv(f)f:A \to B \vdash \mathrm{isEquiv}(f) using very similar natural deduction rules to the rules for copy types, but where the introduction rule states that given a function f:ABf:A \to B and evidence that ff has a quasi-inverse function, one could form a witness of isEquiv(f)\mathrm{isEquiv}(f):

Defining

f:ABqInv(f) g:BA( y:BId B(f(g(y)),y))×( x:AId A(g(f(x)),x))f:A \to B \vdash \mathrm{qInv}(f) \equiv \sum_{g:B \to A} \left(\prod_{y:B} \mathrm{Id}_B(f(g(y)), y)\right) \times \left(\prod_{x:A} \mathrm{Id}_A(g(f(x)), x)\right)

and

isProp(A) x:A y:Ax= Ay\mathrm{isProp}(A) \equiv \prod_{x:A} \prod_{y:A} x =_A y

the formation and introduction rules for isEquiv state that that the type family f:ABisEquiv(f)f:A \to B \vdash \mathrm{isEquiv}(f) comes with

  • a family of functions

    f:ABqinvtoisEquiv(f):qInv(f)isEquiv(f)f:A \to B \vdash \mathrm{qinvtoisEquiv}(f):\mathrm{qInv}(f) \to \mathrm{isEquiv}(f)
  • a family of identifications

    f:ABproptruncisEquiv(f):isProp(isEquiv(f))f:A \to B \vdash \mathrm{proptruncisEquiv}(f):\mathrm{isProp}(\mathrm{isEquiv}(f))

Formation rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓisEquiv(f)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B}{\Gamma \vdash \mathrm{isEquiv}(f) \; \mathrm{type}}

Introduction rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓqInvToIsEquiv(f):qInv(f)isEquiv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B}{\Gamma \vdash \mathrm{qInvToIsEquiv}(f):\mathrm{qInv}(f) \to \mathrm{isEquiv}(f)}
ΓAtypeΓBtypeΓf:ABΓproptruncisEquiv(f):isProp(isEquiv(f))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash \mathrm{proptruncisEquiv}(f):\mathrm{isProp}(\mathrm{isEquiv}(f))}

The elimination, computation, and uniqueness rules depend upon whether BB behaves like a positive copy type or a negative copy type:

As a negative type

Elimination rules for isEquiv:

ΓAtypeΓBtypeΓf:ABΓf 1:BA\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash f^{-1}:B \to A}

Computation rules for isEquiv:

ΓAtypeΓBtypeΓf:ABΓ,y:Bβ isEquiv(f)(y):f(f 1(y))= By\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma, y:B \vdash \beta_{\mathrm{isEquiv}(f)}(y):f(f^{-1}(y)) =_B y}

Uniqueness rules for isEquiv:

ΓAtypeΓBtypeΓf:ABΓ,x:Aη isEquiv(f)(x):f 1(f(x))= Ax\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma, x:A \vdash \eta_{\mathrm{isEquiv}(f)}(x):f^{-1}(f(x)) =_A x}

Using dependent sum types and product types, this could be reduced to the following inference rule

ΓAtypeΓBtypeΓ,f:ABisEquivtoqinv(f):isEquiv(f)qInv(f)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \mathrm{isEquivtoqinv}(f):\mathrm{isEquiv}(f) \to \mathrm{qInv}(f)}
As a positive type

Elimination rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γb:BΓind isEquiv(f) C(f,p,c f,b):C(b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, b):C(b)}

Computation rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc f: x:AC(f(x))Γa:AΓβ isEquiv(f)(f,p,c f,a):ind isEquiv(f) C(f,p,c f,f(a))= C(f(a))c f(a)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c_f:\prod_{x:A} C(f(x)) \quad \Gamma \vdash a:A \end{array} }{\Gamma \vdash \beta_{\mathrm{isEquiv}(f)}(f, p, c_f, a):\mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c_f, f(a)) =_{C(f(a))} c_f(a)}

Uniqueness rules for isEquiv:

ΓAtypeΓBtypeΓ,f:ABΓp:isEquiv(f) Γ,y:BC(y)typeΓc: y:BC(y)Γb:BΓη isEquiv(f)(f,p,c,b):c(b)= C(b)ind isEquiv(f) C(f,p,c,b)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, f:A \to B \quad \Gamma \vdash p:\mathrm{isEquiv}(f) \\ \Gamma, y:B \vdash C(y) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{y:B} C(y) \quad \Gamma \vdash b:B \end{array} }{\Gamma \vdash \eta_{\mathrm{isEquiv}(f)}(f, p, c, b):c(b) =_{C(b)} \mathrm{ind}_{\mathrm{isEquiv}(f)}^C(f, p, c, b)}

Defining isEquiv from other type formers

In dependent type theories with dependent product types, the isContr modality is defined as

isContr(A) x:A y:Ax= Ay\mathrm{isContr}(A) \coloneqq \sum_{x:A} \prod_{y:A} x =_A y

and the uniqueness quantifier on a type family x:AB(x)x:A \vdash B(x), is defined as

!x:A.B(x)isContr( x:AB(x))\exists!x:A.B(x) \coloneqq \mathrm{isContr}\left(\sum_{x:A} B(x)\right)

Assuming function extensionality, one could define isEquiv\mathrm{isEquiv} type family and the equivalence type for the first and fifth definition:

  • We define the property that a function f:ABf:A \to B is an equivalence as the property that the function has contractible fibers:

    f:ABisEquiv(f) y:B!x:A.f(x)= Byf:A \to B \vdash \mathrm{isEquiv}(f) \coloneqq \prod_{y:B} \exists!x:A.f(x) =_B y

    and the equivalence type for the first definition:

    AB f:ABisEquiv(f)A \simeq B \coloneqq \sum_{f:A \to B} \mathrm{isEquiv}(f)
  • We define the property that an equivalence f:ABf:A \simeq B is an equivalence as true, represented in dependent type theory by the unit type, because f:ABf:A \simeq B is always an equivalence:

    f:ABisEquiv(f)𝟙f:A \simeq B \vdash \mathrm{isEquiv}(f) \coloneqq \mathbb{1}

    and there is no need to define ABA \simeq B because the type is already defined. However, there is an equivalence between the types

    δ:(AB) f:ABisEquiv(f)\delta:(A \simeq B) \simeq \sum_{f:A \simeq B} \mathrm{isEquiv}(f)

If the dependent type theory came with a Tarski universe (U,El)(U, \mathrm{El}), one could additionally define the isEquiv U\mathrm{isEquiv}_U type family and the locally UU-small equivalence type for the second, third, and fourth definitions above, but only for UU-small structures:

  • The type of UU-small spans between AA and BB is the type

    Span U(A,B) C:U(El(C)A)×(El(C)B)\mathrm{Span}_U(A, B) \coloneqq \sum_{C:U} (\mathrm{El}(C) \to A) \times (\mathrm{El}(C) \to B)

    We define the property that a UU-small span f:Span U(A,B)f:\mathrm{Span}_U(A, B) is an equivalence as the property that both functions π 1(π 2(f)):El(C)A\pi_1(\pi_2(f)):\mathrm{El}(C) \to A and π 2(π 2(f)):El(C)B\pi_2(\pi_2(f)):\mathrm{El}(C) \to B have contractible fibers:

    f:Span U(A,B)isEquiv U(f)( x:A!z:El(C).π 1(π 2(f))(z)= Ax)×( y:B!z:El(C).π 2(π 2(f))(z)= By)f:\mathrm{Span}_U(A, B) \vdash \mathrm{isEquiv}_U(f) \coloneqq \left(\prod_{x:A} \exists!z:\mathrm{El}(C).\pi_1(\pi_2(f))(z) =_A x\right) \times \left(\prod_{y:B} \exists!z:\mathrm{El}(C).\pi_2(\pi_2(f))(z) =_B y\right)

    The locally UU-small equivalence type is defined as

    A UB f:Span U(A,B)isEquiv(f)A \simeq_U B \coloneqq \sum_{f:\mathrm{Span}_U(A, B)} \mathrm{isEquiv}(f)
  • The type of UU-small multivalued partial functions between AA and BB is the type

    MultiPartFunc U(A,B) P:AU( x:AEl(P(x)))B\mathrm{MultiPartFunc}_U(A, B) \coloneqq \sum_{P:A \to U} \left(\sum_{x:A} \mathrm{El}(P(x))\right) \to B

    We define the property that a UU-small multivalued partial function f:MultiPartFunc U(A,B)f:\mathrm{MultiPartFunc}_U(A, B) is an equivalence as the property that the dependent type El(π 1(f)(x))\mathrm{El}(\pi_1(f)(x)) is a contractible type for all x:Ax:A and the function π 2(f)\pi_2(f) has contractible fibers for all y:By:B:

    f:MultiPartFunc U(A,B)isEquiv U(f)( x:AisContr(El(π 1(f)(x))))×( y:B!x:A. p:El(π 1(f)(x))π 2(f)(x,p)= By)f:\mathrm{MultiPartFunc}_U(A, B) \vdash \mathrm{isEquiv}_U(f) \coloneqq \left(\prod_{x:A} \mathrm{isContr}\left(\mathrm{El}(\pi_1(f)(x))\right)\right) \times \left(\prod_{y:B} \exists!x:A.\sum_{p:\mathrm{El}(\pi_1(f)(x))} \pi_2(f)(x, p) =_B y\right)

    The locally UU-small equivalence type is defined as

    A UB f:MultiPartFunc U(A,B)isEquiv(f)A \simeq_U B \coloneqq \sum_{f:\mathrm{MultiPartFunc}_U(A, B)} \mathrm{isEquiv}(f)
  • The type of UU-small correspondences between AA and BB is the type

    Corr U(A,B)A×BU\mathrm{Corr}_U(A, B) \coloneqq A \times B \to U

    We define the property that a UU-small correspondence R:Corr U(A,B)R:\mathrm{Corr}_U(A, B) is an equivalence as being a one-to-one correspondence:

    R:Corr U(A,B)isEquiv U(R)( x:A!y:B.El(R(x,y)))×( y:B!x:A.El(R(x,y)))R:\mathrm{Corr}_U(A, B) \vdash \mathrm{isEquiv}_U(R) \coloneqq \left(\prod_{x:A} \exists!y:B.\mathrm{El}(R(x,y))\right) \times \left(\prod_{y:B} \exists!x:A.\mathrm{El}(R(x,y))\right)

    The locally UU-small equivalence type is defined as

    A UB f:Corr U(A,B)isEquiv(f)A \simeq_U B \coloneqq \sum_{f:\mathrm{Corr}_U(A, B)} \mathrm{isEquiv}(f)

If the dependent type theory also has function extensionality, then one could define the isEquiv\mathrm{isEquiv} type family and the equivalence type for the sixth and seventh definitions above:

  • For homotopy isomorphisms, given a function f:ABf:A \to B, we define the isEquiv(f)\mathrm{isEquiv}(f) type family as the product type of the type of sections of ff and the type of retractions of ff.
    f:ABisEquiv(f)( g:BA x:Ag(f(x))= Ax)×( h:BA y:Bf(h(y))= By)f:A \to B \vdash \mathrm{isEquiv}(f) \coloneqq \left(\sum_{g:B \to A} \prod_{x:A} g(f(x)) =_A x\right) \times \left(\sum_{h:B \to A} \prod_{y:B} f(h(y)) =_B y\right)
  • For half adjoint equivalences, given a function f:ABf:A \to B, we define the isEquiv(f)\mathrm{isEquiv}(f) type family as the type of quasi-inverse functions with a coherence condition.
    f:ABisEquiv(f) g:BA( x:Ag(f(x))= Ax)×( y:Bf(g(y))= By)×( x:Aap f(H(x))= g(f(x))= AxG(f(x)))f:A \to B \vdash \mathrm{isEquiv}(f) \coloneqq \sum_{g:B \to A} \left(\prod_{x:A} g(f(x)) =_A x\right) \times \left(\prod_{y:B} f(g(y)) =_B y\right) \times \left(\prod_{x:A} \mathrm{ap}_f(H(x)) =_{g(f(x)) =_A x} G(f(x))\right)
  • For invertible functions, given a function f:ABf:A \to B, we define the isEquiv(f)\mathrm{isEquiv}(f) type family as the proposition that the function merely has a quasi-inverse function:
    f:ABisEquiv(f)g:BA.(Πx:A.g(f(x))= Ax)×(Πy:B.f(g(y))= By)f:A \to B \vdash \mathrm{isEquiv}(f) \coloneqq \exists g:B \to A.(\Pi x:A.g(f(x)) =_A x) \times (\Pi y:B.f(g(y)) =_B y)

    and the equivalence type for the first definition:

    AB f:ABisEquiv(f)A \simeq B \coloneqq \sum_{f:A \to B} \mathrm{isEquiv}(f)

Finally, if the dependent type theory has axiom K or uniqueness of identity proofs, then one could define the isEquiv\mathrm{isEquiv} type family and the equivalence type directly for homotopy equivalences above; the coherence condition follows from the fact that the type g(f(x))= Axg(f(x)) =_A x is always a mere proposition in the presence of axiom K or UIP:

f:ABisEquiv(f) g:BA( x:Ag(f(x))= Ax)×( y:Bf(g(y))= By)f:A \to B \vdash \mathrm{isEquiv}(f) \coloneqq \sum_{g:B \to A} \left(\prod_{x:A} g(f(x)) =_A x\right) \times \left(\prod_{y:B} f(g(y)) =_B y\right)

In all three cases, by function extensionality for the first two and additionally by axiom K or UIP for the third case, the isEquiv(f)\mathrm{isEquiv}(f) type family is a mere proposition for all f:ABf:A \to B. Thus, we can define the equivalence type as

AB f:ABisEquiv(f)A \simeq B \coloneqq \sum_{f:A \to B} \mathrm{isEquiv}(f)

Historical note

The first attempt at a definition of an equivalence of type was the definition of a quasi-invertible function by Hofmann & Streicher (1998), §5.4. In the absence of axiom K or uniqueness of identity proofs, this definition suffers from a subltety in the construction of equivalence types, see below.

Later on, the following definitions of equivalences were constructed:

However, these definitions are only equivalent to one another in the presence of function extensionality.

Properties


Most of the following claims may be found proven in UFP13, §2.4 & §4.

 Functions with contractible fibers and one-to-one correspondences

We define an anafunction to be a type family R:A×B𝒰R :A \times B \to \mathcal{U} with a witness

p: a:A!b:B.R(a,b)p:\prod_{a:A} \exists!b:B.R(a,b)

The principle of unique choice holds in dependent type theory. This means that given any anafunction R:A×B𝒰R :A \times B \to \mathcal{U}, there is function f:ABf:A \to B. Similarly, for any function f:ABf:A \to B, there is an anafunction R:A×B𝒰R :A \times B \to \mathcal{U} defined by R(a,b)f(a)= BbR(a,b) \coloneqq f(a) =_B b.

A function with contractible fibers comes with a witness

q: b:B!a:A.f(a)= Abq:\prod_{b:B} \exists!a:A.f(a) =_A b

while an one-to-one correspondence is an anafunction which comes with a witness

q: b:B!a:A.R(a,b)q:\prod_{b:B} \exists!a:A.R(a, b)

Since we established that the types f(a)= Abf(a) =_A b and R(a,b)R(a, b) are the same for function ff and anafunction RR, functions with contractible fibers are equivalent to one-to-one correspondences.

The issue with two-sided quasi-inverses

The definition of equivalences as two-sided quasi-inverse functions (Def. ) suffers from the drawback that the type

f:ABqinv(f)f¯:BAId (AA)(f¯f,(aa))×Id (BB)(ff¯,(bb)), f \colon A \to B \;\;\;\;\;\; \vdash \;\;\;\;\;\; qinv(f) \coloneqq \underset{ \overline{f} \colon B \to A }{\sum} \;\; Id_{(A \to A)} \big( \overline{f} \circ f ,\, (a \mapsto a) \big) \;\times\; Id_{(B \to B)} \big( f \circ \overline{f} ,\, (b \mapsto b) \big) \,,

which may naively look like it merely detects whether ff is an equivalence, is in fact not a mere proposition (UFP13, Thm. 4.1.3).

This means that the type

(1)f:ABf¯:BAId (AA)(f¯f,(aa))×Id (BB)(ff¯,(bb)) \underset{ f \colon A \to B }{\sum} \; \underset{ \overline{f} \colon B \to A }{\sum} \;\; Id_{(A \to A)} \big( \overline{f} \circ f ,\, (a \mapsto a) \big) \;\times\; Id_{(B \to B)} \big( f \circ \overline{f} ,\, (b \mapsto b) \big)

is — despite its possible superficial appearance (cf. [Hofmann & Streicher (1998), §5.4]) – not in fact equivalent to the correct type of equivalences Equiv(A,B)Equiv(A,B), which is instead obtained from this expression by including a 0-truncation [] 0[-]_{0}:

Equiv(A,B)f:AB[f¯:BAId (AA)(f¯f,(aa))×Id (BB)(ff¯,(bb))] 0. Equiv(A,B) \;\simeq\; \underset{ f \colon A \to B }{\sum} \Bigg[ \underset{ \overline{f} \colon B \to A }{\sum} \;\; Id_{(A \to A)} \big( \overline{f} \circ f ,\, (a \mapsto a) \big) \;\times\; Id_{(B \to B)} \big( f \circ \overline{f} ,\, (b \mapsto b) \big) \Bigg]_0 \,.


One could also use propositional truncations instead of 0-truncation; this turns the dependent sum type in the definition into an existential quantifier, and is the proper translation of one of the definitions of bijection in set theory into type theory in the propositions as some types: A function f:ABf:A \to B is an equivalence if there (merely) exists a function f¯:BA\overline{f}:B \to A such that f¯f\overline{f} \circ f is equal to (aa)(a \mapsto a) and ff¯f \circ \overline{f} is equal to (bb)(b \mapsto b):

Equiv(A,B)f:ABf¯:BA.Id (AA)(f¯f,(aa))×Id (BB)(ff¯,(bb)). Equiv(A,B) \;\simeq\; \underset{ f \colon A \to B }{\sum} \exists \overline{f} \colon B \to A. Id_{(A \to A)} \big( \overline{f} \circ f ,\, (a \mapsto a) \big) \;\times\; Id_{(B \to B)} \big( f \circ \overline{f} ,\, (b \mapsto b) \big) \,.

Constructing the inverse function

For every function f:ABf \colon A \to B with contractible fibers (Def. ), there exists a function g:BAg \colon B \to A which is an inverse function.

The principle of unique choice implies that given a function f:ABf:A \to B, if for all b:Bb:B the fiber of ff at bb is contractible, then for all b:Bb:B there is an element g(b):fiber(f,b)g(b):\mathrm{fiber}(f, b).

b:BisContr( a:Af(a)= Ab) b:B a:Af(a)= Ab\prod_{b:B} \mathrm{isContr}\left(\sum_{a:A} f(a) =_A b\right) \to \prod_{b:B} \sum_{a:A} f(a) =_A b

The type theoretic axiom of choice then states that for all elements b:Bb:B one has the structure of an element a:Aa:A such that f(a)= Abf(a) =_A b, then one has a function g:BAg:B \to A such that f(g(b))= Abf(g(b)) =_A b.

b:B a:Af(a)= Ab g:BA b:Bf(g(b))= Ab\prod_{b:B} \sum_{a:A} f(a) =_A b \to \sum_{g:B \to A} \prod_{b:B} f(g(b)) =_A b

There is also another definition of contractible type, which uses the notion of center of contraction; namely, that a type AA is a contractible type if it comes with a element a:Aa:A and a witness that for all elements b:Ab:A, a= Aba =_A b

b:Aa= Ab\prod_{b:A} a =_A b

Since the fiber of ff at bb is contractible, g(b)g(b) is the center of contraction for the fiber of ff at bb.

Thus, for all elements a:Aa:A and b:Bb:B and a witness q(a,b):f(a)= Bbq(a, b):f(a) =_B b, there is a witness r(a,b,q(a,b)):a= Ag(b)r(a, b, q(a, b)):a =_A g(b). Since the type a= Ag(b)a =_A g(b) doesn’t depend on q(a,b)q(a, b), by the rules of function types, the latter condition is the same as for all elements a:Aa:A and b:Bb:B, a function r(a,b):f(a)= Bba= Ag(b)r(a, b):f(a) =_B b \to a =_A g(b).

still to prove: that the function above is an equivalence of types for all a:Aa:A and b:Bb:B.

Semantics

We discuss the categorical semantics of equivalences in homotopy type theory.

Let 𝒞\mathcal{C} be a locally cartesian closed category which is a model category, in which the (acyclic cofibration, fibration) weak factorization system has stable path objects, and acyclic cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.) For instance 𝒞\mathcal{C} could be a type-theoretic model category.

Of isEquiv()isEquiv(-)

Proposition

For A,BA, B two cofibrant-fibrant objects in 𝒞\mathcal{C}, a morphism f:ABf\colon A\to B is a weak equivalence or equivalently a homotopy equivalence in 𝒞\mathcal{C} precisely when the interpretation of isEquiv(f)isEquiv(f) has a global point *hasContrFibers(f)* \to hasContrFibers(f).

Proof

For f:ABf\colon A\to B, the categorical semantics of the dependent type

b:Bhfiber(f,b):Type b\colon B \;\vdash\; hfiber(f,b)\colon Type

is by the rules for the interpretation of identity types and substitution the mapping path space construction PfP f, given by the pullback

[b:Bhfiber(f,b)] Pf A f B I B B \array{ [b : B \vdash hfiber(f,b)] &\coloneqq & P f &\to& A \\ && \downarrow && \downarrow^{\mathrlap{f}} \\ && B^I &\to& B \\ && \downarrow \\ && B }

which, by the factorization lemma, is one way to factor ff as an acyclic cofibration followed by a fibration

f:APfB. f : A \stackrel{\simeq}{\to} P f \to B \,.

By definition and the semantics of contractible types, therefore, if AA and BB are cofibrant, then isEquiv(f)isEquiv(f) has a global element

* bisContr(hfiber(f,b)) * \to \prod_{b} isContr(hfiber(f,b))

precisely when in this factorization, the fibration PfBP f \to B is an acyclic fibration. (See for instance (Shulman, page 49) for more details.)

But by the 2-out-of-3 property, this is equivalent to ff being a weak equivalence — and hence a homotopy equivalence, since it is a map between fibrant-cofibrant objects.

Remark

In the above we fixed one function f:AXf : A \to X. But the type isEquivisEquiv is actually a dependent type

f:ABisEquiv(f) f : A \to B \vdash isEquiv(f)

on the type of all functions. To obtain the categorical semantics of this general dependent hasContrFibershasContrFibers-construction, first notice that the interpretation of

f:AB,a:A,b:B(f(a)=b):Typef : A \to B,\; a : A,\; b : B \;\vdash\; (f(a) = b) \colon Type

is by the rules for interpretation of identity types, evaluation and substitution the left vertical morphism in the pullback diagram

Q B I [A,B]×A×B (eval,id B) B×B, \array{ Q &\to& B^I \\ \downarrow && \downarrow \\ [A,B] \times A \times B &\stackrel{(eval, id_B)}{\to}& B \times B } \,,

where eval:[A,B]×ABeval : [A, B] \times A \to B is the evaluation map for the internal hom. This means that the interpretation of further dependent sum yielding hfibhfib

f:AB,b:B( a:A(f(a)=b)):Type f : A \to B,\; b : B \; \vdash \; \left( \sum_{a : A } (f(a) = b) \right) \colon Type

is the composite left vertical morphism in

Q B I [A,B]×A×B (eval,id B) B×B p 1,3 [A,B]×B \array{ Q &\to& B^I \\ \downarrow && \downarrow \\ [A,B] \times A \times B &\stackrel{(eval, id_B)}{\to}& B \times B \\ \downarrow^{\mathrlap{p_{1,3}}} \\ [A,B] \times B }

Of Equiv()Equiv(-)

(…)

References

General

The notion of two-sided homotopy equivalence of types in homotopy type theory appears (together with the formulation of the univalence axiom) already in

except that these authors refer to the subtly incorrect type (1) of all such equivalences.

The notion of equivalences as functions with contractible homotopy fibers (and thereby the fix of the univalence axiom of Hofmann & Streicher (1998), §5.4) is due to:

The notion of “homotopy isomorphisms” (functions with left- and right-quasi inverses) was proposed by André Joyal in a 2011 Oberwolfach meeting, recorded in:

The notion of equivalences as one-to-one correspondences is due to:

Introduction and exposition:

Textbook account:

Implementation of equivalences in proof assistants:

in Coq:

in Agda:

On equivalences as one-to-one correspondences in homotopy type theory:

  • Mike Shulman, Towards a Third-Generation HOTT Part 1 [slides, video]

Applications

Origin of the notion of type isomorphy in and application to programming language-theory and -practice:

Last revised on May 17, 2024 at 12:54:55. See the history of this page for a list of all contributions to it.