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.