Homotopy Type Theory Seminar

John Dykes, Department of Pure Mathematics, University of Waterloo

"Propositional Logic"

In this week's meeting of the homotopy type theory seminar, we begin by discussing how homotopy equivalence behaves with certain common types. We talk about the difference between classical and intuitionistic logic and introduce propositional truncation. We then prove that univalence implies function extensionality.

MC 5413