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.