18
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$
    – David Roberts ♦
    Commented Jun 14, 2021 at 21:15
  • 3
    $\begingroup$ 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... $\endgroup$
    – xuq01
    Commented Jun 14, 2021 at 22:59
  • 1
    $\begingroup$ 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" $\endgroup$
    – David Roberts ♦
    Commented Jun 14, 2021 at 23:44
  • 2
    $\begingroup$ 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. $\endgroup$
    – Gabriel Ebner
    Commented Jun 15, 2021 at 11:56
  • 2
    $\begingroup$ I know essentially nothing about formalization, but the recent paper of Sanath Devalpurkar and Peter Haine seems germane: arxiv.org/abs/1912.04130 $\endgroup$
    – Clark Barwick
    Commented Jun 17, 2021 at 9:51

1 Answer 1

Reset to default
14
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .