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


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

See also the page on Open Problems and Formalized Homotopy Theory