HoTT Equivalences
- 07 December 2011
- Talks
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.
Video recording: HoTT Equivalences
How to comment on this blog:
At present comments are disabled because the relevant script died.
If you comment on this post on Mastodon and
mention
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
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.
Nice! I think your Wacom tablet works well... I found the writing very legible.
Thanks. The question is, should I bother uploading the HD versions of videos? Vimeo will take them.
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.
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 :-)