nlab and Lean 3

Stream: general

[Henrik Böving]

A friend that uses the nlab mentioned to me that they seem to be linking Lean 3 things still, for example groups: https://ncatlab.org/nlab/show/group at the bottom links to mathlib3. Their Lean explanation page itself is also not really correct: https://ncatlab.org/nlab/show/Lean they e.g. mention it is possible to do HoTT with it.

So I guess if we care about Lean visibility on the nlab someone :tm: should try to get this stuff right?

[Mac Malone]

Henrik Böving said:

Their Lean explanation page itself is also not really correct: https://ncatlab.org/nlab/show/Lean they e.g. mention it is possible to do HoTT with it.

Interestingly, that page does link to a WIP Lean 4 HoTT implementation -- forked-from-1kasper/ground_zero -- so perhaps it is just meant to say that downstream HoTT implementations are conceivably possible even if not necessarily fully realized.

[David Michael Roberts]

PSA anyone can edit the nLab, so go ahead and improve as needed!