2026-09-22 21:28 UTC
@zwarich@hachyderm.io I dutifully defined collection[1] because I was supposed to, but nine years in we have only used it to prove replacement [2], so I guess this matters but not for anything we have done yet in the Intuitionistic Logic Explorer.
[1] https://us.metamath.org/ileuni/ax-coll.html
[2] https://us.metamath.org/ileuni/repizf.html
Replies (1)
-
@soaproot@sfba.social 2026-09-22 21:58
@zwarich@hachyderm.io As for separation and power sets, some of the other contributors are interested in CZF and we even have proved some results using it, but I have not dug into those proofs too much.