2026-09-22 17:55 UTC
After playing around with various attempts to construct models of ZF (or IZF) in the Calculus of Inductive Constructions, I can say that CiC (even with LEM) is severely deficient compared to ZF/IZF in terms of what can be done without assuming some form of Choice. I think that Lean's banishment of these problems by just assuming Choice throughout the ecosystem might be no small part of its appeal to mathematicians.
Replies (1)
-
@soaproot@sfba.social 2026-09-22 20:18
@zwarich@hachyderm.io Wait, did I accidentally make myself cool by working in IZF? (It totally wasn't on purpose, I chose IZF because.... well historical accident sort of but basically IZF seemed like, uh, something I could get my head around I guess).