Talk: Bas Spitters - Formalizing mathematics in the univalent foundations
We have been formalizing mathematics in type theory for many years. Although great progress has been made, there were still a number of issues that are hard to tackle, especially when leaving the realm of
Info about event
Time
Location
Nygaard-295, Aabogade 34, 8200 Aarhus N
Organizer
Abstract:
We have been formalizing mathematics in type theory for many years. Although great progress has been made, there were still a number of issues that are hard to tackle, especially when leaving the realm of discrete mathematics. We mention a lack of quotient types and the absence of a clear mathematical semantics for the Coq type theory.
Homotopy type theory promises a solution to these challenges. I will discuss how to develop some mathematics in the univalent foundations and report on the design of our Coq library.
Basic familiarity with type theory and some categorical semantics will be assumed. For more information see:
http://homotopytypetheory.org/
https://github.com/HoTT/HoTT/
and our book:
http://homotopytypetheory.org/book/