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.

- 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

- 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

Created on April 19, 2018 at 17:16:58
by
Univalent foundations special year 2012