5 ms·
Wait, what? Lean doesn't used any ideas from "topos theory, higher category theory, and homotopy theory." It uses pretty vanilla type theory. The HoTT people s
by spekcular 5y ago
Wait, what?
Lean doesn't used any ideas from "topos theory, higher category theory, and homotopy theory." It uses pretty vanilla type theory. The HoTT people sometimes express annoyance at the "impurity" of their approach, in fact.
Also, it's not so clear that Eilenberg is "most influential mathematician to pass through Columbia's math department doors" when people like Okounkov are there. I don't necessarily disagree, but it's a highly contestable claim.
- deleted 5y ago[deleted]
- bionhoward 5y agoIt’s a good claim. Topos theory is a statement about type systems, right?
- Syzygies 5y agoLean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread. I love how you allow that dependent types are now "vanilla"; perhaps more people will migrate from Haskell to Idris. The HoTT book is the trippiest read. I said "perhaps", and what's an opinion worth if it's not obviously an opinion? Eilenberg has category theory and homological algebra to his credit, those are entire subjects that have shaped the last seventy years of mathematics. I'm happy to throw him into the debate.
- zozbot234 5y agoAIUI, it is possible to do HoTT in Lean 3 with no modifications to Lean itself, albeit by "disabling" singleton elimination from Prop to Type. (An example library is at https://github.com/gebner/hott3 https://github.com/gebner/hott3 .) No idea about the newer Lean 4, but the documentation does not mention any changes to the underlying logic that would affect that.