Quantum Topology / Hopf Algebra Seminar
Alexander Berenbeim
UIC
Motivations For Homotopy Type Theory - Part 2
Abstract: After last week's surfeit of abstract nonsense where we principally introduced Cartesian Closed Categories
(CCCs), briefly covered the \lambda-calculus, and made unfulfilling promises about (co)-monads,
comes a full reboot. We begin by emphasizing the main lesson which may have been obscured last week: models of the \lambda calculus are precisely CCCs and that the conversion rules correspond to introduction, elimination, and computation rules which are expressible as adjoints, which in turn give rise to (co)-monads. This lesson will be explicitly developed by closely working through the examples of the basic type formers found in ML Intuitionistic Type Theory and their interpretation in Homotopy Type Theory. We then will explicitly prove that $\pi_1(S^1) \cong Z$ by building
upon the machinery introduced in the first part of the talk. This talk should be interesting for those intrigued by univalent foundations, or who have an interest in learning more about formal proof verification. In particular, the second half of the talk will be an extended example in proving mathematical theorem in the Homotopy Type Theory fork of Coq. No background will be assumed.
Thursday March 30, 2017 at 2:00 PM in SEO 612