UF IAS 2012 Archive Math in HoTT

Page for the working group on math in HoTT. Please add what you’re working on, or ideas, or descriptions of the ideas below.

Done

• See Formalized Homotopy Theory

What people are working on

• See Formalized Homotopy Theory
• Descent theorem and toposes: Egbert
• Sets and truncation: Bas and Egbert

Thorsten and students are working on -1-truncations and the connection to Hedberg’s theorem

• Univalent categories (doing category theory nicely in HoTT): Mike, Benedikt, and Chris
• Higher groupoids and quotient types: Steve/Guillaume/Thorsten at least

Idea for things to work on

• homology: see the answer to the following question http://mathoverflow.net/questions/78450/homology-theory-constructed-in-a-homotopy-invariant-way)
• stable homotopy theory
• Postnikov towers
• Covering spaces and actions of fundamental groups on covering spaces
• simple results in cohesive HoTT
• limit sketches
• start going through Lurie’s book and formalizing things
• formalizing higher category theory

See also the page on Open Problems and Formalized Homotopy Theory