4 ms·
There are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the
by mbid 9y ago
There are serious efforts to found maths on elementary toposes, which are categories with certain properties. Much the same way that the axioms of ZFC model the properties of sets in terms of the "is element" relation, you can give first order axioms for how the morphisms and objects of an elementary topos behave. Then you may add more axioms to assert that the elementary topos you're talking about is really a category of sets in the sense of ZFC.
If you want to research more about this, I can recommend sheaves in geometry and logic by Maclane and Moerdijk. You can also search for "algebraic set theory" and go from there.
And btw, type theory is essentially the same thing. The axioms are IMO uglier and more ad-hoc, but there are (some proven, some conjectured) equivalence results.