An elementary topos is a category $\ECat$ satisfying the following conditions:
- $\ECat$ inductive and finite projective limits;
- $\ECat$ admits exponentials: for each $A\in \Ob{\ECat}$, the functor $(-)\times A : \ECat\to\ECat$ admits a right adjoint, written $\prn{-}\Sup{A}$;
- $\ECat$ has an arrow $v : \ObjTerm{\ECat}\to \Omega$ that for each $X\in \Ob{\ECat}$ the arrows from $X$ to $\Omega$ give by fibered product with $v$ exactly the subobjects of $X$.
We can reduce these axiomatics, as recent work by A. Kock and Ch. Mikkelson (Hurd & Loeb, 1974) has shown, and describe for example in the manner of F.W. Lawvere (Lawvere, 1972) an elementary topos as a cartesian closed category in which the notion of a subobject is representable.
Bibliography
-
Kock, A., & Mikkelsen, C. J. (1974). Topos-theoretic factorization of non-standard extensions. In A. Hurd & P. Loeb (Eds.), Victoria Symposium on Nonstandard Analysis (pp. 122–143). Springer Berlin Heidelberg.Details
-
Lawvere, F. W. (1972). Introduction. In F. W. Lawvere (Ed.), Toposes, Algebraic Geometry and Logic (pp. 1–12). Springer Berlin Heidelberg.Details