ETCS
Overview
Elementary Theory of the Category of Sets. Lawvere (1964) axiomatized set theory in categorical language—objects are sets, morphisms are functions. Equiconsistent with bounded Zermelo set theory.
Era: 1964
Proposed at: New York, USA (Columbia)
Formal structure
Domain: Category C: objects Ob(C), morphisms Hom(A, B), composition ∘
id_B ∘ f = f = f ∘ id_A; (h ∘ g) ∘ f = h ∘ (g ∘ f)
Constraints: Finite axioms; terminal object 1; pullbacks; NNO (natural numbers)
Objective: ETCS + AC ≃ ZFC for most mathematics