Comment Comment by jhanschoo HoTT is somewhat independent of the choice of proof assistant.Coq: https://github.com/HoTT/HoTTLean: https://github.com/gebner/hott3idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT. parent jhanschoo 5 years ago
Coq: https://github.com/HoTT/HoTT
Lean: https://github.com/gebner/hott3
idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.