Formalized Spectral Sequences in Homotopy Type Theory I September 14, 2017 - 12:00pm Algebra, Combinatorics, and Geometry

Speaker Information

Floris van Doorn

Carnegie Mellon University

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