Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I had set out to add to the entry equivalence in homotopy type theory a detailed derivation of the categorical semantics of $Equiv(X,Y)$. But then I ended up getting distracted by various editorial work in other entries and for the moment I only have this puny remark added, expanding on the previous discussion there.
Maybe more later…
added useful redirects for type of equivalences and types of equivalences
Anonymous
also added redirects for equivalence of types and equivalences of types
Anonymous
This entry gives little justification for its many claims.
I have now at least added pointer to:
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.
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.
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.)
I am removing the following bibitem for the moment, since the video that it points to is gone:
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.
but I added this pointer:
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
where the notion of type equivalence together with the univalence axiom is all preconceived – all except for falling victim to this subtlety.
added this reference:
The notion of equivalences as functions with contractible homotopy fibers (and thereby the fix of the univalence axiom) is due to:
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
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.)
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.
added reference to
for the notion of “homotopy isomorphism”
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
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
moving the section on equivalence types over to the new article equivalence type
Anonymous
added pointer to:
and this one:
and this one:
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
1 to 24 of 24