Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math? 1 year ago (link.springer.com) 5 comments westurner Reply Add to library b9r5 1 year 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 1 year ago But HoTT is removed from lean core?From > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4 westurner 1 year ago "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0 fithisux 1 year ago Still, both should be taught.
b9r5 1 year 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 1 year ago But HoTT is removed from lean core?From > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4 westurner 1 year ago "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0 fithisux 1 year ago Still, both should be taught.
westurner 1 year ago But HoTT is removed from lean core?From > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4 westurner 1 year ago "Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0 fithisux 1 year ago Still, both should be taught.
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.
But HoTT is removed from lean core?
From > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4westurner
1 year ago
fithisux
1 year ago
"Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0
Still, both should be taught.