Formalized Spectral Sequences in Homotopy Type Theory I

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