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)
identity type, equivalence of types, definitional isomorphism
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 , 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 which may be inverted (up to the relevant re-indentifications), hence if any program operating on data of type may be transformed into a program operating on data of type , and vice versa (see practical examples referenced below).
Alternatively, a function 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 is a contractible type if it comes with an element and a family of identities indicating that is a center of contraction. A type family is uniquely quantified if the dependent sum type is a contractible type. In dependent type theory with identity types and dependent sum types, an equivalence between types and could be defined as
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 is an equivalence is by exhibiting it as a term of the type of homotopy equivalences.
Given types and and function , is an equivalence of types if has a quasi-inverse function and satisfies the universal property of a copy type of with copy function . This means that one could define the family of h-propositions using very similar natural deduction rules to the rules for copy types, but where the introduction rule states that given a function and evidence that has a quasi-inverse function, one could form a witness of :
Defining
and
the formation and introduction rules for isEquiv state that that the type family 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 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 , is defined as
Assuming function extensionality, one could define type family and the equivalence type for the first and fifth definition:
We define the property that a function 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 is an equivalence as true, represented in dependent type theory by the unit type, because is always an equivalence:
and there is no need to define because the type is already defined. However, there is an equivalence between the types
If the dependent type theory came with a Tarski universe , one could additionally define the type family and the locally -small equivalence type for the second, third, and fourth definitions above, but only for -small structures:
The type of -small spans between and is the type
We define the property that a -small span is an equivalence as the property that both functions and have contractible fibers:
The locally -small equivalence type is defined as
The type of -small multivalued partial functions between and is the type
We define the property that a -small multivalued partial function is an equivalence as the property that the dependent type is a contractible type for all and the function has contractible fibers for all :
The locally -small equivalence type is defined as
The type of -small correspondences between and is the type
We define the property that a -small correspondence is an equivalence as being a one-to-one correspondence:
The locally -small equivalence type is defined as
If the dependent type theory also has function extensionality, then one could define the 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 type family and the equivalence type directly for homotopy equivalences above; the coherence condition follows from the fact that the type 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 type family is a mere proposition for all . 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.
Later on, the following definitions of equivalences were constructed:
as a function with contractible fibers, first proposed by Voevodsky (2010), p. 8, 10
as a homotopy isomorphism, first proposed by André Joyal in a 2011 Oberwolfach meeting, recorded in Kapulkin & Lumsdaine (2012, 2021), Def. 3.1.1,
as a one-to-one correspondence, first proposed in Shulman 2022
However, these definitions are only equivalent to one another in the presence of function extensionality.
Most of the following claims may be found proven in UFP13, §2.4 & §4.
We define an anafunction to be a type family with a witness
The principle of unique choice holds in dependent type theory. This means that given any anafunction , there is function . Similarly, for any function , there is an anafunction defined by .
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 and are the same for function and anafunction , 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 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 , which is instead obtained from this expression by including a 0-truncation :
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 is an equivalence if there (merely) exists a function such that is equal to and is equal to :
For every function with contractible fibers (Def. ), there exists a function which is an inverse function.
The principle of unique choice implies that given a function , if for all the fiber of at is contractible, then for all there is an element .
The type theoretic axiom of choice then states that for all elements one has the structure of an element such that , then one has a function such that .
There is also another definition of contractible type, which uses the notion of center of contraction; namely, that a type is a contractible type if it comes with a element and a witness that for all elements ,
Since the fiber of at is contractible, is the center of contraction for the fiber of at .
Thus, for all elements and and a witness , there is a witness . Since the type doesn’t depend on , by the rules of function types, the latter condition is the same as for all elements and , a function .
…
still to prove: that the function above is an equivalence of types for all and .
We discuss the categorical semantics of equivalences in homotopy type theory.
Let 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 could be a type-theoretic model category.
For two cofibrant-fibrant objects in , a morphism is a weak equivalence or equivalently a homotopy equivalence in precisely when the interpretation of has a global point .
For , the categorical semantics of the dependent type
is by the rules for the interpretation of identity types and substitution the mapping path space construction , given by the pullback
which, by the factorization lemma, is one way to factor as an acyclic cofibration followed by a fibration
By definition and the semantics of contractible types, therefore, if and are cofibrant, then has a global element
precisely when in this factorization, the fibration 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 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 . But the type is actually a dependent type
on the type of all functions. To obtain the categorical semantics of this general dependent -construction, first notice that the interpretation of
is by the rules for interpretation of identity types, evaluation and substitution the left vertical morphism in the pullback diagram
where is the evaluation map for the internal hom. This means that the interpretation of further dependent sum yielding
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 -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 May 17, 2024 at 12:54:55. See the history of this page for a list of all contributions to it.