Elementary topoi generalize properties of the category of sets, requiring finite limits, colimits, and cartesian closure. They feature a subobject classifier Ω, which acts as a generalized truth values object, allowing for internal logic within the topos.

The axioms of elementary topoi provide a rich structure for studying categorical logic and set-like objects. The subobject classifier plays a crucial role, enabling the representation of membership, subobjects, and power objects, while supporting an intuitionistic internal logic.

Foundations of Elementary Topoi

Axioms of elementary topos

Elementary topos generalizes properties of category of sets as category with additional structure (Grothendieck topoi)
Axioms require all finite limits and colimits exist including products, equalizers, coproducts, coequalizers (pullbacks, pushouts)
Cartesian closure ensures internal hom objects and exponential objects exist for any pair of objects ( $B^A$ )
Subobject classifier Ω acts as generalized truth values object with universal mono true: 1 → Ω (classifying map)

Role of subobject classifier

Subobject classifier Ω generalizes set of truth values allowing for internal logic within topos (intuitionistic logic)
Characteristic functions uniquely map subobjects to Ω representing membership (indicator functions)
Classification establishes correspondence between subobjects of X and morphisms X → Ω (power set)
Power objects represent all subobjects of given object defined using subobject classifier (℘(X) ≅ Ω^X)
Elements of Ω correspond to truth values in internal logic (generalized Boolean algebra)

Axioms of elementary topos, How elements are defined in axiomatic set theory - Mathematics Stack Exchange

Structure and Logic of Elementary Topoi

Limits and colimits in topos

Finite limits include terminal object 1 binary products A×B equalizers and constructed pullbacks
Finite colimits include initial object 0 binary coproducts A+B coequalizers and constructed pushouts
Universality ensures limits and colimits satisfy universal properties (uniqueness up to isomorphism)
Preservation dictates limits preserved by right adjoints colimits by left adjoints (adjoint functor theorem)
Interaction with exponentials shows products distribute over colimits exponentials preserve limits in second argument ( $A × (B + C) ≅ (A × B) + (A × C)$ )

Internal logic vs categorical structure

Internal logic of topos corresponds to higher-order intuitionistic type theory (Curry-Howard correspondence)
Objects represent types morphisms represent functions between types in internal language (lambda calculus)
Subobject classifier Ω represents proposition type power objects $Ω^X$ represent predicate types on X
Exponentials $Y^X$ represent function types from X to Y (currying)
Natural number object provides internal arithmetic (Peano axioms)
Each topos models its internal logic (categorical semantics)
Mitchell-Bénabou language formally captures internal logic (typed lambda calculus)
Kripke-Joyal semantics interprets internal language in terms of topos structure (forcing)