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 (dependent) type theory and in particular in homotopy type theory, two types $D$, $C$ 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 $D \to C$ which may be inverted (up to the relevant re-indentifications), hence if any program operating on data of type $A$ may be transformed into a program operating on data of type $B$, and vice versa (see practical examples referenced below).
Alternatively, a function $D \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.
In dependent type theory, a type $A$ is a contractible type if it comes with an element $a:A$ and a family of identities $x:A \vdash c(x):a =_A x$ indicating that $a$ is a center of contraction. A type family $x:A \vdash B(x)$ is uniquely quantified if the dependent sum type $\sum_{x:A} B(x)$ is a contractible type. In dependent type theory with identity types and dependent sum types, an equivalence between types $A$ and $B$ could be defined as
There is also a notion of strict equivalence between two types $A$ and $B$, where given families of elements $x:A \vdash f(x)B$ and $y:B \vdash g(y):A$, instead of having families of identities $G(x):g(f(x)) =_A x$ and $H(y):f(g(y)) =_B y$, one has judgmental equalities $g(f(a)) \equiv a:A$ and $b \equiv f(g(b)):B$ or propositional equalities $g(f(a)) \equiv_A a \; \mathrm{true}$ and $b \equiv_B f(g(b)) \; \mathrm{true}$, making the families of elements into judgmentally strict equivalences and propositionally strict equivalences respectively.
Judgmentally strict equivalences are used in defining judgmentally strict equivalence types, which in turn are used to define univalent universes in Mike Shulman‘s model of higher observational type theory.
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 $f$ is an equivalence is by exhibiting it as a term of the type of homotopy equivalences.
Given types $A$ and $B$ and function $f:A \to B$, $f$ is an equivalence of types if $f$ has a quasi-inverse function and $B$ satisfies the universal property of a copy type of $A$ with copy function $f:A \to B$. This means that one could define the family of h-propositions $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:A \to B$ and evidence that $f$ has a quasi-inverse function, one could form a witness of $\mathrm{isEquiv}(f)$:
Defining
and
the formation and introduction rules for isEquiv state that that the type family $f:A \to B \vdash \mathrm{isEquiv}(f)$ comes with
a family of functions
a family of identifications
Formation rules for isEquiv:
Introduction rules for isEquiv:
The elimination, computation, and uniqueness rules depend upon whether $B$ behaves like a positive copy type or a negative copy type:
Elimination rules for isEquiv:
Computation rules for isEquiv:
Uniqueness rules for isEquiv:
Using dependent sum types and product types, this could be reduced to the following inference rule
Elimination rules for isEquiv:
Computation rules for isEquiv:
Uniqueness rules for isEquiv:
In dependent type theories with dependent product types, the isContr modality is defined as
and the uniqueness quantifier on a type family $x:A \vdash B(x)$, is defined as
Assuming function extensionality, one could define $\mathrm{isEquiv}$ type family and the equivalence type for the first and fifth definition:
We define the property that a function $f:A \to B$ is an equivalence as the property that the function has contractible fibers:
and the equivalence type for the first definition:
We define the property that an equivalence $f:A \simeq B$ is an equivalence as true, represented in dependent type theory by the unit type, because $f:A \simeq B$ is always an equivalence:
and there is no need to define $A \simeq B$ because the type is already defined. However, there is an equivalence between the types
If the dependent type theory came with a Tarski universe $(U, \mathrm{El})$, one could additionally define the $\mathrm{isEquiv}_U$ type family and the locally $U$-small equivalence type for the second, third, and fourth definitions above, but only for $U$-small structures:
The type of $U$-small spans between $A$ and $B$ is the type
We define the property that a $U$-small span $f:\mathrm{Span}_U(A, B)$ is an equivalence as the property that both functions $\pi_1(\pi_2(f)):\mathrm{El}(C) \to A$ and $\pi_2(\pi_2(f)):\mathrm{El}(C) \to B$ have contractible fibers:
The locally $U$-small equivalence type is defined as
The type of $U$-small multivalued partial functions between $A$ and $B$ is the type
We define the property that a $U$-small multivalued partial function $f:\mathrm{MultiPartFunc}_U(A, B)$ is an equivalence as the property that the dependent type $\mathrm{El}(\pi_1(f)(x))$ is a contractible type for all $x:A$ and the function $\pi_2(f)$ has contractible fibers for all $y:B$:
The locally $U$-small equivalence type is defined as
The type of $U$-small correspondences between $A$ and $B$ is the type
We define the property that a $U$-small correspondence $R:\mathrm{Corr}_U(A, B)$ is an equivalence as being a one-to-one correspondence:
The locally $U$-small equivalence type is defined as
If the dependent type theory also has function extensionality, then one could define the $\mathrm{isEquiv}$ type family and the equivalence type for the sixth and seventh definitions above:
and the equivalence type for the first definition:
Finally, if the dependent type theory has axiom K or uniqueness of identity proofs, then one could define the $\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)) =_A x$ is always a mere proposition in the presence of axiom K or UIP:
In all three cases, by function extensionality for the first two and additionally by axiom K or UIP for the third case, the $\mathrm{isEquiv}(f)$ type family is a mere proposition for all $f:A \to B$. Thus, we can define the equivalence type as
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. In the absence of function extensionality, the definition of an equivalence as a homotopy isomorphism, first proposed by André Joyal in a 2011 Oberwolfach meeting, recorded in Kapulkin & Lumsdaine (2012, 2021), Def. 3.1.1, similarly suffers from a subltety in the construction of equivalence types.
It wasn’t until Voevodsky (2010), p. 8, 10 that the correct definition of an equivalence as a function with contractible fibers was formulated, where the definition of equivalence types works even without function extensionality. The definition of an equivalence as a one-to-one correspondence was proposed in Shulman 2022, which is equivalent to Voevodsky’s definition by the principle of unique choice.
Most of the following claims may be found proven in UFP13, §2.4 & §4.
We define an anafunction to be a type family $R :A \times B \to \mathcal{U}$ with a witness
The principle of unique choice holds in dependent type theory. This means that given any anafunction $R :A \times B \to \mathcal{U}$, there is function $f:A \to B$. Similarly, for any function $f:A \to B$, there is an anafunction $R :A \times B \to \mathcal{U}$ defined by $R(a,b) \coloneqq f(a) =_B b$.
A function with contractible fibers comes with a witness
while an one-to-one correspondence is an anafunction which comes with a witness
Since we established that the types $f(a) =_A b$ and $R(a, b)$ are the same for function $f$ and anafunction $R$, functions with contractible fibers are equivalent to one-to-one correspondences.
The definition of equivalences as two-sided quasi-inverse functions (Def. ) suffers from the drawback that the type
which may naively look like it merely detects whether $f$ is an equivalence, is in fact not a mere proposition (UFP13, Thm. 4.1.3).
This means that the type
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)$, which is instead obtained from this expression by including a 0-truncation $[-]_{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:A \to B$ is an equivalence if there (merely) exists a function $\overline{f}:B \to A$ such that $\overline{f} \circ f$ is equal to $(a \mapsto a)$ and $f \circ \overline{f}$ is equal to $(b \mapsto b)$:
For every function $f \colon A \to B$ with contractible fibers (Def. ), there exists a function $g \colon B \to A$ which is an inverse function.
The principle of unique choice implies that given a function $f:A \to B$, if for all $b:B$ the fiber of $f$ at $b$ is contractible, then for all $b:B$ there is an element $g(b):\mathrm{fiber}(f, b)$.
The type theoretic axiom of choice then states that for all elements $b:B$ one has the structure of an element $a:A$ such that $f(a) =_A b$, then one has a function $g:B \to A$ such that $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 $A$ is a contractible type if it comes with a element $a:A$ and a witness that for all elements $b:A$, $a =_A b$
Since the fiber of $f$ at $b$ is contractible, $g(b)$ is the center of contraction for the fiber of $f$ at $b$.
Thus, for all elements $a:A$ and $b:B$ and a witness $q(a, b):f(a) =_B b$, there is a witness $r(a, b, q(a, b)):a =_A g(b)$. Since the type $a =_A g(b)$ doesn’t depend on $q(a, b)$, by the rules of function types, the latter condition is the same as for all elements $a:A$ and $b:B$, a function $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:A$ and $b:B$.
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.
For $A, B$ two cofibrant-fibrant objects in $\mathcal{C}$, a morphism $f\colon A\to B$ is a weak equivalence or equivalently a homotopy equivalence in $\mathcal{C}$ precisely when the interpretation of $isEquiv(f)$ has a global point $* \to hasContrFibers(f)$.
For $f\colon A\to B$, the categorical semantics of the dependent type
is by the rules for the interpretation of identity types and substitution the mapping path space construction $P f$, given by the pullback
which, by the factorization lemma, is one way to factor $f$ as an acyclic cofibration followed by a fibration
By definition and the semantics of contractible types, therefore, if $A$ and $B$ are cofibrant, then $isEquiv(f)$ has a global element
precisely when in this factorization, the fibration $P 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 $f$ being a weak equivalence — and hence a homotopy equivalence, since it is a map between fibrant-cofibrant objects.
In the above we fixed one function $f : A \to X$. But the type $isEquiv$ is actually a dependent type
on the type of all functions. To obtain the categorical semantics of this general dependent $hasContrFibers$-construction, first notice that the interpretation of
$f : 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
where $eval : [A, B] \times A \to B$ is the evaluation map for the internal hom. This means that the interpretation of further dependent sum yielding $hfib$
is the composite left vertical morphism in
(…)
isEquiv
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:
Andrej Bauer, HoTT equivalences, talk (2011) [webpage, video]
Mike Shulman, from slide 60 of part 2, slide 49 of part 3 in: Minicourse in homotopy type theory (2012) [web]
Andrej Bauer, Equivalences [video], Part 4 of: Introduction to homotopy type theory, lecture series (2019)
Textbook account:
Implementation of equivalences in proof assistants:
in Coq:
in Agda:
On equivalences as one-to-one correspondences in homotopy type theory:
Origin of the notion of type isomorphy in and application to programming language-theory and -practice:
Mikael Rittri, Using types as search keys in function libraries, in: FPCA ‘89: Proceedings of the fourth international conference on Functional programming languages and computer architecture (1989) 174–183 [doi:10.1145/99370.99384, pdf]
Roberto Di Cosmo, Isomorphisms of Types – from $\lambda$-calculus to information retrieval and language design, Progress in Theoretical Computer Science, Birkhäuser (1995) [doi:10.1007/978-1-4612-2572-0]
Gilles Barthe, Olivier Pons, Type Isomorphisms and Proof Reuse in Dependent Type Theory, in Foundations of Software Science and Computation Structures. FoSSaCS 2001, Lecture Notes in Computer Science 2030, Springer (2001) [doi:10.1007/3-540-45315-6_4]
Roberto Di Cosmo, A short survey of isomorphisms of types, Mathematical Structures in Computer Science 15 5 (2005) 825-838 [doi:10.1017/S0960129505004871, pdf]
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman, Proof Repair across Type Equivalences [arXiv:2010.00774]
Talia Ringer, Proof repair along type equivalences, §4 in: Proof Repair, Univ. Washington (2021) [proquest:2568297410, video]
Last revised on November 24, 2023 at 17:35:23. See the history of this page for a list of all contributions to it.