HoTT Equivalences

On December 6th 2011 I gave a talk about homotopy equivalences in the context of homotopy type theory at our seminar for foundations of mathematics and theoretical computer science. I discuss the differences and relations between isomorphism (in the sense of type theory), an adjoint equivalence, and a homotopy equivalence. Even though the talk itself was not super-well prepared, I hope the recording will be interesting to some people. I was going fairly slowly, so it should be possible to follow the talk. I apologize for such a long video, but I really did not see how to chop it up into smaller pieces. Also, I need to figure out why I cannot fast forward the video beyond what has been downloaded.

5 thoughts on “HoTT Equivalences

  1. About fast-forwarding: vimeo.com supports it only in their HTML5 viewer. You can switch from the Flash viewer to HTML5 viewer by clicking on the button in the bottom-right corner.

  2. Having watched some of it, I find it wonderfully clear and quite illuminating. It is great to be able to jump around in the talk, eg to revisit things, or skip boring or laborious bits.

    I don’t think I yet understand the relation between adjoint equivalences (between categories I presume) and the property of a function that all its fibres are contractible. The latter property requires there to be not only at least one isomorphism, but also something-more. Are you saying that this something-more, up to bureaucratic shuffling around, amounts to a proof that certain triangles commute, in a certain sense?

    I have heard that it is a key property of the notion you call equivalence that to say that something
    is an equivalence is a proposition (ie. the space of paths between a pair of proofs of the proposition is contractible). This somehow truncates things beneficially, so the possibility of paths between paths doesn’t get too out of hand. Do you agree, or how would you put it?

    If I was offered three wishes, my first would be a remote control gizmo that would allow fast forward (or rewind) through life itself in some browsable fashion. The ability to repair or delete history would be great too.

  3. Clear sound, readable handwriting, great overall quality! As for understanding to the content I have yet to listen to it a couple of time more :-)

Leave a Reply

Your email address will not be published. Required fields are marked *

− 9 = 1

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>