ETCS with a choice operator $\epsilon$. 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).

ETCS

SEAR plus epsilon

Last revised on July 28, 2024 at 02:57:26. See the history of this page for a list of all contributions to it.