Homotopy Type Theory Seminar

Andrej Vukovic, Department of Pure Mathematics, University of Waterloo

"Fundamental Group of the Circle and Other Highlights"

Today we construct the circle type and show that its fundamental group is Z, using synthetic homotopy theory. As requested at the last meeting, we also show that function extensionality implies weak function extensionality.

MC 5413