# Available frameworks for homotopy type theory

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.

• UniMath is not for synthetic homotopy theory which the HoTT Blakers–Massey theorem is, as far as I know. Lean's mathlib is much much more developed that the HoTT side, I'm not really aware of how the latter is going. HoTT in Lean is a bit different to implement because Lean is more classical than Coq. Though you probably are aware of this. – David Roberts Jun 14 at 21:15
• Current version of Lean (Lean 3) does not have support for HoTT. Lean 2 does, but I haven't heard of anyone using it in a long time. There's a big community interested in doing synthetic things using Coq/HoTT, though, although I suppose some interesting things require cubical... – xuq01 Jun 14 at 22:59
• There is, it seems, a hack to try to get HoTT in Lean 3: github.com/gebner/hott3. I see in the Readme there this crucial comment: "the Lean 3 kernel is inconsistent with univalence" – David Roberts Jun 14 at 23:44
• The HoTT implementation in Lean 3 is not inconsistent (as far as we know). There are some features supported by the Lean kernel (i.e., large elimination) which are inconsistent with the axiom of univalence, but every declaration tagged with the @[hott] attribute is automatically checked so that it stays in the safe univalence-compatible fragment. However, as Floris has already said, nobody is working on this library anymore. – Gabriel Ebner Jun 15 at 11:56
• I know essentially nothing about formalization, but the recent paper of Sanath Devalpurkar and Peter Haine seems germane: arxiv.org/abs/1912.04130 – Clark Barwick Jun 17 at 9:51