[004T] Structure

In [0000], we review the \(2\)-category of toposes. This section is not needed for the rest but gives some intuitions for the design of axioms for synthetic topos theory.

[001T] is the core of the document. We introduce the topical type theory within which topos theory will be developed synthetically.

In [0039], we develop basic topo theory in the topical type theory.

In [003V], [004M], and [0042], we study some concrete examples of toposes in the topical type theory.