renaming this page to equivalence of types in parallel to equivalence of categories, embedding of topological spaces, embedding of smooth manifolds, and embedding of types

Anonymouse

]]>I have re-worked the Idea section here, trying to make it convey more of the actual broad ideas at play.

In the course I have:

added more original references on the notion of type isomorphy, even if invertibility was originally formulated with respect to definitional equality.

As far as I can tell, the notion goes back to Rittri (1989) and appears in full beauty in a textbook account in Di Cosmo (1995), just around the time when Hofmann & Streicher consider the homotopy-theoretic version.

generally I have compiled references (here) where people use type isomorphy/equivalence in actual programming practice

added a graphics showing type equivalence/bijection with their categorical semantics

and this one:

- Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman,
*Proof Repair across Type Equivalences*[arXiv:2010.00774]

and this one:

- Talia Ringer,
*Proof repair along type equivalences*, §4 in:*Proof Repair*, Univ. Washington (2021) [proquest:2568297410, video]

added pointer to:

- 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]

moving the section on equivalence types over to the new article equivalence type

Anonymous

]]>changed

as a relation which is both a total and functional relation and an onto and entire relation.

to

as a relation which is an injective and surjective anafunction.

Anonymous

]]>Added

as a relation which is both a total functional relation and an onto entire relation. –

in homotopy type theory this leads to the definition of equivalence as a one-to-one correspondence

(Def. \ref{OneToOneCorrespondence} below).

to definitions list

Anonymous

]]>added reference to

- Chris Kapulkin, Peter LeFanu Lumsdaine, Def. 3.1.1 in:
*The Simplicial Model of Univalent Foundations (after Voevodsky)*, Journal of the European Mathematical Society**23**(2021) 2071–2126 [arXiv:1211.2851, doi:10.4171/jems/1050]

for the notion of “homotopy isomorphism”

]]>I have removed the subsection “Definition – Other variations”:

(Because, as a definition this was now redundant, and as a discussion of properties it was in the wrong spot.)

I have moved the key paragraph that used to be in this subsection to after the first announcement of the list of definitions (here) where it now serves as an announcement of the discussion (that should eventually be had) in the Properties-section.

]]>Thanks, but this discussion ought to come before the definitions, not inside a Properties-subsection.

I have moved it to there and expanded somewhat.

(There is still plenty of room left to structure this entry better. The main thing missing currently is a clear statement of that/how the notions are (in)equivalent.)

]]>Replaced

The possibly most evident definition of equivalences as quasi-inverse functions

with

There are two ways to define a bijection in set theory: As a function which is both an injection (whose fibers are h-propositions) and a surjection (whose fibers are inhabited), and as an isomorphism of sets. The former definition in homotopy type theory leads to the definition of equivalence as a function with contractible fibers, while the latter definition leads to the definition of equivalence as a quasi-inverse function. However, the definition of equivalences as quasi-inverse functions

Anonymous

]]>added this reference:

The notion of equivalences as functions with contractible homotopy fibers (and thereby the fix of the univalence axiom) is due to:

- Vladimir Voevodsky, p. 10 of:
*Univalent Foundations Project*(2010) [pdf]

]]>

I have added a sub-section *Properties – The issue with quasi-inverses* (here) trying to highlight what is maybe the single most important subtlety in the business that this entry should discuss.

(Possibly this subsection eventually ought to be placed elsewhere in the section hierarchy; but for the moment there is not enough logical coherence in the entry to decide this either way.)

In the course of this I also added pointer to

- Martin Hofmann, Thomas Streicher, §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, pdf]

where the notion of type equivalence together with the univalence axiom is all preconceived – all except for falling victim to this subtlety.

]]>oh, I found the 2011 video by AB, have now added it back, in this form:

- Andrej Bauer,
*HoTT equivalences*, talk (2011) [webpage, video]

(somebody may want to fix this accordingly on the HoTT blog here)

]]>but I added this pointer:

- Andrej Bauer,
*Equivalences*[video], Part 4 of:*Introduction to homotopy type theory*, lecture series (2019)

I am removing the following bibitem for the moment, since the video that it points to is gone:

- Andrej Bauer,
*A seminar on HoTT equivalences*(blog post)

I have tried to recover the video via the WaybackMachine, but with inconclusive results: While the WaybackMachine claims to have records, the video it eventually serves doesn’t play (on my device, anyways).

If a working link still exists and anyone can get hold of it, let’s add it back into the entry.

]]>In the section “As functions with contractible fibers” (here) I have adjusted wording and typesetting.

In particular, I have given the actual definition a numbered Definition-environment (now here)

Then I used this to fix the first sentence further below in *Properties – Constructing the inverse function* (here), which used to start out with

For every equivalence, …

by changing it to:

For every function $f \colon A \to B$ with contractible fibers (Def. 2.1), …

(Because, at this point in the entry, half a dozen definitions of “equivalence” have been mentioned, so we need to be specific if we now turn to discussing how they relate.)

]]>Spottet this sentence at the end of the Idea-section:

These are sometimes called weak equivalences, but there is nothing weak about them (in particular, they always have homotopy inverses).

One might debate whether here is the right place to discuss the issue of weak equivalences, but if we do then the above sentence is unsatisfactory – so I have replaced it by the following:

]]>In point-set topology and generally in the context of homotopical 1-category-theory, these are called

weak equivalences, since without suitable resolution they may not be homotopy equivalences. However, via the categorical semantics of homotopy type theory in type-theoretic model categories, the required resolutions are all implicit (essentially since all objects are assumed to be cofibrant and identity types are interpreted as fibrant resolution of diagonal maps) so that all equivalences are actually homotopy equivalences.

This entry gives little justification for its many claims.

I have now at least added pointer to:

- Univalent Foundations Project, §2.4 and §4 in:
*Homotopy Type Theory – Univalent Foundations of Mathematics*(2013) [web, pdf]

and added the following line at the beginning of the Definition-section:

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

renaming the page because the definition is valid also in non-homotopy type theories like in dependent type theories with axiom K.

Anonymous

]]>also added redirects for equivalence of types and equivalences of types

Anonymous

]]>added useful redirects for type of equivalences and types of equivalences

Anonymous

]]>added alternate definition of equivalence as one-to-one correspondence and a reference for the definition

Anonymous

]]>