Timeline for Available frameworks for homotopy type theory
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 17, 2021 at 9:51 | comment | added | Clark Barwick | I know essentially nothing about formalization, but the recent paper of Sanath Devalpurkar and Peter Haine seems germane: arxiv.org/abs/1912.04130 | |
| Jun 15, 2021 at 18:10 | vote | accept | Neil Strickland | ||
| Jun 15, 2021 at 13:02 | comment | added | Peter LeFanu Lumsdaine | @GabrielEbner: Just as a side note, large elimination isn’t generally inconsistent with univalence — it’s just Lean’s specific formulation of it that is. (Sorry to nitpick — just want to forestall misunderstandings, like the widespread-for-a-while belief that dependent pattern matching was inconsistent with univalence, largely because Agda’s scheme of dependent pattern-matching was a form that baked in K/UIP.) | |
| Jun 15, 2021 at 12:34 | history | edited | Neil Strickland |
edited tags
|
|
| Jun 15, 2021 at 11:56 | comment | added | Gabriel Ebner |
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.
|
|
| Jun 15, 2021 at 4:20 | history | became hot network question | |||
| Jun 15, 2021 at 1:23 | answer | added | Floris van Doorn | timeline score: 14 | |
| Jun 14, 2021 at 23:44 | comment | added | David Roberts♦ | 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" | |
| Jun 14, 2021 at 22:59 | comment | added | xuq01 | 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... | |
| Jun 14, 2021 at 21:15 | comment | added | David Roberts♦ | 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. | |
| Jun 14, 2021 at 20:16 | history | asked | Neil Strickland | CC BY-SA 4.0 |