3 ms·

Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

• b9r5 2y ago
  In a practical sense, hasn't type theory already replaced ZFC in the foundations of math? Lean is what working mathematicians currently use to formally prove theorems, and Lean is based on type theory rather than ZFC.
  • westurner 2y ago
    But HoTT is removed from lean core? From https://news.ycombinator.com/item?id=42440016#42444882 https://news.ycombinator.com/item?id=42440016#42444882 : > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4 https://www.google.com/search?q=hott+in+lean4 https://github.com/forked-from-1kasper/ground_zero https://github.com/forked-from-1kasper/ground_zero : > Lean 4 HoTT Library
• deleted 2y ago
  [deleted]
• fithisux 2y ago
  Still, both should be taught.
• westurner 2y ago
  "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0 https://link.springer.com/article/10.1007/s10516-023-09676-0