I am thinking about trying to formalise some parts of classical unstable homotopy theory in homotopy type theory, especially the EHP and Toda fibrations, and some related work of Gray, Anick and Cohen-Moore-Neisendorfer. I am encouraged by the successful formalisation of the Blakers-Massey and Freudenthal theorems; I would expect to make extensive use of similar techniques. I would also expect to use the James construction, which I believe has also been formalised. Some version of localisation with respect to a prime will also be needed.


My question here is as follows: what is the current status of the various different libraries for working with HoTT? If possible, I would prefer Lean over Coq, and Coq over Agda. I am aware of <https://github.com/HoTT/HoTT>, which seems moderately active. I am not clear whether that should be regarded as superseding all other attempts to do HoTT in Coq such as <https://github.com/UniMath>. I am also unclear about how the state of the art in Lean or Agda compares with Coq.



Available frameworks for homotopy type theory
The HoTT libraries in Lean can be considered dead. Since Lean has moved away from HoTT, I don't think it's a more convenient system to do HoTT in than - for example - Coq.


There is still some formalization material in the Lean 2 library that hasn't been formalized in another proof assistant, but probably the best thing to do with that is to port it to other libraries instead of working on top of it.


About the Coq-HoTT vs Unimath libraries: I've used both a bit, and I found the Coq-HoTT library way more pleasant to work with. Also, it focuses more on synthetic homotopy theory than Unimath, which focuses more on doing "ordinary mathematics" in a univalent style.


I haven't used Agda much, but it has a good library for synthetic homotopy theory. Last time I checked it had quite a bit more in that direction that Coq-HoTT, but it has *way* less activity.


