Title: Homotopy Type Theory and Univalence
Speaker: Jim Fowler
Abstract: Homotopy Type Theory (HoTT), as the name suggests, blends type theory with homotopy theory. In HoTT, the notion of "equality" is interpreted as the existence of a path. Transitivity of equality, that a=b and b=c implies a=c, then can be seen as concatenation of paths. The "types" in HoTT can be viewed as spaces. As a topologist, finding out that the foundations of mathematics are a sort of geometry is extremely satisfying, and I'm excited about the implications for computer-assisted proofs, and for using HoTT as a place to do "synthetic homotopy theory." This Invitations talk will assume no background in either type theory or homotopy theory and will introduce some of the basic ideas of both.
