Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: equivalence of types

Bottom of Page

1 to 25 of 25

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 25th 2012

    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)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…

  2. added alternate definition of equivalence as one-to-one correspondence and a reference for the definition

    Anonymous

    diff, v19, current

  3. added useful redirects for type of equivalences and types of equivalences

    Anonymous

    diff, v21, current

  4. also added redirects for equivalence of types and equivalences of types

    Anonymous

    diff, v21, current

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

    Anonymous

    diff, v24, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    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.

    diff, v36, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    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.

    diff, v36, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022
    • (edited Dec 27th 2022)

    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:A→Bf \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.)

    diff, v36, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    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.

    diff, v36, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    but I added this pointer:

    diff, v36, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

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

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

    diff, v36, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022
    • (edited Dec 27th 2022)

    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.

    diff, v37, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022
    • (edited Dec 27th 2022)

    added this reference:

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

    diff, v37, current

  14. 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

    diff, v38, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    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.)

    diff, v39, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    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.

    diff, v39, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 27th 2022

    added reference to

    for the notion of “homotopy isomorphism”

    diff, v39, current

  18. Added

    1. 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

    diff, v40, current

  19. 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

    diff, v40, current

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

    Anonymous

    diff, v40, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2023

    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]

    diff, v49, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2023

    and this one:

    diff, v50, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2023

    and this one:

    diff, v50, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJan 28th 2023
    • (edited Jan 28th 2023)

    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

    diff, v52, current

1 to 25 of 25

  1.