ETCS with a choice operator . The categorical analogue of (bounded) SEAR plus epsilon (although that article seems to be about SEAR with the non-extensional version of the choice operator).
Last revised on July 28, 2024 at 02:57:26. See the history of this page for a list of all contributions to it.