gebner/hott3
View on GitHub ↗ ★ 83 Lean
HoTT in Lean 3
4 mentions on Hacker News by 4 people: 0 stories, 4 comments · first 2018-05-29 · latest 2021-12-12
20082026
-
…[0] that uses an attribute to restrict uses of that rule, but it isn't really ergonomic to use. [0] https://github.com/gebner/hott3
comment by scapp · 2021-12-12 · in The HoTT Game -
…itself, albeit by "disabling" singleton elimination from Prop to Type. (An example library is at https://github.com/gebner/hott3 .) No idea about the newer Lean 4, but the documentation does not mention any changes to the underlying logic…
comment by zozbot234 · 2021-12-01 · in An introduction to topos theory (2011) [pdf] -
…is somewhat independent of the choice of proof assistant. 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…
comment by jhanschoo · 2021-06-24 · in Homotopy Type Theory -
…There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3 Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think L
comment by im_down_w_otp · 2018-05-29 · in Theorem Proving in Lean