Homotopy Type Theory Seminar

Andrej Vukovic, Department of Pure Mathematics, University of Waterloo

"Univalence"

In this week's meeting of the homotopy type theory seminar, we begin by reviewing homotopy equivalence and the transport map. We then discuss dependent pair and function types in the context of homotopy theory and introduce function extensionality. Finally, we formalize the univalence axiom with the type-theoretic notion of homotopy equivalence.

MC 5413