Proposing a community goal to formalize a synthetic rational homotopy theory

[djspacewhale]

A 1-connected space is rational when its homotopy groups are vector spaces over the rational numbers. I like the language of rational abelian groups, as the space of such ℚ‐vector space structures on any given abelian group is a proposition, but this is nonstandard. Classically, many dreams of the young algebraic topologist come true in the category of rational spaces - for example, the Hurewicz homomorphisms from homotopy groups to (ordinary) homology groups are always isomorphisms. The abstract nonsense of model categories gives several algebraic "presentations" of the ∞-category of rational spaces, including the model category of connective rational dg Lie algebras (wherein, for a dg Lie algebra X presenting a space X*, the graded Lie algebra of the homology of X is isomorphic to the graded Lie algebra of homotopy groups X* with the Whitehead bracket!).

Inspired by a talk by Reid Barton at this year's HoTT-UF proposing to formalize the theory of model categories and their localizations for, in his case, synthetic topological K-theory; reading Simon Henry's paper introducing a non-univalent constructive theory of model categories; and with Axel Ljungström's synthetic definition of the generalized Whitehead bracket; I propose an analogous project to Barton's synthetic topological K-theory for a synthetic rational homotopy theory.

The main conjecture of this project would be something of this form:

Conjecture. Assuming the Whitehead principle, the wild category of (UU l-small) rational types is the localization of the weak model category of (UU l-small) connective rational dg Lie algebras at the quasi-isomorphisms.

The Whitehead principle would likely be necessary as localizing at quasi-isomorphisms of chain complexes - chain maps inducing isomorphisms in homology for all n : ℤ- is morally just a homological version of Whitehead.

This project would motivate completing many outstanding goals in the library, (likely) introduce a new namespace for homological algebra, and pose an interesting research goal of formalizing model categories and their localizations for, to my knowledge, the first time in a univalent setting. Agda-UniMath seems a good home for this project as, as Barton notes in his talk, modal extensions to the base type theory (that may break compatibility with cubical Agda) have been the most valuable tools in the past for things like simplicial types, if the need for those arises.