David Jaz Myers: Homotopy type theory for doing category theory

MIT Category Theory Seminar
2020/03/26
©Spifong
Speaker: David Jaz Myers
Title: Homotopy type theory for doing category theory
Abstract:
Homotopy Type Theory is a new foundations of mathematics which starts by asking what what it means to identify two mathematical objects. It depends on what type of objects they are: to identify the tangent space of the sphere at (0,0,1) with R^2, we need to choose a basis; to identify H^n(S^n; Z) with Z, we need to choose an orientation of the n-sphere; and to identify the smallest perfect number n with 6, we must prove that n = 6. So, type theory concerns itself with what type of thing everything is. As a result, we can derive what it means to identify two objects just from knowing what type of things they are.
This later property is very useful in category theory, where one is often tempted to say "...and with the obvious morphisms". In this talk, we will see how the HoTT point of view influences categorical practice. We'll see that universal properties give a unique way to identify an object, and therefore there are no issues with choosing functorial representatives of limits, or constructing an inverse to an essentially surjective, fully faithful functor -- even if one does not assume any choice principles.

[@fbkintanar]

This is a great talk, but the audio is defective. I hope you can find a opportunity to give this talk again with better audio, and add the video to this channel or your home page.

[@jackozeehakkjuz]

I was able to show that the precategory whose set of objects is 2=1+1 and with hom(a,b)=1 for all a,b in 2 is not a category. This is because, e.g. denoting the elements of 2 as x=inl(*) and y=inr(*), the identity type in 2 is (x=y) = 0 but the isomorphisms are (x≈y)=1. Now, how to see that if G is a group, then BG is not a category? If I can't get an answer here, can I have the link to the Zulip chat? Thank you all. Great talk.

[@fbkintanar]

around 39:00, the lemma is labeled UFP. What does UFP stand for, and what does it say about the lemma? Uniqueness of of Functoriality Proofs? Univalent Foundations Program? Univalent Fiber Principle? Uniqueness of Fibred Propositions?

[@davidgolembiowski4275]

I was curious as well. After listening a second time, then doing some online searching, I think "UFP" is the "[universal] fiber product" or 'pullback' where "[t]he pullback of two morphisms f and g need not exist, but if it does, it is essentially uniquely defined by the two morphisms." Sources: en.wikipedia.org/wiki/Pullback_(category_theory)#Fiber_bundles and en.wikipedia.org/wiki/Pullback_bundle

[@davidgolembiowski4275]

granted the "[universal]" part might be "[unique]". it's hard to say.

[@hywelgriffiths5747]

There are a couple of theorems labeled 'UFP' and at least one labeled 'AKS'. They're references to the sources of the theorems given on the last slide