I would like to get an overview over what different first-order systems suitable for the formalization of "classical" mathematics are currently known.
So far I only know the variants of ZFC, building on sets and membership as its primitives, and the variants of ETCS, building on sets and morphisms as its primitives.
What are other first-order systems that have been proposed as foundational?
I'd be happy not only to see the definitions of other systems but also to get a feeling of how they form a home for everyday-use mathematics concretely:
E.g.: How is set theory developed in the system, i.e. how are sets, elements, maps, relations, quotients by relations, families of sets and their products, disjoint union, ..., modelled in the system? How to construct the natural numbers, the rational numbers, the real numbers?
For any proposed system I am also interested in understanding the relation to the "classical" foundation by ZFC.