Formalized Spectral Sequences in Homotopy Type Theory I

Thursday, September 14, 2017 - 12:00
427 Thackeray Hall
Speaker Information
Floris van Doorn
Carnegie Mellon University

Abstract or Additional Information

Homotopy type theory is a novel language based on a connection between type theory and algebraic topology. This allows you to define concepts in algebraic topology in a way which is very close to the logical foundations, making it convenient for formalized proofs in a computer proof assistant. Furthermore, everything you can define in homotopy type theory automatically respects homotopy equivalence. In the first out of two talks, I'll give a general introduction to homotopy type theory