The Mathematics of Neo-Rationalism: Notes on Categorical Logic and Topos Theory

Dedicated to Dieter Roth, Gerhard Rühm, and Oswald Wiener.

This book provides the maths behind the program initiated by Peter Wolfendale and Reza Negarestani called “Neo-Rationalism.” My aim is to extend their program through these self-contained lecture-style notes in two parts. Part I develops categorical logic along the following arc: from Lawvere’s functorial semantics of algebraic theories, through the doctrinal hierarchy of logical fragments (cartesian, regular, coherent, Heyting), to theleft unifying frameworks of doctrines and generalized sketches. Part II develops topos theory: the elementary topos axioms, the standard examples (sets, $G$-sets, presheaves, graphs, sheaves), the internal higher-order logic via the Mitchell–Bénabou language and Kripke–Joyal semantics, the bi-Heyting structure of presheaf toposes, geometric morphisms, and the view of toposes as custom-tailored universes for mathematics.

How to Read These Notes

Part I assumes basic category theory (categories, functors, natural transformations, limits, adjunctions)—Appendix C is a one-page refresher, and Awodey & Bauer’s own appendices [4] a fuller one. Part II assumes Part I through Section 10. Readers who want the shortest path to toposes can read §2, §7, skim §8, and jump to Part II; readers headed for type theory should take §11 seriously and continue with Shulman [5].

Part I. Categorical Logic

1. Introduction: Logic through the Lens of Categories

1.1 What the Subject Is

Categorical logic is the study of logical systems using the tools of category theory. The subject originated in F. W. Lawvere’s 1963 PhD thesis on the functorial semantics of algebraic theories, and it has since expanded to encompass a vast range of logical systems drawn from both mathematics and computer science.¹ The basic point of view can be stated in two slogans.

The first slogan is Lawvere’s functorial semantics. Instead of treating a theory as a bundle of uninterpreted syntax and a model as a set-based structure satisfying axioms, one distills the theory into a category ${𝒞}_{𝕋}$ carrying exactly the categorical structure needed to interpret the theory’s logic (finite products for equational logic, finite limits for cartesian logic, and so on), and one recovers models as functors ${𝒞}_{𝕋}\to 𝒞$ preserving that structure. Syntax and semantics become objects of the same kind, related by functors, and the classical metatheorems—soundness, completeness, the existence of free models—become statements about universal properties.

The second slogan, also due to Lawvere, identifies the quantifiers and connectives as adjoint functors: existential and universal quantification are the left and right adjoints to substitution, conjunction and implication are related by the adjunction defining Heyting algebras, and comprehension, equality, and even the powerset arise from adjunctions.

1.2 Two Traditions: Model Theory and Proof Theory

Following de Paiva and Rodin, it is useful to distinguish two grand strands within categorical logic:²

• Categorical model theory. In the Lawvere tradition, one studies the correspondence between theories-as-categories and their categories of models. Provability is reflected in the ordering of subobjects; a formula is a subobject, and satisfaction is containment of subobjects. Part I of these notes lives mostly in this tradition.

• Categorical proof theory. In the Curry–Howard–Lambek tradition, one identifies propositions with types (objects) and proofs—not merely provability—with terms (morphisms). The paradigmatic result is Lambek’s theorem that the simply typed $\lambda$-calculus is the internal language of cartesian closed categories, so that $\beta \eta$-equivalence classes of terms correspond to morphisms. Shulman’s lecture notes [5] develop categorical logic thoroughly from this side, using multicategories as an intermediate structure between type theories and monoidal or cartesian categories.³

The two strands meet in the higher reaches of the subject: an elementary topos is simultaneously the model-theoretic environment for higher-order theories (Part II) and, via its internal type theory, a proof-theoretic object.

1.3 How the Subject Is Organized: Fragments and Structures

A recurring theme is a dictionary between fragments of first-order and higher-order logic and classes of structured categories. Each row of the following table is a “doctrine” in the informal sense of Section 12; the table is the roadmap for all of Part I and the bridge to Part II.⁴

Reading the table downward, each fragment adds connectives, and each class of categories adds the corresponding structure. Reading a single row, one has three interlocking activities: a proof theory (the deductive calculus of the fragment), a categorical semantics (interpretation in any category of the given class), and a completeness theorem mediated by a syntactic classifying category.

1.4 Plan of Part I

Section 2 collects the categorical preliminaries on subobjects that the semantics requires. Sections 3 and 4 develop algebraic theories, functorial semantics, and Lawvere’s syntax–semantics duality in detail, following Awodey & Bauer [4]. Sections 6–10 climb the first-order hierarchy: cartesian, regular, coherent, and Heyting logic. Section 12 steps back to the organizing frameworks: doctrines as 2-monads, Makkai’s generalized sketches, and Fujii’s unified framework for algebraic notions.

2. Preliminaries: Subobjects, Predicates, and Stability

Throughout Part I, the semantic home of a predicate on an object $A$ is the poset of subobjects of $A$. This section fixes the relevant machinery.⁵

2.1 Subobjects

Let $A$ be an object of a category $𝒞$. Given monomorphisms $i:I\rightarrowtail A$ and $j:J\rightarrowtail A$, say $i\le j$ when $i$ factors through $j$, i.e. when there is $k:I\to J$ with $j\circ k=i$. Such a $k$ is automatically monic and unique. This makes the class of monos into $A$ a preorder; its poset reflection is the poset $Sub\left(A\right)$ of subobjects of $A$: elements are equivalence classes of monos, where $i\sim j$ iff $i\le j\le i$ (in which case $I\cong J$ over $A$). One calls $𝒞$ well-powered when each $Sub\left(A\right)$ is (equivalent to) a small poset; all categories in these notes are well-powered.

When $𝒞$ has pullbacks, $Sub$ becomes a functor $$Sub:{𝒞}^{\mathrm{o}\mathrm{p}}\to 𝐏𝐨𝐬,$$ sending $f:A\to B$ to the monotone map $f^{*}:Sub\left(B\right)\to Sub\left(A\right)$ given by pullback of monos along $f$ (pullbacks of monos are monos, and the two-pullbacks lemma makes this functorial up to the identifications built into $Sub$).

2.2 Predicates, Meets, and the Top Element

If $𝒞$ has pullbacks, each $Sub\left(A\right)$ has finite meets: the top element is $\left[{\mathrm{i}\mathrm{d}}_A\right]$, and the meet of $[i:I\rightarrowtail A]$ and $[j:J\rightarrowtail A]$ is the diagonal of the pullback square $$\begin{array}{ccc}\hfill I\wedge J\hfill & \hfill \to \hfill & \hfill J\hfill \\ \hfill \downarrow \hfill & \hfill \hfill & \hfill \downarrow j\hfill \\ \hfill I\hfill & \hfill \stackrel{i}{\to }\hfill & \hfill A\hfill \end{array}$$ Moreover these meets are stable: for any $f:B\to A$, $$f^{*}\left({\top }_A\right)={\top }_B,f^{*}(U\wedge V)=f^{*}U\wedge f^{*}V.$$ Stability is the categorical shadow of the syntactic fact that substitution commutes with the connectives, $(\phi \wedge \psi )\left[t/x\right]=\phi \left[t/x\right]\wedge \psi \left[t/x\right]$: since substitution will be interpreted as pullback, every operation used to interpret a connective must be preserved by pullback for the semantics to be well-defined. “Stable under pullback” is a hypothesis that will recur in every definition of Part I.

2.3 Generalized Elements

A generalized element of $C$ is simply a morphism $x:X\to C$; one thinks of $X$ as a stage or domain of variation of the element. Given a subobject $S\rightarrowtail C$, write $x{\in }_{C}S$ when $x$ factors (necessarily uniquely) through $S$. The following rules let one reason about subobjects element-wise, and will reappear in Part II as the degenerate, “global” fragment of Kripke–Joyal semantics:

1. $x{\in }_C\top$ always;

2. $S\le T$ iff for every stage $X$ and every $x:X\to C$, $x{\in }_{C}S$ implies $x{\in }_{C}T$;

3. $x{\in }_{C}S\wedge T$ iff $x{\in }_{C}S$ and $x{\in }_{C}T$;

4. for the diagonal $\Delta =[⟨{\mathrm{i}\mathrm{d}}_C,{\mathrm{i}\mathrm{d}}_C⟩]\in Sub(C\times C)$: $⟨x,y⟩\in \Delta$ iff $x=y$;

5. for an equalizer $E(f,g)\rightarrowtail A$ of $f,g:A\rightrightarrows B$: $x{\in }_{A}E(f,g)$ iff $fx=gx$;

6. for a pullback: $x{\in }_A{f}^{*}S$ iff $fx{\in }_{B}S$.

2.4 Adjoints Between Subobject Posets

A monotone map between posets is a functor; adjoint functors between posets are Galois connections: $L⊣R$ means $L\left(x\right)\le y\iff x\le R\left(y\right)$. All logical structure in Part I lives in this poset-level world. For $f:A\to B$ in a category with pullbacks, one asks whether the pullback functor $f^{*}:Sub\left(B\right)\to Sub\left(A\right)$ has adjoints: $${\exists }_f⊣f^{*}⊣{\forall }_f.$$ When they exist, the left adjoint ${\exists }_f$ interprets existential quantification along $f$ and the right adjoint ${\forall }_f$ universal quantification. The adjunction laws $${\exists }_{f}U\le V\iff U\le f^{*}V,f^{*}V\le U\iff V\le {\forall }_{f}U$$ are precisely the two-way inference rules for the quantifiers, a point we take up in Section 7.

3. Algebraic Theories and Functorial Semantics

Algebraic theories describe structures determined by everywhere-defined operations and equational axioms: groups, rings, modules, lattices. The scope of the notion is wider than it first appears—many concepts without an obviously equational flavor admit algebraic formulations—while some familiar ones are genuinely excluded: fields (because $0^{-1}$ is undefined) and categories (because composition is only partially defined) are not algebraic.⁶

3.1 Signatures, Terms, and Theories

3.2 Models in Any Category with Finite Products

The set-based notion of a group—a set $G$ with functions $e:1\to G$, $m:G\times G\to G$, $i:G\to G$ satisfying equations between composites—transcribes verbatim into any category $𝒞$ with finite products: the equations become commutative diagrams, e.g. associativity becomes $$\begin{array}{ccc}\hfill G\times G\times G\hfill & \hfill \stackrel{m\times \mathrm{i}\mathrm{d}}{\to }\hfill & \hfill G\times G\hfill \\ \hfill \downarrow \mathrm{i}\mathrm{d}\times m\hfill & \hfill \hfill & \hfill \downarrow m\hfill \\ \hfill G\times G\hfill & \hfill \stackrel{m}{\to }\hfill & \hfill G\hfill \end{array}$$ This yields the category $𝐆𝐫𝐩\left(𝒞\right)$ of groups in $𝒞$: topological groups when $𝒞=𝐓𝐨𝐩$, Lie groups when $𝒞$ is a category of manifolds, and so on.

In general, an interpretation $I$ of a theory $𝕋$ in a finite-product category $𝒞$ assigns to the (single) sort an object $I$ and to each $f\in {\Sigma }_k$ a morphism $f^I:I^k\to I$. A term $t$ is always interpreted in a context $x_1,\dots ,x_n\mid t$ listing (at least) its variables, as a morphism $t^I:I^n\to I$: variables become product projections, and $f(t_1,\dots ,t_k)$ becomes $f^I\circ ⟨t_1^I,\dots ,t_k^I⟩$. The interpretation satisfies an equation $u=v$ in context when $u^I=v^I$ as morphisms $I^n\to I$, and it is a model when it satisfies all axioms. A homomorphism of models is a morphism of $𝒞$ commuting with the interpretations of all basic operations. This defines the category $Mod(𝕋,𝒞)$.

3.3 The Syntactic Category

A theory presented by operations and equations is like an algebra presented by generators and relations: useful, but presentation-bound. Group theory can equally be presented by a single binary “double division” operation and one exotic axiom; the concept presented is the same. The remedy is to package the theory itself as a category, remembering all derived operations and all provable equations while forgetting which were basic.⁹

One may think of ${𝒞}_{𝕋}$ as the Lindenbaum–Tarski category of $𝕋$: the syntax-invariant algebraic gadget presented by the theory. It carries a tautological model $U$: the underlying object is the singleton context $\left[x_1\right]$, and each $f\in {\Sigma }_k$ is interpreted as the morphism $[x_1,\dots ,x_k\mid f(x_1,\dots ,x_k)]$. Satisfaction in $U$ is provability: $$U\models s=t\iff 𝕋⊢s=t.$$

3.4 Models Are Functors; the Classifying Category

A finite-product category equipped with a model $U$ satisfying this universal property is called a classifying category for $𝕋$; it is unique up to equivalence, and the theorem says the syntactic category is one. Two consequences follow.

First, the correspondence gives a principled answer to “what is a theory?”: the category ${𝒞}_{𝕋}$ with its universal property, not any particular presentation. Second, the universal model $U$ is logically generic by (1): it satisfies all and only the provable equations. Classical, $𝐒𝐞𝐭$-valued semantics almost never provides such a single generic model; allowing models in arbitrary finite-product categories does.

3.5 Completeness

Completeness with respect to restricted classes of models then follows from embedding theorems, in a pattern that will repeat for the richer fragments:

3.6 The Four-Part Scheme, Reorganized

Awodey and Bauer summarize the reorganization that functorial semantics effects on the traditional picture of logic.¹³ Traditionally a logical system comprises: a type theory (calculus of types and terms); a logic (here, equational reasoning); a notion of theory (basic types, terms, axioms); and interpretations and models (denotational assignment of objects and morphisms, with satisfaction of axioms). Functorial semantics repackages all four: theories are structured categories; models are structure-preserving functors; homomorphisms are natural transformations—obtained “for free” from the functorial setting; and universal models exist, are logically generic, and reduce completeness to embedding theorems for classifying categories. This scheme is not special to algebraic theories: it is the template applied to each fragment in the sections that follow, and to higher-order logic in Part II.

4. Lawvere Duality and Abstract Algebraic Theories

4.1 Syntax Is Dual to Semantics

There is a remarkable duality, going back to Lawvere’s thesis, of the schematic form $$\text{𝐒𝐲𝐧𝐭𝐚𝐱}\simeq {\text{𝐒𝐞𝐦𝐚𝐧𝐭𝐢𝐜𝐬}}^{\mathrm{o}\mathrm{p}},$$ which is nearly invisible without categorical tools.¹⁴ Concretely:

The proof identifies the universal model inside ${Mod}_{\mathrm{f}\mathrm{g}}{\left(𝕋\right)}^{\mathrm{o}\mathrm{p}}$ as $U=F\left(1\right)$, the free model on one generator, with $U^n=F\left(n\right)$ (since free functors send coproducts of generating sets to coproducts of models, which become products in the opposite category). An $n$-ary term $t$ corresponds to the element $t(x_1,\dots ,x_n)\in F\left(n\right)$, hence—by freeness—to a homomorphism $F\left(1\right)\to F\left(n\right)$, which read in the opposite category is a morphism $U^n\to U$: exactly the interpretation of $t$. Provable equality of terms is equality of elements in the free model, so the syntactic category is faithfully reconstructed. An invariant copy of the syntax of $𝕋$ sits inside the opposite of its category of models, as the finitely generated free algebras.

4.2 Lawvere Algebraic Theories

Nothing in the duality depended on a syntactic presentation, which motivates the presentation-free notion:

Every Lawvere theory determines a syntactic theory whose $k$-ary operations are all morphisms $A^k\to A$, with an equation for every commuting diagram; and every syntactic theory determines a Lawvere theory, its syntactic category. The abstract notion covers examples where the operations come from mathematics rather than from a signature:¹⁵

4.3 Algebraic Categories and Monadicity

Which categories are categories of models of an algebraic theory? The classical answer within a fixed signature is Birkhoff’s HSP theorem (closure under homomorphic images, subalgebras, products). The presentation-free answer characterizes the forgetful functor:

The free model functor $F:𝐒𝐞𝐭\to Mod\left(𝐀\right)$ is constructed on finite sets as $F\left(n\right)={Hom}_{𝐀}(A^n,-)$—the representables are exactly the finitely generated free models, recovering Theorem 4.1 in the abstract setting—and extended to all sets by filtered colimits.

4.4 Algebraic Functors: Translations and their Semantics

A syntactic translation of theories is an FP-functor $T:𝐀\to 𝐁$; it induces a functor on semantics in the opposite direction by precomposition, $T^{*}\left(M\right)=M\circ T:Mod\left(𝐁\right)\to Mod\left(𝐀\right)$. Forgetful functors arise this way: the underlying-group functor $𝐑𝐢𝐧𝐠\to 𝐆𝐫𝐩$ is $T^{*}$ for the translation classifying the underlying group of the universal ring. Conversely, a functor $f:Mod\left(𝐁\right)\to Mod\left(𝐀\right)$ commuting with the forgetful functors is $T^{*}$ for an essentially unique generator-preserving translation $T$; and dropping generator-preservation, the semantic characterization of “definable” functors is: those preserving limits, filtered colimits, and regular epimorphisms (with theories taken Cauchy-complete). Every such $T^{*}$ has a left adjoint $T_{!}$, generalizing free constructions such as the free ring on a group.¹⁸

5. Interlude: Proofs as Morphisms and the $\lambda$-Calculus

Before climbing the first-order hierarchy, we pause for the proof-theoretic strand promised in the introduction: the Curry–Howard–Lambek correspondence, in which morphisms interpret proofs rather than provable containments.¹⁹

5.1 Cartesian Closed Categories

Two consequences of the adjunction deserve note. First, exponentials are automatically functorial, contravariantly in the exponent and covariantly in the base, and satisfy the expected isomorphisms $C^{A\times B}\cong {\left(C^B\right)}^A$ and ${(B\times C)}^A\cong B^A\times C^A$, all by Yoneda-style uniqueness arguments. Second, in a CCC the name of a morphism $f:A\to B$ is the point $⌜f⌝=\lambda (f\circ {\pi }_2):1\to B^A$: morphisms are internalized as elements of function objects.

5.2 Simply Typed $\lambda$-Calculus

The simply typed $\lambda$-calculus over a set of base types has types generated by $1,A\times B,A\to B$; terms generated by typed variables, pairing and projections, application $st$, the unit $*$, and abstraction $\lambda x^A.t$; and equations $$\left(\lambda x.t\right)s=t\left[s/x\right]\left(\beta \right),\lambda x.\left(tx\right)=t(x\notin t)\left(\eta \right),$$ plus the analogous laws for products. It is simultaneously a pure functional programming language and, by Curry–Howard, a proof calculus for minimal propositional logic: types are propositions ($\to$ is implication, $\times$ conjunction, $1$ truth), terms are proofs, and $\beta$-reduction is proof normalization (cut elimination).

This is the functorial-semantics template of §3 transposed to the proof-theoretic setting, with one important difference of grain: in Part I’s model-theoretic reading, a hom-poset records provability; here a hom-set records the proofs themselves, and equality of morphisms is the meaningful, decidable-by-normalization relation of $\beta \eta$-convertibility. The doctrinal tower of Part I has a parallel proof-relevant tower: monoidal categories interpret linear/ordered calculi, CCCs interpret the simply typed $\lambda$-calculus, locally cartesian closed categories interpret dependent type theory, and elementary toposes interpret full intuitionistic HOL.

5.3 Multicategories: Separating the Structural Rules

A sequent $A_1,\dots ,A_n⊢B$ has a list on the left. Interpreting the list as a product $A_1\times \cdots \times A_n$ works, but silently imports the structural rules—weakening, contraction, exchange—as properties of the diagonal and projections. Shulman’s systematic development therefore interposes multicategories: structures whose morphisms $(A_1,\dots ,A_n)\to B$ have finite lists as domains, with multi-composition but no assumption that the domain list is a product. Type theories present multicategories; requiring representability of the domain list by an object (via $\otimes$ or $\times$) then recovers monoidal or cartesian categories, and the choice of admissible structural rules—none, exchange only, all—selects the flavor of logic (linear, affine, ordered, intuitionistic).²⁰

5.4 Functional Completeness

A final CCC fact with logical meaning: for any object $A$ of a CCC $𝒞$, the slice-like category obtained by freely adjoining a point $x:1\to A$ (the polynomial category $𝒞\left[x\right]$) is again a CCC, and morphisms $B\to C$ in $𝒞\left[x\right]$ correspond to morphisms $A\times B\to C$ in $𝒞$. This is functional completeness: a term with a free variable of type $A$ is the same as a morphism from a product with $A$—the categorical justification for the deduction theorem, and the reason $\lambda$-abstraction is total.

6. First-Order Logic, Categorically

We now pass from equational logic to predicate logic, with connectives $\wedge ,\vee ,\Rightarrow ,\neg$ and quantifiers $\forall ,\exists$. The strategy is fixed by the template of Section 3: identify the categorical structure that models each logical operation (adjoints will do most of the work), study categories with that structure and functors preserving it, construct classifying categories, and derive completeness from embeddings.²¹

6.1 Why Equations Are Not Enough

Consider the property of a group of having no nontrivial square roots of unity: $$\forall x:G.(x\cdot x=e\Rightarrow x=e).$$ This is not equivalent to any system of equations. Yet its set-theoretic meaning suggests a categorical one: each of $x\cdot x=e$ and $x=e$ carves out a subset of $G$—an equalizer, hence available in any category with finite limits—and the implication asserts that the first subobject is contained in the second. Thus (2) can be interpreted in any finite-limit category as the requirement that one equalizer factor through another. The general scheme: formulas are interpreted as subobjects, and sequents $\phi ⊢\psi$ as containments $\left[\left[\phi \right]\right]\le \left[\left[\psi \right]\right]$ in a subobject poset.²²

6.2 The Shape of a First-Order Theory

A first-order theory $𝕋$ has two layers. The type-theoretic layer supplies sorts, function symbols with signatures $f:(A_1,\dots ,A_n;B)$, typing judgments $\Gamma \mid t:B$ for $\Gamma =(x_1:A_1,\dots ,x_n:A_n)$ a typing context, and equations between terms. The logical layer supplies relation symbols $R$ with signatures $(A_1,\dots ,A_n)$, formula judgments $\Gamma \mid \phi 𝗉𝗋𝖾𝖽$, and axioms in the form of sequents in context $$\Gamma \mid \phi ⊢\psi ,$$ read: in context $\Gamma$, hypothesis $\phi$ entails $\psi$. (With $\wedge$ available, finite lists of hypotheses reduce to a single one.) A fragment is fixed by choosing which logical operations may appear; the fragments of interest were tabulated in the introduction. Languages and theories are best not separated too strictly: in rich systems, well-formedness of terms can depend on provability—as when ${\int }_0^{\infty }f$ denotes a real number only if $f$ is integrable—so types and logic may be defined by mutual recursion.²³

6.3 Interpretation: The General Pattern

Fix a fragment and a category $𝒞$ with the corresponding structure. An interpretation assigns: to each sort $A$ an object $\left[\left[A\right]\right]$; to each context $\Gamma =(x_1:A_1,\dots ,x_n:A_n)$ the product $\left[\left[\Gamma \right]\right]=\left[\left[A_1\right]\right]\times \cdots \times \left[\left[A_n\right]\right]$; to each function symbol a morphism; to each relation symbol $R$ of signature $(A_1,\dots ,A_n)$ a subobject $\left[\left[R\right]\right]\rightarrowtail \left[\left[A_1\right]\right]\times \cdots \times \left[\left[A_n\right]\right]$; and then, by structural recursion:

• terms $\Gamma \mid t:B$ become morphisms $\left[\left[t\right]\right]:\left[\left[\Gamma \right]\right]\to \left[\left[B\right]\right]$ (variables are projections; application is composition);

• formulas $\Gamma \mid \phi$ become subobjects $\left[[\Gamma \mid \phi ]\right]\in Sub\left(\left[\left[\Gamma \right]\right]\right)$, using the categorical operation matching each connective;

• substitution into a term is composition; substitution of a term into a formula is pullback: $$\left[[\Gamma \mid \phi \left[t/y\right]]\right]={\left[\left[t\right]\right]}^{*}\left[[y:B\mid \phi ]\right].$$

A model of $𝕋$ is an interpretation validating every axiom $\Gamma \mid \phi ⊢\psi$ in the sense that $\left[[\Gamma \mid \phi ]\right]\le \left[[\Gamma \mid \psi ]\right]$ in $Sub\left(\left[\left[\Gamma \right]\right]\right)$.

6.4 Cartesian Logic

Cartesian logic is the fragment with $=,\top ,\wedge$ only, interpreted in cartesian categories: categories with all finite limits. Its deductive calculus consists of the structural rules (weakening, substitution, identity, cut), the truth rule $\psi ⊢\top$, the two-way conjunction rules, and the equality rules (reflexivity, and substitution of provably equal terms). The interpretation clauses: $\top$ is the top subobject; $R(t_1,\dots ,t_n)$ is the pullback of $\left[\left[R\right]\right]$ along $⟨\left[\left[t_1\right]\right],\dots ,\left[\left[t_n\right]\right]⟩$; $t{=}_{A}u$ is the equalizer of $\left[\left[t\right]\right],\left[\left[u\right]\right]$; conjunction is meet; weakening a formula from $\Gamma$ to $\Gamma ,x:A$ is pullback along the projection.

The proof is induction on derivations; the only interesting cases are substitution—sound because pullback functors are monotone—and the equality rule, where the key computation shows $\left[\left[t{=}_{A}u\right]\right]\wedge \left[\left[\phi \left[t/z\right]\right]\right]\le \left[\left[\phi \left[u/z\right]\right]\right]$ using the fact that the equalizer of $\left[\left[t\right]\right],\left[\left[u\right]\right]$ equalizes the graphs $⟨\mathrm{i}\mathrm{d},\left[\left[t\right]\right]⟩,⟨\mathrm{i}\mathrm{d},\left[\left[u\right]\right]⟩$ as well.²⁴

6.5 The Cartesian Calculus, Displayed

For reference, the full deductive calculus of the fragment, as a table of rules on sequents-in-context (context annotations suppressed when unchanged):²⁵ $$\begin{array}{cc}\text{𝖶𝖾𝖺𝗄𝖾𝗇𝗂𝗇𝗀}\hfill & \frac{\Gamma \mid \psi ⊢\phi }{\Gamma ,x:A\mid \psi ⊢\phi }\hfill \\ \text{𝖲𝗎𝖻𝗌𝗍𝗂𝗍𝗎𝗍𝗂𝗈𝗇}\hfill & \frac{\Gamma \mid t:A\Gamma ,x:A\mid \psi ⊢\phi }{\Gamma \mid \psi \left[t/x\right]⊢\phi \left[t/x\right]}\hfill \\ \text{𝖨𝖽𝖾𝗇𝗍𝗂𝗍𝗒, 𝖢𝗎𝗍}\hfill & \frac{}{\phi ⊢\phi }\frac{\psi ⊢\theta \theta ⊢\phi }{\psi ⊢\phi }\hfill \\ \text{𝖳𝗋𝗎𝗍𝗁}\hfill & \frac{}{\psi ⊢\top }\hfill \\ \text{𝖢𝗈𝗇𝗃𝗎𝗇𝖼𝗍𝗂𝗈𝗇}\hfill & \frac{\vartheta ⊢\phi \vartheta ⊢\psi }{\vartheta ⊢\phi \wedge \psi }\frac{\vartheta ⊢\phi \wedge \psi }{\vartheta ⊢\phi }\frac{\vartheta ⊢\phi \wedge \psi }{\vartheta ⊢\psi }\hfill \\ \text{𝖤𝗊𝗎𝖺𝗅𝗂𝗍𝗒}\hfill & \frac{}{\psi ⊢t{=}_{A}t}\frac{\psi ⊢t{=}_{A}u\psi ⊢\phi \left[t/z\right]}{\psi ⊢\phi \left[u/z\right]}\hfill \end{array}$$ Symmetry and transitivity of equality are derivable from the last rule (substitute into $z{=}_{A}t$ and $z{=}_{A}v$ respectively). Each subsequent fragment adds its rules on top: regular logic adds the two-way $\exists$-rule and Frobenius (§8); coherent logic the $\perp$-elimination and two-way $\vee$-rules with distributivity; Heyting logic the two-way rules for $\Rightarrow$ and $\forall$. In every case the “two-way” shape of a rule is the syntactic trace of an adjunction, per Section 7.

6.6 Separating the Fragments

That the hierarchy is strict is witnessed by theories expressible at one level and provably not below:

7. Quantifiers as Adjoints

7.1 The Fundamental Adjunctions

Let $f:A\to B$ in a category with pullbacks. Lawvere’s second great observation is that quantification along $f$ is adjoint to substitution along $f$: $${\exists }_f⊣f^{*}⊣{\forall }_f\begin{array}{cc}\hfill {\exists }_{f}U\le V& \iff U\le f^{*}V\hfill \\ \hfill f^{*}V\le U& \iff V\le {\forall }_{f}U\hfill \end{array}$$ For the projection $\pi :\left[\left[\Gamma \right]\right]\times \left[\left[A\right]\right]\to \left[\left[\Gamma \right]\right]$, these adjunctions are exactly the natural-deduction rules for the quantifiers. The left adjunction, unwound, says: $\exists x.\phi$ entails $\psi$ (no $x$ free in $\psi$) iff $\phi$ entails $\psi$; the right one similarly for $\forall$. The eigenvariable side condition of traditional proof theory is absorbed into the statement that one is transposing across an adjunction.

7.2 Beck–Chevalley and Frobenius

Two coherence conditions make the adjoints fit the logic.

Beck–Chevalley. Substitution must commute with quantification: syntactically, $(\exists y.\phi )\left[t/x\right]=\exists y.\left(\phi \left[t/x\right]\right)$ for $y$ not in $t$. Categorically: for every pullback square $$\begin{array}{ccc}\hfill A^{\prime }\hfill & \hfill \stackrel{g^{\prime }}{\to }\hfill & \hfill A\hfill \\ \hfill \downarrow f^{\prime }\hfill & \hfill \hfill & \hfill \downarrow f\hfill \\ \hfill B^{\prime }\hfill & \hfill \stackrel{g}{\to }\hfill & \hfill B\hfill \end{array}$$ one requires $g^{*}\circ {\exists }_f={\exists }_{f\prime }\circ g{\prime }^{*}$ (and dually for $\forall$). This is the stability, under pullback, of the quantifiers.

Frobenius. The law $\exists x.(\phi \wedge \psi )⊣⊢(\exists x.\phi )\wedge \psi$ (no $x$ in $\psi$) corresponds to $${\exists }_f(U\wedge f^{*}V)={\exists }_{f}U\wedge V.$$ In the presence of implication (right adjoints to $\wedge$), Frobenius is automatic; in its absence it must be imposed.²⁸

To summarize: interpreting a quantifier means having an adjoint to substitution, stable under pullback. The next two sections identify the categories in which the $\exists$-adjoint exists for the right class of maps.

8. Regular Categories and Regular Logic

Regular logic is the fragment $=,\top ,\wedge ,\exists$. It is the logic of images: the existential quantifier applied to a graph.

The mono part $m:\mathrm{i}\mathrm{m}\left(f\right)\rightarrowtail B$ of the factorization of $f:A\to B$ is the least subobject of $B$ through which $f$ factors: the image. Existential quantification along $f$ is then $${\exists }_f(U\rightarrowtail A)=\mathrm{i}\mathrm{m}(U\to A\to B),$$ and one checks: ${\exists }_f⊣f^{*}$ always; Beck–Chevalley holds because images are stable under pullback; Frobenius holds likewise. Thus a regular category interprets all of regular logic, soundly.

8.1 The Calculus of Relations

Regular categories are exactly the environment for a well-behaved algebra of relations, and this gives an alternative, quantifier-free face to regular logic.³¹

A relation $R:A\looparrowright B$ is a subobject $⟨r_0,r_1⟩:R\rightarrowtail A\times B$. Given also $S:B\looparrowright C$, form the pullback of $r_1$ against $s_0$ to obtain the object of “composable pairs” $R{\times }_{B}S$, map it to $A\times C$, and take the image: $$S\circ R=\mathrm{i}\mathrm{m}(R{\times }_{B}S\to A\times C).$$ In $𝐒𝐞𝐭$ this is the familiar $\{(a,c)\mid \exists b.R(a,b)\wedge S(b,c)\}$: relational composition is an image, i.e. an existential quantifier, which is why regularity (stable images) is exactly what makes composition associative. One obtains a locally ordered 2-category (indeed an allegory in Freyd’s sense) $\mathrm{R}\mathrm{e}\mathrm{l}\left(𝒞\right)$ with: identities the diagonals; an order $\le$ on parallel relations from $Sub(A\times B)$; an involution $R^{†}$ by swapping components; and meets inherited from subobjects. Morphisms of $𝒞$ embed as the relations whose graphs are single-valued and total: $f\mapsto ⟨\mathrm{i}\mathrm{d},f⟩$, and one recovers $𝒞$ inside $\mathrm{R}\mathrm{e}\mathrm{l}\left(𝒞\right)$ as the relations $R$ with $R{R}^{†}\le \mathrm{i}\mathrm{d}$ and $\mathrm{i}\mathrm{d}\le R^{†}R$.

The modular law is the relational avatar of Frobenius reciprocity, and in fact regular categories, unitary tabular allegories, and regular theories-as-syntax are three equivalent presentations of one subject: one can define a regular category as a category whose relations form an allegory with enough structure, and regular logic as the equational theory of that allegory. Statements provable in regular logic are exactly those stable under the relational translation—a quantifier-elimination phenomenon that partly explains the fragment’s tractability for automation (§9).

8.2 Regular Theories and their Classifying Categories

The functorial-semantics template runs as before. A regular theory is a set of regular sequents; a model in a regular category $𝒞$ is an interpretation validating them; homomorphisms are as expected. The syntactic regular category ${𝒞}_{𝕋}$ has as objects the formulas-in-context $[\overrightarrow{x}\mid \phi ]$ of the fragment, and as morphisms $[\overrightarrow{x}\mid \phi ]\to [\overrightarrow{y}\mid \psi ]$ the $𝕋$-provably-functional relations: regular formulas $\theta (\overrightarrow{x},\overrightarrow{y})$ such that $𝕋$ proves $\theta$ entails $\phi \wedge \psi$, that $\theta$ is single-valued, and that $\phi$ entails $\exists \overrightarrow{y}.\theta$. Then:

• ${𝒞}_{𝕋}$ is a regular category;

• there is a universal model $U_{𝕋}$ in ${𝒞}_{𝕋}$, and for every regular $𝒞$, evaluation at $U_{𝕋}$ gives an equivalence ${Hom}_{\mathrm{r}\mathrm{e}\mathrm{g}}({𝒞}_{𝕋},𝒞)\simeq Mod(𝕋,𝒞)$ with regular (finite-limit- and regular-epi-preserving) functors on the left;

• satisfaction in $U_{𝕋}$ coincides with provability, so the calculus of regular logic is strongly complete for categorical semantics.³²

Classical completeness—with respect to $𝐒𝐞𝐭$-models—then follows from an embedding theorem: every small regular category admits a conservative regular embedding into a presheaf category (via a regular-logic refinement of Yoneda), and evaluations are jointly faithful. Deeper representation theorems (the Barr embedding, and Deligne’s theorem in Part II) refine this pattern.

8.3 Soundness for the Regular Fragment, in Detail

To display the mechanics once at full magnification, here is the soundness argument for the two quantifier rules in a regular category $𝒞$, extending Theorem 6.1.³³

Rule ($\exists$-intro/elim as adjunction). The bidirectional rule $$\frac{\Gamma ,y:B\mid \phi ⊢\psi }{\Gamma \mid (\exists y.\phi )⊢\psi }\left(y\text{not free in}\psi \right)$$ is validated because, writing $\pi :\left[\left[\Gamma \right]\right]\times \left[\left[B\right]\right]\to \left[\left[\Gamma \right]\right]$, $$\left[[\exists y.\phi ]\right]={\exists }_{\pi }\left[\left[\phi \right]\right]\le \left[\left[\psi \right]\right]\iff \left[\left[\phi \right]\right]\le {\pi }^{*}\left[\left[\psi \right]\right],$$ and ${\pi }^{*}\left[\left[\psi \right]\right]$ is exactly the interpretation of $\psi$ weakened into the extended context: the adjunction is the rule.

Frobenius, used tacitly. The entailment $(\exists y.\phi )\wedge \chi ⊢\exists y.(\phi \wedge \chi )$ (no $y$ in $\chi$) requires ${\exists }_{\pi }\left(\left[\left[\phi \right]\right]\right)\wedge \left[\left[\chi \right]\right]\le {\exists }_{\pi }(\left[\left[\phi \right]\right]\wedge {\pi }^{*}\left[\left[\chi \right]\right])$, i.e. the Frobenius law. In a regular category, verify it on images: with $\left[\left[\phi \right]\right]=\left[m\right]$ and image factorizations as in Definition 8.1, both sides compute the image of the same composite, using stability of the factorization along the mono $\left[\left[\chi \right]\right]\rightarrowtail \left[\left[\Gamma \right]\right]$.

Substitution stability. Finally the substitution rule needs Beck–Chevalley: for a term $t$, the square $$\begin{array}{ccc}\hfill \left[\left[\Gamma \right]\right]\times \left[\left[B\right]\right]\hfill & \hfill \stackrel{⟨\mathrm{i}\mathrm{d},\left[\left[t\right]\right]⟩\times \mathrm{i}\mathrm{d}}{\to }\hfill & \hfill \left[\left[\Gamma \right]\right]\times \left[\left[A\right]\right]\times \left[\left[B\right]\right]\hfill \\ \hfill \downarrow \pi \hfill & \hfill \hfill & \hfill \downarrow \pi \hfill \\ \hfill \hfill & \hfill \stackrel{⟨\mathrm{i}\mathrm{d},\left[\left[t\right]\right]⟩}{\to }\hfill & \hfill \left[\left[\Gamma \right]\right]\times \left[\left[A\right]\right]\hfill \end{array}$$ is a pullback, so $⟨\mathrm{i}\mathrm{d},\left[\left[t\right]\right]{⟩}^{*}{\exists }_{\pi }={\exists }_{\pi }{(⟨\mathrm{i}\mathrm{d},\left[\left[t\right]\right]⟩\times \mathrm{i}\mathrm{d})}^{*}$: substituting into an existential equals existentially quantifying the substitution. All three verifications are one-line diagram chases given the standing stability hypotheses: the definition of regular category is reverse-engineered from exactly these proof obligations.

8.4 The Calculus of Relations, Revisited

Regular categories are exactly the environments supporting a well-behaved algebra of binary relations, a point worth making explicit both because it explains the axioms and because it opens the door to relational and allegorical formulations of logic.³⁴

A relation $R:A\looparrowright B$ is a subobject $R\rightarrowtail A\times B$. In a regular category, relations compose: given $S:B\looparrowright C$, form the pullback of $R\to B\leftarrow S$, obtaining an object of “matching pairs” mapping to $A\times C$, and let $S\circ R$ be its image: $$S\circ R=\mathrm{i}\mathrm{m}(R{\times }_{B}S\to A\times C).$$ Existential quantification (the image) is exactly what the composite $\exists b.R(a,b)\wedge S(b,c)$ requires.

Morphisms embed into relations via graphs, $f\mapsto ⟨\mathrm{i}\mathrm{d},f⟩$, and are characterized inside $\mathrm{R}\mathrm{e}\mathrm{l}\left(𝒞\right)$ as the maps: relations $F$ with $F^{†}F\ge \Delta$ (totality) and $F{F}^{†}\le \Delta$ (single-valuedness). This is the semantic counterpart of the provably-functional-relations device used to build the syntactic regular category in §8: there, syntax manufactured maps from functional relations; here, semantics recognizes them.

9. Coherent Logic

Coherent logic extends regular logic by finite disjunction: $=,\top ,\wedge ,\exists ,\perp ,\vee$. The corresponding categories:

In a coherent category the interpretation extends by $\left[\left[\perp \right]\right]=\perp$, $\left[[\phi \vee \psi ]\right]=\left[\left[\phi \right]\right]\vee \left[\left[\psi \right]\right]$, and distributivity of $\wedge$ over $\vee$—which follows from stability—keeps the calculus sound. Coherent sequents $\phi {⊢}_{\overrightarrow{x}}\psi$ between coherent formulas axiomatize coherent theories.

9.1 Metatheory: Undecidability and Automation

Coherent sequents have a distinctive proof theory: reading $\phi ⊢\exists \overrightarrow{y}.({\psi }_1\vee \cdots \vee {\psi }_k)$ as a forward-chaining rule (“from facts matching $\phi$, produce witnesses and case-split”), proof search becomes a breadth-first closure procedure requiring no clausification or Skolemization, and yielding proofs that are directly readable and directly formalizable. This makes the fragment well suited to automated reasoning—expressive, yet with transparent proofs:

• Bezem proved that provability in coherent logic is undecidable [17], so the fragment is no toy;

• Bezem & Coquand initiated its automation [18];

• Stojanović et al. built a coherent-logic geometry theorem prover producing formal and human-readable proofs [19] and designed a vernacular for coherent proofs [20];

• Avigad et al. gave a formal system for Euclid’s Elements whose inferences are essentially coherent [21];

• Ganesalingam & Gowers’s problem solver with human-style write-ups works in a closely related forward-reasoning regime [22].

10. Heyting Categories and Full First-Order Logic

10.1 Implication and Universal Quantification

To interpret $\Rightarrow ,\neg ,\forall$ we need right adjoints.

A Heyting category interprets full intuitionistic first-order logic soundly: all the rules of the intuitionistic sequent calculus are validated, but excluded middle $\top ⊢\phi \vee \neg \phi$ and double-negation elimination generally fail, because subobject lattices are Heyting but rarely Boolean. First-order classical logic corresponds to Boolean categories: Heyting categories in which every subobject is complemented.

10.2 Kripke Semantics as Presheaf Semantics

The classical completeness theorem for intuitionistic logic—Kripke’s theorem that a sequent is provable iff it holds in all Kripke models over all posets—becomes, categorically, completeness with respect to models in presheaf categories over posets: a Kripke model on a poset $P$ is exactly a model in ${𝐒𝐞𝐭}^P$ (sets varying over stages, growing along $P$; the forcing clauses are the pointwise formulas of Example 10.2). The two-step completeness scheme—embed the syntactic Heyting category generically, then evaluate—delivers this: the classifying Heyting category of an intuitionistic first-order theory embeds conservatively into a presheaf category over a poset.³⁷

10.3 The Hierarchy, Assembled

We may now read the table of §6 as a tower of forgetful/free relationships between 2-categories of structured categories: cartesian $\supset$ regular $\supset$ coherent $\supset$ Heyting, with structure-preserving functors and all natural transformations at each level, and with each fragment’s classifying category providing a left 2-adjoint to the inclusion of “semantics” into “syntax.” The hierarchy of logics is thus a hierarchy of doctrines—the subject of the next section.

11. Interlude: The Curry–Howard–Lambek Correspondence

Before ascending to doctrines, we pause for the proof-theoretic strand promised in §6, which runs parallel to the model-theoretic hierarchy and rejoins it inside the topos.³⁸

11.1 Cartesian Closed Categories, Again

A category is cartesian closed (a CCC) when it has finite products and exponentials: $Hom(C\times A,B)\cong Hom(C,B^A)$, naturally in all variables. Transposition sends $f:C\times A\to B$ to its currying $\lambda f:C\to B^A$; the counit is evaluation $\mathrm{e}\mathrm{v}:B^A\times A\to B$; and the triangle identities say exactly that $$\mathrm{e}\mathrm{v}\circ (\lambda f\times {\mathrm{i}\mathrm{d}}_A)=f,\lambda (\mathrm{e}\mathrm{v}\circ (g\times {\mathrm{i}\mathrm{d}}_A))=g,$$ which the reader should recognize, ahead of the formal statement, as the $\beta$ and $\eta$ laws of the $\lambda$-calculus.

11.2 The Simply Typed $\lambda$-Calculus

The simply typed $\lambda$-calculus ${\lambda }^{\to \times }$ over a set of base types has types generated by $1,A\times B,A\to B$; terms generated by variables, pairing $⟨s,t⟩$, projections, abstraction $\lambda x:A.t$, and application $st$; typing judgments $x_1:A_1,\dots ,x_n:A_n⊢t:B$ derived by the evident rules; and the equational theory generated by $$\left(\lambda x.t\right)s=t\left[s/x\right]\left(\beta \right),\lambda x.\left(tx\right)=t(x\notin t)\left(\eta \right),$$ together with the product laws. A $\lambda$-theory adds base constants and equational axioms.

The correspondence is the categorical leg of the Curry–Howard triangle:

Note the shift of dimension from Part I: there, a formula was a subobject and entailment a mere ordering; here, a proposition is an object and each proof is a distinct morphism. Categorical model theory truncates proofs to provability; categorical proof theory keeps them. The two reconcile in a topos, where a proposition may be regarded either as a subobject of $1$ (truncated) or as an arbitrary object under the propositions-as-types reading (untruncated), and where the support factorization mediates between them.

11.3 Multicategories, Again

Shulman’s notes [5] refine the correspondence using multicategories: structures whose morphisms $(A_1,\dots ,A_n)\to B$ have finite lists of inputs, composed by grafting. A sequent with $n$ hypotheses is interpreted as a multimorphism directly—no product needed—and the cartesian structure (the ability to duplicate and discard hypotheses, i.e. contraction and weakening) becomes a property of the multicategory rather than a consequence of re-encoding contexts as products. The payoff is modularity: dropping contraction and weakening yields linear logic and monoidal categories by the same machinery, and the two-step analysis (type theory $\leftrightarrow$ multicategory $\leftrightarrow$ representable structure) cleanly explains why the $\otimes$/$\times$ distinction tracks the structural rules. The syntax–structure correspondences of Part I are then two instances of a single pattern, one that covers substructural and higher-order logics as well.

12. Doctrines and Unifying Frameworks

12.1 Doctrines

The word doctrine, introduced in the wake of Lawvere’s work, names the organizing principle we have been using: a doctrine is a species of structured category, together with the functors preserving the structure—“categories with finite products,” “regular categories,” “Heyting categories,” “elementary toposes.” The term is old and useful but has never had a single fixed technical meaning.³⁹ Several formalizations coexist:

• Doctrines as 2-monads. Kelly & Street’s “Review of the elements of 2-categories” [7] develops monads in a 2-category; taking the 2-category to be $𝐂𝐚𝐭$, a doctrine is a (nice) 2-monad $D$ on $𝐂𝐚𝐭$, its algebras are the theories of the doctrine, and lax/pseudo/strict morphisms of algebras give the appropriate translations. “Categories with finite products” is the paradigm: the 2-monad freely adjoins finite products.

• Doctrines as indexed posets (Lawvere doctrines). A first-order doctrine in the sense that grew out of Lawvere’s “hyperdoctrines” is a functor $P:{𝒞}^{\mathrm{o}\mathrm{p}}\to 𝐏𝐨𝐬$—think ${Sub}_{𝒞}$—with adjoints to reindexing modeling the quantifiers, plus Beck–Chevalley and Frobenius. This viewpoint isolates the logical superstructure over a base of contexts, and supports modern developments: Dagnino & Rosolini [9] study modalities on doctrines and show how comonads on doctrines induce the box-like operators of modal logic, with quotients and comprehension treated uniformly.

• Doctrines in the physics literature. Paugam’s book on the mathematics of quantum field theory [8], Sec. 2.1, uses higher categories, doctrines, and theories as the organizing frame for the functor-of-points approach to spaces of fields.

12.2 Generalized Sketches

Ehresmann’s sketches present theories by specifying a small category together with chosen cones and cocones to be sent to limits and colimits—a graphical, universal-property-first alternative to logical syntax. Makkai’s three-part “Generalized sketches as a framework for completeness theorems” [10] widens the notion so that sketches can specify categorical doctrines themselves, especially (but not only) those based on universal properties, and equips the framework with both a model theory and a proof theory, each categorical in nature and each supporting completeness theorems.⁴⁰ The framework is a natural home for structures—like the internal categories of Example 6.3—that outrun simple multi-sorted signatures.

12.3 A Unified Framework for Algebraic Notions

Beyond Lawvere theories, twentieth-century algebra produced a zoo of “theory-like” gadgets: PROs and PROPs (product-and-permutation categories presenting operations with many inputs and outputs), symmetric and nonsymmetric operads, clones, monads. Fujii’s “A unified framework for notions of algebraic theory” [11] organizes the zoo: each notion of algebraic theory embeds into a single framework (via monoid objects in suitable monoidal categories indexed by a choice of “metatheory”), morphisms of metatheories transport theories and models, and the standard constructions—categories of models, free algebras, the passage to monads—become functorial in the metatheory.⁴¹

12.4 Bridge to Part II

The top row of our table remains: higher-order logic and elementary toposes. Everything in Part I concerned predicates over objects; nothing yet allows predicates to be collected into an object of predicates. The subobject classifier does exactly this, and a category with finite limits, exponentials, and a subobject classifier—an elementary topos—is a Heyting category with enough additional structure to interpret quantification over predicates, powersets, and hence intuitionistic higher-order logic in full.

Part II. Topos Theory

13. What Is a Topos?

13.1 The Slogan and its Limits

An elementary topos can be regarded as a category that is enough like the category of sets to interpret intuitionistic higher-order logic. In this sense topos theory is a branch of categorical logic. But that is only one of several ways of thinking about what a topos is.⁴² At least four complementary answers circulate:

1. A topos is a generalized universe of sets: a place in which to do mathematics, where the ambient logic may be intuitionistic and the axiom of choice may fail.

2. A topos is a generalized space: the category of sheaves on a site remembers the space (indeed improves on it), and geometric morphisms generalize continuous maps.

3. A topos is a theory: a Grothendieck topos classifies a geometric theory, and the topos is the theory’s presentation-invariant incarnation—the higher-order analogue of the classifying categories of Part I.

4. A topos is an algebraic object: a cartesian closed category with a subobject classifier, studied by universal-algebraic means, localizations, and 2-categorical structure.

13.2 A Capsule History

The concept has a double origin.⁴³ Around 1963 Lawvere set out to found mathematics on category theory, asking what makes the category of sets special purely in terms of objects and morphisms—a radical inversion of the membership-based axiomatics of set theory. In 1966 he encountered Grothendieck’s notion of topos (Greek: place), invented for algebraic geometry, where one cares not only whether a statement is true but where it is true—on which open subset two functions agree, for example. Grothendieck’s toposes are categories of sheaves on sites, conceived as places in which to do mathematics; they were introduced as the environment for the cohomology theories needed for the Weil conjectures. By 1971 Lawvere and Tierney had distilled and generalized the notion to the elementary topos: a finitary, first-order axiomatization—finite limits, exponentials, subobject classifier—encompassing Grothendieck’s examples and many more, with a notion of truth that has a general concept of space built in. Baez points to Voevodsky’s proof of Milnor’s conjecture, which uses simplicial sheaves, as a recent product of the geometric line of development.

14. Elementary Toposes: Definition and First Consequences

14.1 The Definition

14.2 Reading the Axioms in $𝐒𝐞𝐭$

In $𝐒𝐞𝐭$: (A) provides the empty set, singletons, products, disjoint unions, equalizers $\{x\mid f\left(x\right)=g\left(x\right)\}$, and quotients; (B) provides function sets $B^A$; and (C) is the two-element set: taking $\Omega =\{0,1\}$ with $𝗍𝗋𝗎𝖾=1$, functions $A\to \{0,1\}$ are exactly the characteristic functions of subsets. The classifier axiom asserts, in an arbitrary $ℰ$, the natural correspondence $$Sub\left(A\right)\cong ℰ(A,\Omega ),S\mapsto {\chi }_S,\chi \mapsto {\chi }^{*}\left(𝗍𝗋𝗎𝖾\right),$$ making $\Omega$ an object of truth values and making $Sub$ representable.⁴⁶

14.3 First Consequences

We will not prove these here—the systematic development is Mac Lane & Moerdijk [33], Ch. IV, with the logic-first route in Goldblatt [32] and the encyclopedic treatment in Johnstone [23], Part A—but each will be used below.

15. A Gallery of Toposes

The definition is best absorbed through examples. The following gallery is essentially Baez’s, down to his framing: different kinds of mathematicians will feel at home in different toposes.⁴⁷

The slogan is Baez’s; Blechschmidt’s “custom-tailored mathematical universes” [27], taken up in §21, develop it into a working method. One chooses the topos so that the mathematics of interest becomes native to it.

15.1 The Classifier Across the Gallery

We tabulate $\Omega$, and with it the flavor of truth, across the examples so far:

Reading the table, the classifier is a precise record of what kind of partiality the topos tolerates: symmetry classes, time to arrival, incidence, locality. Baez’s dictum that there is a topos for one’s specific needs (§15) can be sharpened: choosing a topos is choosing an $\Omega$, i.e. choosing what shall count as a degree of truth.

16. Presheaf Toposes and Generic Figures

Presheaf toposes deserve a section of their own: they are combinatorial, fully computable, and already exhibit almost every phenomenon that separates toposes from $𝐒𝐞𝐭$. This is the pedagogical thesis of Reyes–Reyes–Zolfaghari’s Generic figures and their glueings [30], a book that bridges Conceptual Mathematics and Mac Lane–Moerdijk: it introduces topos theory through presheaf toposes, viewed as categories of objects glued from “generic figures,” with a running cast of easily visualized examples.⁴⁸

16.1 $𝒞$-Sets and their Figures

Fix a small category $𝒞$. A $𝒞$-set (presheaf) is a functor $X:{𝒞}^{\mathrm{o}\mathrm{p}}\to 𝐒𝐞𝐭$; write $x\cdot f\in X\left(c\prime \right)$ for the action of $f:c\prime \to c$ on $x\in X\left(c\right)$. By Yoneda, $$X\left(c\right)\cong \widehat{𝒞}(\mathrm{y}c,X),$$ so elements of $X$ at stage $c$ are the same as maps from the representable $\mathrm{y}c=𝒞(-,c)$: the representables are the generic figures, and an arbitrary $𝒞$-set is a colimit of representables—a glueing of figures along the incidence relations encoded by $𝒞$. All limits and colimits are computed pointwise; exponentials are given by the Yoneda-forced formula $$Y^X\left(c\right)=\widehat{𝒞}(\mathrm{y}c\times X,Y),$$ and the subobject classifier by sieves, as follows.

16.2 The Heyting Operations on Sieves

The internal propositional connectives of $\widehat{𝒞}$ can be computed directly on sieves, and the formulas repay study: they are the Kripke clauses of §19 in embryo. For sieves $S,T$ on $c$:⁴⁹ $$\begin{array}{cc}\hfill S\wedge T& =S\cap T,S\vee T=S\cup T,\top =\text{all maps into}c,\perp =⌀,\hfill \\ \hfill (S\Rightarrow T)& =\{f:c\prime \to c\mid \forall g:c″\to c\prime .fg\in S\text{implies}fg\in T\},\hfill \\ \hfill \neg S& =\{f:c\prime \to c\mid \text{no}g\text{has}fg\in S\}.\hfill \end{array}$$ Meets and joins are computed pointwise, but implication is not: a transition $f$ belongs to $S\Rightarrow T$ only if the implication $S$-to-$T$ persists under all further transitions $g$. The quantification over the future is forced by the requirement that $S\Rightarrow T$ be a sieve—closed under precomposition—and it is the exact algebraic reason presheaf logic is intuitionistic: $S\cup \neg S$ need not contain ${\mathrm{i}\mathrm{d}}_c$ even when computed with the displayed $\neg$.

16.3 The Topos of Graphs, Worked in Detail

Let $𝒞$ be the category with two objects $V,E$ and two nonidentity arrows $s,t:V\rightrightarrows E$.⁵⁰ A presheaf $X$ on $𝒞$ is a pair of sets $X\left(E\right),X\left(V\right)$ with two maps $X\left(s\right),X\left(t\right):X\left(E\right)\rightrightarrows X\left(V\right)$: a directed multigraph, with $X\left(V\right)$ the vertices, $X\left(E\right)$ the edges, and the actions of $s,t$ giving source and target. The generic figures are $\mathrm{y}V$ (a single vertex) and $\mathrm{y}E$ (a single edge with its two, possibly distinct, endpoints); every graph is a glueing of copies of these along incidence.

The classifier. Sieves on $V$: either all of $\{{\mathrm{i}\mathrm{d}}_V\}$’s sieve or empty—two truth values for vertices, $\Omega \left(V\right)=\{1_V,0_V\}$. Sieves on $E$: a sieve may contain ${\mathrm{i}\mathrm{d}}_E$ (hence everything), or any subset of $\{s,t\}$; so $$\Omega \left(E\right)=\{\top ,\{s,t\},\{s\},\{t\},⌀\},$$ five truth values for edges. As a graph, $\Omega$ has two vertices ($𝗂𝗇$ and $𝗈𝗎𝗍$) and five edges: the classifying graph $$\top :𝗂𝗇\to 𝗂𝗇,\{s,t\}:𝗂𝗇\to 𝗂𝗇,\{s\}:𝗂𝗇\to 𝗈𝗎𝗍,\{t\}:𝗈𝗎𝗍\to 𝗂𝗇,⌀:𝗈𝗎𝗍\to 𝗈𝗎𝗍.$$ Given a subgraph $A\subseteq X$, the classifying map sends a vertex to $𝗂𝗇$ or $𝗈𝗎𝗍$ according to membership, and an edge $e$ to the record of how much of $e$ lies in $A$: the edge itself ($\top$); both endpoints but not the edge ($\{s,t\}$); only its source ($\{s\}$); only its target ($\{t\}$); or nothing ($⌀$).

Failure of classicality, concretely. Let $X$ be a single edge $e:v\to w$ and $A$ the subgraph $\{v\}$. Then $\neg A$ (the largest subgraph disjoint from $A$) is $\{w\}$: the edge $e$ is excluded because its source lies in $A$. Hence $\neg \neg A=\{v\}$… but now take $A=\{e$’s two endpoints$\}$: $\neg A=⌀$, so $\neg \neg A=X⊋A$. Double negation is a closure operator, not the identity: the internal logic of graphs is non-Boolean, and the picture shows exactly why—an edge cannot be separated from its endpoints.

16.4 Bi-Heyting Structure: The Two Negations

In a presheaf topos every subobject lattice $Sub\left(X\right)$ is not only a Heyting algebra but a co-Heyting algebra as well: joins have a left-adjoint-like “subtraction” $\backslash$ with $$U\le V\vee W\iff U\backslash V\le W,$$ making $Sub\left(X\right)$ bi-Heyting. Consequently there are two negations: $$\neg U=(U\Rightarrow \perp )=\text{largest subobject disjoint from}U,\sim U=(X\backslash U)=\text{smallest subobject with}U\vee \sim U=X.$$ In $𝐒𝐞𝐭$ the two coincide; in graphs they diverge. For the single-edge graph and $A=\{v\}$: $\neg A=\{w\}$ as above, while $\sim A=\{e,v,w\}=X$ minus nothing that can be removed—the edge must stay (to cover $X$) and drags both endpoints with it. In general $\neg U\le \sim U$, the discrepancy measuring the boundary of $U$. Reyes and collaborators build modal operators by iterating combinations of the two negations, and argue in “The non-boolean logic of natural language negation” [31] that natural-language negation tracks the co-Heyting $\sim$ rather than the Heyting $\neg$: the negation of a predicate keeps its presuppositional boundary, as $\sim$ does and $\neg$ does not.⁵¹

16.5 Dynamical Systems and Other Small Presheaf Toposes

Two more base categories from the Reyes–Reyes–Zolfaghari cast—monoid actions and “bouquets”—show how much variety two or three arrows can generate.⁵²

16.6 Points of a Presheaf Topos

A point of $\widehat{𝒞}$ (geometric morphism from $𝐒𝐞𝐭$; §20) corresponds, by Diaconescu’s other theorem, to a flat functor $F:𝒞\to 𝐒𝐞𝐭$—one whose category of elements is cofiltered—with the inverse image given by the tensor $X\mapsto X{\otimes }_{𝒞}F$. For the graph base category, flatness works out to: a point is a choice of “way of looking at a graph through one figure at a time,” and the two obvious points are evaluation-at-$V$ and evaluation-at-$E$; these are jointly faithful and jointly conservative, which is why graph-theoretic statements can be checked on vertices and edges separately. For $M$-sets the points are the flat $M$-sets; for evolutive sets, evaluation at the unique stage. Presheaf toposes thus have enough points, all of an essentially combinatorial nature.

16.7 Exponentials of Graphs, Computed

The exponential formula $Y^X\left(c\right)=\widehat{𝒞}(\mathrm{y}c\times X,Y)$ becomes concrete, and instructive, for graphs. Vertices of $Y^X$ are graph morphisms $\mathrm{y}V\times X\to Y$. Now $\mathrm{y}V\times X$ is the vertex part of $X$: all vertices, no edges. So a vertex of $Y^X$ is any function from vertices of $X$ to vertices of $Y$—no edge-preservation required. Edges of $Y^X$ are morphisms $\mathrm{y}E\times X\to Y$; unwinding, $\mathrm{y}E\times X$ consists of two disjoint copies of the vertices of $X$ (the source copy and target copy) together with, for every edge of $X$, an edge from its source in the source copy to its target in the target copy. An edge of $Y^X$ from vertex-function $g_0$ to vertex-function $g_1$ is therefore an assignment sending each edge $x:u\to v$ of $X$ to an edge $g\left(x\right):g_0\left(u\right)\to g_1\left(v\right)$ of $Y$.

Thus $Y^X$ is a graph whose vertices are arbitrary vertex-maps and whose edges are “edge-maps between possibly different vertex-maps”: graph homomorphisms $X\to Y$ appear not as the vertices of $Y^X$ but as its loops—an edge from $g_0$ to $g_0$ covering it. The global points $1\to Y^X$, since $1$ is the single loop, likewise pick out the honest homomorphisms. This generalizes the $G$-set phenomenon of Example 15.3: in a presheaf topos, the function object $Y^X$ must contain enough “unnatural” would-be morphisms for the adjunction to hold, and the genuinely structure-preserving ones are recovered as the fixed or looped elements.⁵³

16.8 Evolutive Sets: Presheaves as Time

A second running example of [30]: take $𝒞=(\mathbb{N},\le )$, or any linear order of instants. A presheaf $X$ on ${𝒞}^{\mathrm{o}\mathrm{p}}$—equivalently a copresheaf, sets evolving forward—assigns to each instant $n$ a set $X_n$ and to each passage $n\le m$ a transition $X_n\to X_m$: an evolutive set, in which elements may merge (transitions need not be injective) and may be born (need not be surjective). The truth values at instant $n$ are the sieves on $n$, i.e. the up-closed sets of later instants: a truth value is a time of becoming true—true now, true from tomorrow, true eventually-at-$k$, never true. Negation reads “will never be true from any accessible future,” so $\neg \neg \phi$ says that $\phi$ remains possible at every future instant—which is clearly weaker than $\phi$ being true now, and this is exactly how $\neg \neg \phi \Rightarrow \phi$ fails. The double-negation topology of §17 forces exactly the “eventually constant” sheaves, Kostecki [28] uses this example to motivate the stage-dependent reading of presheaf semantics; it is also the simplest nontrivial Kripke frame, making §19 computable by hand.

17. Sheaves and Grothendieck Toposes

17.1 From Spaces to Sites

Let $X$ be a topological space. A presheaf on $X$ is a presheaf on the poset $𝒪\left(X\right)$ of opens; a sheaf is a presheaf $F$ satisfying the glueing condition: for every open cover $U={\bigcup }_i{U}_i$, a family of sections $s_i\in F\left(U_i\right)$ agreeing on overlaps glues to a unique $s\in F\left(U\right)$. Continuous functions, smooth functions, sections of a bundle: the fundamental objects of geometry are sheaves, and $\mathrm{S}\mathrm{h}\left(X\right)$ is a topos.

Grothendieck’s generalization replaces $𝒪\left(X\right)$ by any small category $𝒞$ equipped with a Grothendieck topology $J$: an assignment to each object $c$ of a collection $J\left(c\right)$ of covering sieves, required to contain the maximal sieve, to be stable under pullback, and to satisfy a transitivity (local character) axiom. The pair $(𝒞,J)$ is a site, and $\mathrm{S}\mathrm{h}(𝒞,J)\subseteq \widehat{𝒞}$ is the full subcategory of presheaves satisfying descent for covering sieves. A Grothendieck topos is a category equivalent to some $\mathrm{S}\mathrm{h}(𝒞,J)$.

The subobject classifier of $\mathrm{S}\mathrm{h}(𝒞,J)$ refines the sieve formula: ${\Omega }_J\left(c\right)$ is the set of $J$-closed sieves on $c$, a sieve $S$ being closed when any $f$ that is “covered into” $S$ already belongs to $S$. For $\mathrm{S}\mathrm{h}\left(X\right)$ this specializes to: $\Omega \left(U\right)=\{\text{open subsets of}U\}$, and the truth value of a statement is literally the largest open set on which it holds—Grothendieck’s “where is it true?” made formal.

17.2 Lawvere–Tierney Topologies

The elementary-topos abstraction of a Grothendieck topology is internal: a Lawvere–Tierney topology on a topos $ℰ$ is a morphism $j:\Omega \to \Omega$ with $$j\circ 𝗍𝗋𝗎𝖾=𝗍𝗋𝗎𝖾,j\circ j=j,j\circ \wedge =\wedge \circ (j\times j):$$ an internal closure/modal operator (“it is locally the case that”). Each $j$ determines a closure of subobjects $U\mapsto \bar{U}$, a notion of $j$-dense mono, and a subtopos ${\mathrm{S}\mathrm{h}}_j\left(ℰ\right)\subseteq ℰ$ of $j$-sheaves, again with finite-limit-preserving reflector. On a presheaf topos, Lawvere–Tierney topologies correspond exactly to Grothendieck topologies on the base; but the notion applies to any topos, and two special cases matter for logic:

• the double-negation topology $j=\neg \neg$, whose sheaves form the largest Boolean subtopos ${\mathrm{S}\mathrm{h}}_{\neg \neg }\left(ℰ\right)$, which is where classical logic reappears; it is used in the topos-theoretic independence proofs (Cohen forcing = sheaves for a $\neg \neg$-like topology on a poset of conditions);

• open and closed topologies induced by a truth value $u\in Sub\left(1\right)$, giving the open and closed subtoposes into which $ℰ$ decomposes.

18. The Internal Logic I: The Mitchell–Bénabou Language

18.1 Formulas as Morphisms to $\Omega$

Part I interpreted logic about a category from outside. A topos supports a slicker, self-contained idiom: since $Sub\left(A\right)\cong ℰ(A,\Omega )$, predicates are morphisms into $\Omega$, and the whole apparatus of Part I can be internalized as a typed language whose types and terms are the objects and morphisms of $ℰ$. This is the Mitchell–Bénabou language of $ℰ$.⁵⁵

The language has:

• types: the objects of $ℰ$, closed under $\times$, ${(-)}^{(-)}$, and $P(-)={\Omega }^{(-)}$;

• terms: built from typed variables by pairing, projection, application, $\lambda$-abstraction, and the morphisms of $ℰ$ as function symbols; a term $\sigma$ of type $B$ with free variables of types $A_1,\dots ,A_n$ denotes a morphism $\left[\left[\sigma \right]\right]:A_1\times \cdots \times A_n\to B$;

• formulas: terms of type $\Omega$. Atomic formulas include $\sigma {=}_B\tau$ (denoting ${\chi }_{\Delta }\circ ⟨\left[\left[\sigma \right]\right],\left[\left[\tau \right]\right]⟩$) and $\sigma {\in }_B\rho$ for $\rho$ of type $PB$ (denoting evaluation composed with the membership relation ${\in }_B\rightarrowtail B\times PB$); compound formulas are formed by composing with the internal Heyting operations on $\Omega$; and quantified formulas $\forall x.\phi$, $\exists x.\phi$ are formed by applying the adjoints ${\forall }_{\pi },{\exists }_{\pi }$ to the subobject denoted by $\phi$ and reconverting to characteristic morphisms.

Thus every formula $\phi (x_1,\dots ,x_n)$ has an extension $\{(x_1,\dots ,x_n)\mid \phi \}\rightarrowtail A_1\times \cdots \times A_n$, and a sequent $\phi ⊢\psi$ holds in $ℰ$ when the extension of $\phi$ is contained in that of $\psi$. A formula is true when its extension is the whole product—equivalently, when $\left[\left[\phi \right]\right]$ factors through $𝗍𝗋𝗎𝖾$.

18.2 What the Language Is for

The point is expressive economy: one reasons about the objects of an arbitrary topos as if they were sets, writing element-wise definitions and proofs, provided one reasons intuitionistically. Three illustrations:

19. The Internal Logic II: Kripke–Joyal Semantics

19.1 Forcing

The Mitchell–Bénabou language says what formulas denote; Kripke–Joyal semantics says how to compute whether they hold, by unwinding extensions stage by stage. For a formula $\phi \left(x\right)$ with $x$ of type $A$, an object $U$, and a generalized element $\alpha :U\to A$, define $$U⊩\phi \left(\alpha \right):\iff \alpha {\in }_A\{x\mid \phi \},$$ i.e. $\alpha$ factors through the extension of $\phi$. The forcing relation obeys two structural laws—monotonicity (if $U⊩\phi \left(\alpha \right)$ and $f:U\prime \to U$ then $U\prime ⊩\phi \left(\alpha f\right)$) and local character (if $\{f_i:U_i\to U\}$ is jointly epic and $U_i⊩\phi \left(\alpha f_i\right)$ for all $i$, then $U⊩\phi \left(\alpha \right)$)—and is computed by structural recursion:⁵⁶ $$\begin{array}{cc}\hfill U⊩(\sigma =\tau )\left(\alpha \right)& \iff \left[\left[\sigma \right]\right]\alpha =\left[\left[\tau \right]\right]\alpha ;\hfill \\ \hfill U⊩(\phi \wedge \psi )\left(\alpha \right)& \iff U⊩\phi \left(\alpha \right)\text{and}U⊩\psi \left(\alpha \right);\hfill \\ \hfill U⊩(\phi \vee \psi )\left(\alpha \right)& \iff \text{there is a jointly epic}\{f_i:U_i\to U\}\text{with each}{U}_i\text{forcing}\phi \left(\alpha f_i\right)\text{or}\psi \left(\alpha f_i\right);\hfill \\ \hfill U⊩(\phi \Rightarrow \psi )\left(\alpha \right)& \iff \text{for all}f:U\prime \to U:U\prime ⊩\phi \left(\alpha f\right)\text{implies}U\prime ⊩\psi \left(\alpha f\right);\hfill \\ \hfill U⊩\neg \phi \left(\alpha \right)& \iff \text{for all}f:U\prime \to U:U\prime ⊩\phi \left(\alpha f\right)\text{implies}U\prime \cong 0;\hfill \\ \hfill U⊩(\exists y.\phi )\left(\alpha \right)& \iff \text{there is an epi}p:U\prime \twoheadrightarrow U\text{and}\beta :U\prime \to B\text{with}U\prime ⊩\phi (\alpha p,\beta );\hfill \\ \hfill U⊩(\forall y.\phi )\left(\alpha \right)& \iff \text{for all}f:U\prime \to U\text{and all}\beta :U\prime \to B:U\prime ⊩\phi (\alpha f,\beta ).\hfill \end{array}$$ Truth of $\phi$ is $1⊩\phi$ with the generic (identity) element. Note where the intuitionism lives: disjunction and existence hold only locally—after passing to a cover—and implication and universal quantification must be stable—they quantify over all later stages.

19.2 Specializations

19.3 Soundness, Completeness, and Use

Kripke–Joyal semantics is sound and complete for the internal logic: a sequent holds in $ℰ$ iff it is forced at every stage—this is just the definition unwound—and the internal logic itself is sound for intuitionistic higher-order deduction. The working consequence:

This transfer principle is used constantly in the applications of §21.

19.4 Two Worked Applications of Forcing

20. Geometric Morphisms

20.1 Definition and Provenance

Toposes form a 2-category, in two inequivalent ways. Logical functors preserve all the elementary structure (finite limits, exponentials, $\Omega$)—the right notion for the “topos as theory of sets” reading. Geometric morphisms track the geometry:

The paradigm: a continuous map $g:X\to Y$ of spaces induces $g^{*}⊣g_{*}$ between $\mathrm{S}\mathrm{h}\left(X\right)$ and $\mathrm{S}\mathrm{h}\left(Y\right)$, and for sober spaces every geometric morphism arises so; points of $\mathrm{S}\mathrm{h}\left(X\right)$ recover the points of $X$. Likewise sheafification exhibits $\mathrm{S}\mathrm{h}(𝒞,J)\hookrightarrow \widehat{𝒞}$ as a geometric embedding, and every Grothendieck topos sits so inside a presheaf topos. Kostecki’s introduction emphasizes the resulting two-level variability: objects of a presheaf topos are structures varying over internal stages, and geometric morphisms let entire theories be transported between toposes, each topos giving the theory its own interpretation.⁶⁰

20.2 Inverse Images Preserve Geometric Logic

Because $f^{*}$ preserves finite limits and (being a left adjoint) all colimits, it preserves exactly the ingredients of geometric logic: $\top ,\wedge ,=,\exists ,\bigvee$. It need not preserve $\Rightarrow ,\forall ,\neg$. This is the structural explanation of the privileged status of geometric theories announced in §9: models of a geometric theory transport along inverse images, so each geometric theory $𝕋$ has a classifying topos $𝐒𝐞𝐭\left[𝕋\right]$ with $$\mathrm{G}\mathrm{e}\mathrm{o}\mathrm{m}(ℱ,𝐒𝐞𝐭\left[𝕋\right])\simeq Mod(𝕋,ℱ)$$ naturally—the higher-order terminus of the classifying-category tower of Part I. The object classifier $𝐒𝐞𝐭\left[𝕆\right]$ (presheaves on ${𝐒𝐞𝐭}_{\mathrm{f}\mathrm{i}\mathrm{n}}$), the ring classifier (presheaves on finitely presented rings), and the local-ring classifier (the Zariski topos) are the standard first examples; the last returns the story to Grothendieck’s algebraic geometry.

20.3 Classifying Toposes, Worked a Little

The correspondence $\mathrm{G}\mathrm{e}\mathrm{o}\mathrm{m}(ℱ,𝐒𝐞𝐭\left[𝕋\right])\simeq Mod(𝕋,ℱ)$ unwinds in two cases.

21. Toposes as Mathematical Universes

21.1 Set-Like Structure: NNO, Choice, Booleanness

How much of set theory does a topos support? The elementary axioms give pairing, powersets ($PA={\Omega }^A$), function spaces, and comprehension (extensions of formulas). The remaining classical commitments become optional axioms, each with a clean categorical form:

• Infinity. A natural numbers object is $0:1\to N$, $s:N\to N$ initial among such data: for any $x:1\to X$, $f:X\to X$ there is a unique recursion map $N\to X$. $𝐒𝐞𝐭$ and $\widehat{𝒞}$ have NNOs (constant presheaf $\mathbb{N}$); ${𝐒𝐞𝐭}_{\mathrm{f}\mathrm{i}\mathrm{n}}$ does not—infinity is a feature one adds, not part of the notion of topos.

• Excluded middle. $ℰ$ is Boolean when $\Omega$ is an internal Boolean algebra (equivalently every subobject is complemented; equivalently $\neg \neg =\mathrm{i}\mathrm{d}$). $𝐒𝐞𝐭$, ${𝐒𝐞𝐭}_{\mathrm{f}\mathrm{i}\mathrm{n}}$, $G$-sets are Boolean; graphs and almost all sheaf toposes are not.

• Choice. $ℰ$ satisfies AC when every epi splits. AC implies Booleanness (Diaconescu’s theorem: choice yields excluded middle), and fails already in $G$-sets for nontrivial $G$ (the epi $G_{\text{regular}}\to 1$ has no equivariant splitting) and in sheaves over most spaces (no continuous choice of local sections).

• Two-valuedness and well-pointedness. $Sub\left(1\right)$ may be large ($Sub\left(1\right)\cong 𝒪\left(X\right)$ in $\mathrm{S}\mathrm{h}\left(X\right)$: the truth values are the opens); a topos is two-valued when $Sub\left(1\right)=\{0,1\}$ and well-pointed when $1$ generates. Well-pointed toposes with NNO and AC are exactly the models of Lawvere’s Elementary Theory of the Category of Sets (ETCS), a structural set theory of strength just below ZF; adding replacement-style axioms calibrates the gap.⁶¹

21.2 Arithmetic from the NNO

The NNO’s universal property is precisely primitive recursion at higher types, and here is how ordinary arithmetic falls out. Given the data $0:1\to N$, $s:N\to N$, define addition by recursion in the second argument: the maps ${\mathrm{i}\mathrm{d}}_N:N\to N$ and $s\circ (-)$ exhibit $N^N$ as a recursion-algebra, and currying the unique mediating map $N\to N^N$ gives $+:N\times N\to N$ with $$x+0=x,x+s\left(y\right)=s(x+y),$$ these equations holding as identities of morphisms, hence internally with full generality. Multiplication and exponentiation iterate the trick. Induction is then a theorem of the internal logic: for a subobject $P\rightarrowtail N$ containing $0$ and closed under $s$, the universal property applied to $P$’s own zero-and-successor data produces a section of the inclusion, forcing $P=N$. Peano arithmetic (in its higher-order, categorical form) thus holds in any topos with NNO—with the caveat that the ambient logic is intuitionistic, so e.g. trichotomy for the internal integers holds but analogous statements for the internal reals of the next subsection do not.

21.3 Diaconescu’s Argument, and Internal Number Systems

Proof sketch. Fix a truth value $p\in Sub\left(1\right)$; we produce its complement. Consider the two-element quotient: internally, form the set $Q=\{x\in 2\mid x=0\vee x=1\vee p\}/\sim$ where $\sim$ identifies $0\sim 1$ iff $p$ holds. The evident surjection $2\twoheadrightarrow Q$ splits by AC; a splitting selects representatives $r\left(\left[0\right]\right),r\left(\left[1\right]\right)\in 2$, and equality in $2$ is decidable, so internally either $r\left(\left[0\right]\right)=r\left(\left[1\right]\right)$—which forces $p$—or $r\left(\left[0\right]\right)\ne r\left(\left[1\right]\right)$—which forces $\neg p$, since $p$ would identify the classes. Hence $p\vee \neg p$ holds; as $p$ was arbitrary, $\Omega$ is Boolean. The argument is fully constructive in the metatheory and formalizes verbatim in the internal language; its moral is that choice smuggles in case-analysis.⁶²

Internal number systems. With an NNO $N$, the internal integers and rationals are constructed as in constructive set theory (quotients of $N\times N$, etc.), uniquely up to isomorphism. The reals bifurcate: Cauchy reals (equivalence classes of internal Cauchy sequences) and Dedekind reals (two-sided cuts in $\mathbb{Q}$) agree in $𝐒𝐞𝐭$ but not in general—in $\mathrm{S}\mathrm{h}\left(X\right)$ the Dedekind reals are the sheaf of continuous real-valued functions on $X$: real analysis internal to $\mathrm{S}\mathrm{h}\left(X\right)$ is automatically parametrized real analysis, a first instance of the tailoring theme of the next subsection. Internal completeness, Heine–Borel, and the intermediate value theorem then hold or fail according to the constructive status of their proofs—IVT, whose usual proof uses undecidable case-splitting on the sign of $f\left(m\right)$, fails sheaf-internally in general, while its approximate version survives.

21.4 Custom-Tailored Universes

Blechschmidt’s survey “Exploring mathematical objects from custom-tailored mathematical universes” [27] distills the working method that the internal language makes possible.⁶³ Each topos is a universe with its own ambient assumptions: the effective topos, where all functions are computable; smooth toposes, where infinitesimals exist and all functions are smooth; sheaf toposes over a space, where everything varies continuously over that space. The method:

1. choose or build a topos $ℰ$ whose native objects are the structures of interest (e.g. $\mathrm{S}\mathrm{h}\left(X\right)$ for a scheme or space $X$, with the structure sheaf ${𝒪}_X$ a native ring);

2. prove theorems inside $ℰ$ constructively, treating those objects as bare sets/rings/modules;

3. translate outward through Kripke–Joyal (Slogan 19.6): a constructive theorem about the internal ring ${𝒪}_X$ becomes, externally, a theorem about the sheaf, often one whose direct proof would require delicate glueing or finiteness bookkeeping. Blechschmidt’s flagship examples are of this shape: e.g. internal one-line arguments specializing to Grothendieck-style generic freeness over reduced schemes.

Two refinements complete the toolkit. First, the choice of topos can encode hypotheses: passing to ${\mathrm{S}\mathrm{h}}_{\neg \neg }$ or to Barr covers (§20) adjusts the ambient logic. Second, the failure of classical axioms is a feature: that the smooth topos refutes $\neg (D\ne \{0\})$-style classicality is exactly what permits honest nilpotent infinitesimals; that the effective topos refutes “every function $\mathbb{N}\to \mathbb{N}$ is dominated by a computable one”-negations is what makes it a universe of computability.

21.5 Forcing, Classically: Independence via $\neg \neg$-Sheaves

The Lawvere–Tierney machinery reproduces Cohen’s independence proofs in a form that is one of the subject’s founding applications.⁶⁴ To violate the continuum hypothesis: take the poset $P$ of finite partial functions $\kappa \times \mathbb{N}\rightharpoonup 2$ (Cohen conditions) for $\kappa$ a suitably large cardinal, form the presheaf topos ${𝐒𝐞𝐭}^{P^{\mathrm{o}\mathrm{p}}}$, and pass to the Boolean subtopos ${\mathrm{S}\mathrm{h}}_{\neg \neg }$ of double-negation sheaves. The result is a Boolean topos with choice in which the generic function forces $2^{{\aleph }_0}\ge \kappa$; cutting down to a well-pointed model (or reading the construction as Boolean-valued sets) yields the classical independence of CH from ZFC. The conceptual gain over the classical presentation: the “forcing language” is the internal language, the “forcing relation” is Kripke–Joyal, and the passage to $\neg \neg$-sheaves is the standard subtopos machinery of §17—no new metamathematics, only a change of universe. Independence proofs thus join synthetic differential geometry and computability as instances of the single method of this section: choose the topos in which the desired phenomenon is generic.

21.6 The Higher-Order Classifying Correspondence

The two parts of these notes fit together as follows. Part I: a theory in a fragment of first-order logic generates a classifying category in the matching doctrine, and models are structure-preserving functors out of it. Part II: an intuitionistic higher-order theory generates a syntactic topos, its universal model living inside; conversely every topos is the classifying topos of its own internal theory. Sound and complete rules for the internal logic are those of intuitionistic HOL; Booleanness, choice, infinity are optional axioms locating $𝐒𝐞𝐭$ within the space of all universes. Functorial semantics, which began with one-sorted equational logic, extends all the way up.⁶⁵

22. A Guide to the Literature

22.1 Topos Theory, in Increasing Order of Difficulty

A rough order of increasing difficulty; the one-line characterizations follow Baez’s reading advice.⁶⁶

1. Lawvere & Schanuel [29]: elementary introduction to the topos of sets; deceptively gentle—Baez passes on Schanuel’s warning that skipping the exercises makes the later chapters impossible.

2. Reyes, Reyes & Zolfaghari [30]: combinatorial (presheaf) toposes via generic figures and glueings; the missing link before the graduate texts; six running examples, including the graphs of §16; Sec. 9.1 for the two negations.

3. Goldblatt [32]: same level, logic-first; starts from scratch with categories; criticized by experts as showing what toposes illuminate rather than what they can do, which is precisely what a beginner wants.

4. Mac Lane & Moerdijk [33]: the standard graduate text, broad and deep, unifying the geometric and logical lineages; Secs. VI.5–VI.6 for the internal language and forcing.

5. Johnstone [23]: the Elephant, “the bible of topos theory”—two of three projected volumes published, roughly 1200 pages, organized by the perspectives of §13; sequel to the 1977 Topos Theory [24], long the key text and famously unforgiving.

Shorter on-ramps: Baez’s nutshell [25] and eight Azimuth lectures [26]; Kostecki’s guided tour [28]; Blechschmidt’s survey [27] for the universes-and-applications viewpoint.

22.2 Categorical Logic

Start with Awodey & Bauer [4] (algebraic theories and first-order fragments, the backbone of Part I), then Shulman [5] for the type-theoretic, multicategorical development; Abramsky & Tzevelekos [2] for a compact introduction from the computer-science side; Bell [1] for history; and Johnstone [23], Parts A and D, as the reference of record. For the regular and coherent fragments specifically: van Oosten [12], Butz [13], Gran [14], Borceux [15], and Reyes [16]. For the organizing frameworks: Kock & Reyes [6], Kelly & Street [7], Dagnino & Rosolini [9], Paugam [8], Makkai [10], and Fujii [11].

23. Exercises

The following exercises track the text; those marked $*$ require material from the cited sources beyond what is developed here.

23.1 Part I

1. Verify that the two-pullbacks lemma (Lemma 2.1) makes $Sub$ a functor ${𝒞}^{\mathrm{o}\mathrm{p}}\to 𝐏𝐨𝐬$, checking independence of the choice of pullbacks.

2. Show that in $𝐒𝐞𝐭$, ${\exists }_f⊣f^{*}⊣{\forall }_f$ with the formulas of §7, and verify Beck–Chevalley and Frobenius by direct computation.

3. Write out the theory of a single idempotent endomorphism ($e\circ e=e$) and describe its syntactic category and its category of $𝐒𝐞𝐭$-models. What are the finitely generated free models?

4. Prove that the category of fields has neither products nor a terminal object, and locate exactly which limits exist. Conclude again (Example 4.10) that fields are not algebraic, and determine which fragment of §6’s table first suffices to axiomatize them.

5. Show that a poset in the topos of graphs is a graph whose vertex-set and edge-set each carry a poset structure compatibly with source and target, and characterize reflexivity internally.

6. In a regular category, prove that the composition of relations (§8.1) is associative, indicating precisely where pullback-stability of images is used.

7. ($*$) Following [4], Sec. 2.5, construct the classifying regular category of the theory of a surjection between two sorts, and identify its universal model.

8. Show that in any coherent category, $\wedge$ distributes over $\vee$ in every $Sub\left(A\right)$, using stability of joins.

9. Verify the Kripke clause for $\Rightarrow$ in Example 10.2 directly from the adjunction $(-)\wedge U⊣U\Rightarrow (-)$ computed pointwise-with-restrictions.

10. ($*$) Using [5], formulate the theory of a monoid in a symmetric monoidal multicategory and identify the extra structural rules needed to specialize it to the cartesian theory of monoids of §3.

23.2 Part II

1. Verify in detail that the five sieves on $E$ listed in §16 exhaust the sieves, that the stated graph structure on $\Omega$ is forced by the presheaf action, and that ${\chi }_A$ as defined is a graph morphism.

2. Compute $\Omega$ for the topos of reflexive graphs (add an arrow $e:E\to V$ with $se=te={\mathrm{i}\mathrm{d}}_V$ to the base category—note the direction) and compare: how many truth values do edges have?

3. Determine the truth values of the evolutive-set topos over $(\mathbb{N},\le )$ (§16.8) at each instant, verify the reading of $\neg$ given there, and identify the $\neg \neg$-sheaves.

4. For $G$-sets, show $\Omega =\{0,1\}$ with trivial action, and conclude that $G$–$𝐒𝐞𝐭$ is Boolean; then exhibit the failure of AC for $G=\mathbb{Z}/2$ by finding a non-split equivariant epi.

5. Complete the computation of $Y^X$ for graphs (§16.7) by describing the source and target maps of $Y^X$ explicitly, and verify the exponential adjunction on a small example ($X=Y=$ the single edge).

6. Show that the global points of $\Omega$ in the topos of graphs are exactly $\top$ and $⌀$ (the two loops), so that “external” truth values number two while internal ones number five at edge stage: internal and external logic diverge.

7. Prove monotonicity and local character of the forcing relation directly from the definition in §19.

8. Using the forcing clauses, verify that in the single-edge graph the formula $\forall x,y.(x=y\vee \neg x=y)$ fails at stage $E$, and that its double negation also fails, but that $\neg \neg (x=y\vee \neg x=y)$ holds—as it must, in any topos.

9. ($*$) Following [33], Ch. VI.8, carry out the identification of the Dedekind reals of $\mathrm{S}\mathrm{h}\left(X\right)$ with the sheaf of continuous functions for $X=[0,1]$, at least at the level of the forcing clause for locatedness.

10. ($*$) Read the statement of Barr’s theorem in [23], Part D, and use it to justify the following practice: to prove a geometric sequent in all Grothendieck toposes, it suffices to prove it with classical logic and choice.

A. Summary Tables and Glossary

A.1 Fragments and Structures

A.2 Glossary

Beck–Chevalley condition

Commutation of quantifier-adjoints with pullback functors over pullback squares; the semantic form of “substitution commutes with quantification.”

Classifying category/topos

The structured category representing the models-functor of a theory; carries the universal (generic) model.

Doctrine

A species of structured category serving as the environment for a fragment of logic; formalizable as a 2-monad on $𝐂𝐚𝐭$, among other ways.

Frobenius law

${\exists }_f(U\wedge f^{*}V)={\exists }_{f}U\wedge V$; automatic in the presence of implication.

Generic figure

A representable presheaf; arbitrary presheaves are glueings of generic figures.

Geometric morphism

Adjunction $f^{*}⊣f_{*}$ with left-exact inverse image; the topos-level continuous map.

Kripke–Joyal semantics

The stagewise forcing computation of the internal language; specializes to Kripke and Beth semantics.

Lawvere–Tierney topology

Internal closure operator $j:\Omega \to \Omega$; determines a subtopos of $j$-sheaves.

Mitchell–Bénabou language

The typed higher-order internal language of a topos; formulas are morphisms to $\Omega$.

Natural numbers object

Initial “zero-and-successor” object; the optional axiom of infinity.

Regular category

Finite limits plus pullback-stable image factorizations; the environment for $\exists$.

Sieve

A precomposition-closed set of morphisms into an object; sieves are the truth values in presheaf toposes.

Subobject classifier

$𝗍𝗋𝗎𝖾:1\to \Omega$ representing $Sub$; the object of truth values.

B. Further Exercises

The following exercises track the text; several are adapted from the exercise streams of the sources.⁶⁷

1. (AB) Formulate the notion of a left $G$-set, for a fixed group $G$, as an algebraic theory. What are the models in an arbitrary finite-product category?

2. (AB) Determine what a group is in: ${𝐒𝐞𝐭}_{\mathrm{f}\mathrm{i}\mathrm{n}}$; $𝐓𝐨𝐩$; the category of graphs; and $𝐆𝐫𝐩$ itself. (For the last: show first that two commuting monoid structures with a common unit coincide and are commutative—the Eckmann–Hilton argument—and conclude that groups in $𝐆𝐫𝐩$ are abelian groups.)

3. (AB) Show that the syntactic category ${𝒞}_{𝕋}$ of an algebraic theory has all finite products, and that the universal model $U$ satisfies exactly the provable equations.

4. (AB) Describe the action on morphisms of the universal group $U:{𝐆}^{\mathrm{o}\mathrm{p}}\to 𝐒𝐞𝐭$ of Example 3.9, and verify that terms $s,t$ have equal interpretations $U^n\to U$ iff $s=t$ in the free group on $n$ generators.

5. Prove the two-pullbacks lemma (Lemma 2.1), and deduce that pullback along $g\circ f$ agrees with pullback along $f$ after pullback along $g$ on subobject posets.

6. (AB) Show that a category with finite products and pullbacks of monos along monos has all finite limits, by constructing equalizers from the pullback of $⟨\mathrm{i}\mathrm{d},f⟩$ against $⟨\mathrm{i}\mathrm{d},g⟩$.

7. Verify the six generalized-element rules of §2, and use them to give element-style proofs that meets of subobjects are pullback-stable.

8. Show that in $𝐒𝐞𝐭$, ${\forall }_{f}U=\{b\mid f^{-1}\left(b\right)\subseteq U\}$ is right adjoint to $f^{-1}$, and verify Beck–Chevalley for an explicit non-square pullback of your choosing.

9. Show that $𝐓𝐨𝐩$ is not regular: exhibit a quotient map whose pullback fails to be a quotient map.

10. Prove the modular law of §8.1 in $𝐒𝐞𝐭$ by element chasing, then in a general regular category using stable images.

11. Show that the category of fields has neither a terminal nor an initial object, and locate exactly which steps of Theorem 4.9 fail.

12. (RRZ) In the topos of graphs: compute ${\Omega }^{\mathrm{y}V}$ and ${\Omega }^{\mathrm{y}E}$ explicitly; verify the five-element edge stage of $\Omega$; and check the bi-Heyting inequality $\neg A\le \sim A$ on three subgraphs of the single-edge graph.

13. (RRZ) In evolutive sets ($\mathbb{N}$-sets): verify that the right ideals of $\mathbb{N}$ form the classifier described in Example 16.3, compute $\neg$ on it, and determine for which $k$ the truth value $k$ satisfies $k=\neg \neg k$.

14. Show that in $G$–$𝐒𝐞𝐭$ for nontrivial finite $G$, the object $G$ with left translation has no global points, yet the unique map $G\to 1$ is epi; conclude internal inhabitation without global inhabitation, and reconcile with the Kripke–Joyal $\exists$-clause.

15. Verify the forcing computation for graphs in §19: no jointly epic family of graph maps can decide $x=x_v$ at the edge stage.

16. Prove from the universal property of the NNO that $+$ as defined in §21 is associative and commutative. (Hint: uniqueness of recursion maps.)

17. Work out the Sierpiński-topos truth-value computation: exhibit $Sub\left(1\right)\cong \{⌀,\{o\},X\}$, compute the Heyting implication table, and find a sheaf $B$ and formula witnessing local but not global existence.

18. Show that a Lawvere–Tierney topology $j$ gives a closure operator $U\mapsto \bar{U}$ on each $Sub\left(A\right)$ commuting with pullback, and that $\neg \neg$ satisfies the three axioms.

19. (AB) Derive symmetry and transitivity of equality in the cartesian calculus from the substitution-of-equals rule.

20. Complete the proof sketch of Diaconescu’s theorem (Theorem 21.1) in the internal language, marking exactly where decidable equality of $2$ and the splitting are used.

C. Category-Theoretic Background in One Page

For reference we recall the notions used throughout; any of [4] (Appendix A), [2], or [29] supplies the details at increasing leisure.

Categories, functors, naturality. A category has objects, morphisms, associative composition, identities. A functor preserves all of it. A natural transformation $\vartheta :F\to G$ assigns components ${\vartheta }_A:FA\to GA$ commuting with every $Ff,Gf$. Functor categories ${𝒟}^{𝒞}$ collect functors and natural transformations; presheaves are the case $𝒟=𝐒𝐞𝐭$, ${𝒞}^{\mathrm{o}\mathrm{p}}$ in the exponent.

Yoneda. $\mathrm{y}:𝒞\to \widehat{𝒞}$, $\mathrm{y}c=𝒞(-,c)$, is full and faithful, and $\widehat{𝒞}(\mathrm{y}c,X)\cong X\left(c\right)$ naturally. Consequences used above: representables generate; $\mathrm{y}$ preserves limits; an object is determined by its generalized elements.

Limits and colimits. Products, equalizers, pullbacks; their duals. A category with binary products, a terminal object, and equalizers has all finite limits; a pullback of a mono is a mono. Filtered colimits commute with finite limits in $𝐒𝐞𝐭$.

Adjunctions. $F⊣U$ means $𝒟(FA,B)\cong 𝒞(A,UB)$ naturally; unit $\eta :\mathrm{i}\mathrm{d}\to UF$ and counit $\epsilon :FU\to \mathrm{i}\mathrm{d}$ satisfy the triangle identities. Left adjoints preserve colimits; right adjoints preserve limits. Poset case: Galois connections. Examples on which Part I runs: free $⊣$ forgetful; ${\exists }_f⊣f^{*}⊣{\forall }_f$; $(-)\times A⊣{(-)}^A$; sheafification $⊣$ inclusion.

Monads. An adjunction generates a monad $T=UF$ with unit and multiplication; algebras for $T$ reconstruct (Beck) the “algebraic” part of the adjunction. Finitary monads on $𝐒𝐞𝐭$ = Lawvere theories (Theorem 4.9).

2-categorical language. $𝐂𝐚𝐭$ has categories, functors, and natural transformations; doctrines live here as 2-monads (§12); toposes form 2-categories under either logical functors or geometric morphisms (§20).

D. Background in Detail: Categories, Functors, Adjoints

For self-containedness we collect the background notions used throughout; any introductory text (e.g. the opening chapters of [2], [29], or [32]) covers them fully.

D.1 Categories and Functors

A category $𝒞$ consists of objects, morphisms with assigned domain and codomain, identities, and an associative, unital composition. A functor $F:𝒞\to 𝒟$ assigns objects to objects and morphisms to morphisms preserving all the structure; a natural transformation $\eta :F\Rightarrow G$ assigns to each object $c$ a component ${\eta }_c:Fc\to Gc$ with $Gf\circ {\eta }_c={\eta }_{c\prime }\circ Ff$ for every $f:c\to c\prime$. Functors $𝒞\to 𝒟$ and natural transformations form the functor category ${𝒟}^{𝒞}$. A functor is faithful/full when injective/surjective on each hom-set; an equivalence when full, faithful, and essentially surjective.

D.2 Limits and Colimits

A cone over a diagram $D:𝒥\to 𝒞$ is an object $c$ with compatible morphisms to every $D\left(j\right)$; a limit is a universal cone. Special cases: terminal object ($𝒥$ empty), binary products, equalizers, pullbacks. Colimits are the dual: initial object, coproducts, coequalizers, pushouts. A category with finite products and equalizers has all finite limits; a functor preserves a limit when it sends universal cones to universal cones. Monomorphisms are the morphisms $m$ with $mx=my\Rightarrow x=y$; equivalently, such that $$\begin{array}{ccc}\hfill A\hfill & \hfill \stackrel{\mathrm{i}\mathrm{d}}{\to }\hfill & \hfill A\hfill \\ \hfill \downarrow \mathrm{i}\mathrm{d}\hfill & \hfill \hfill & \hfill \downarrow m\hfill \\ \hfill A\hfill & \hfill \stackrel{m}{\to }\hfill & \hfill B\hfill \end{array}$$ is a pullback. Epimorphisms are dual; regular epi/mono means “a coequalizer/equalizer of some pair.”

D.3 Adjunctions

An adjunction $F⊣G$ between $F:𝒞\to 𝒟$ and $G:𝒟\to 𝒞$ is a natural bijection $𝒟(Fc,d)\cong 𝒞(c,Gd)$; equivalently unit and counit $\eta :\mathrm{I}\mathrm{d}\Rightarrow GF$, $ϵ:FG\Rightarrow \mathrm{I}\mathrm{d}$ satisfying the triangle identities. Left adjoints preserve colimits; right adjoints preserve limits. Between posets, an adjunction is a Galois connection, the form in which most of Part I’s logic lives. Examples used in the text: free $⊣$ forgetful (free groups, free models of any algebraic theory); $(-)\times A⊣{(-)}^A$ (exponentials, currying); ${\exists }_f⊣f^{*}⊣{\forall }_f$ (quantifiers); sheafification $⊣$ inclusion; $f^{*}⊣f_{*}$ (geometric morphisms).

D.4 Yoneda

For a small category $𝒞$, the Yoneda embedding $\mathrm{y}:𝒞\to \widehat{𝒞}={𝐒𝐞𝐭}^{{𝒞}^{\mathrm{o}\mathrm{p}}}$ sends $c$ to $𝒞(-,c)$. The Yoneda lemma states $\widehat{𝒞}(\mathrm{y}c,X)\cong X\left(c\right)$ naturally; consequences used above: $\mathrm{y}$ is full and faithful; it preserves all limits that exist; every presheaf is a colimit of representables; and universal properties determine objects up to isomorphism. The completeness proofs of §3, the generic figures of §16, and the classifier of §17 all rest on it.

1. J. L. Bell, 2005. The development of categorical logic. In Handbook of Philosophical Logic. doi:10.1007/1-4020-3092-4.

2. S. Abramsky and N. Tzevelekos, 2011. Introduction to categories and categorical logic. doi:10.1007/978-3-642-12821-9_1; arXiv:1102.1313.

3. V. de Paiva and A. Rodin, 2013. Elements of categorical logic: Fifty years later. doi:10.1007/s11787-013-0086-9.

4. S. Awodey and A. Bauer, 2019. Introduction to Categorical Logic. Lecture notes. https://awodey.github.io/catlog/.

5. M. Shulman, 2016. Categorical Logic from a Categorical Point of View. Lecture notes. https://mikeshulman.github.io/catlog/catlog.pdf.

6. A. Kock and G. E. Reyes, 1977. Doctrines in categorical logic. In Handbook of Mathematical Logic. doi:10.1016/S0049-237X(08)71104-2.

7. G. M. Kelly and R. Street, 1974. Review of the elements of 2-categories (Sec. 3: Monads in a 2-category). doi:10.1007/BFb0063101.

8. F. Paugam, 2014. Towards the Mathematics of Quantum Field Theory, Sec. 2.1: Higher categories, doctrines, and theories. Springer.

9. F. Dagnino and G. Rosolini, 2021. Doctrines, modalities and comonads. arXiv:2107.14031.

10. M. Makkai, 1997. Generalized sketches as a framework for completeness theorems, Parts I–III. doi:10.1016/S0022-4049(96)00007-2; doi:10.1016/S0022-4049(96)00008-4; doi:10.1016/S0022-4049(96)00009-6.

11. S. Fujii, 2019. A unified framework for notions of algebraic theory. Theory and Applications of Categories. arXiv:1904.08541.

12. J. van Oosten, 1995. Basic Category Theory, Sec. 4.2: The logic of regular categories. Lecture notes. https://www.staff.science.uu.nl/~ooste110/syllabi/catsmoeder.pdf.

13. C. Butz, 1998. Regular categories and regular logic. BRICS Lecture Series LS-98-2. https://www.brics.dk/LS/98/2/BRICS-LS-98-2.pdf.

14. M. Gran, 2021. An introduction to regular categories. doi:10.1007/978-3-030-84319-9_4; arXiv:2004.08964.

15. F. Borceux, 1994. Handbook of Categorical Algebra, Vol. 2, Ch. 2: Regular categories. Cambridge University Press.

16. G. E. Reyes, 1977. Sheaves and Concepts: A Model-Theoretic Interpretation of Grothendieck Topoi, Ch. II: Coherent logic. Cahiers de topologie et géométrie différentielle. https://www.numdam.org/article/CTGDC_1977__18_2_105_0.pdf.

17. M. Bezem, 2005. On the undecidability of coherent logic. doi:10.1007/11601548_2.

18. M. Bezem and T. Coquand, 2005. Automating coherent logic. doi:10.1007/11591191_18.

19. S. Stojanović et al., 2010. A coherent logic based geometry theorem prover capable of producing formal and readable proofs. doi:10.1007/978-3-642-25070-5_12.

20. S. Stojanović et al., 2014. A vernacular for coherent logic. doi:10.1007/978-3-319-08434-3_28; arXiv:1405.3391.

21. J. Avigad et al., 2009. A formal system for Euclid’s Elements. doi:10.1017/S1755020309990098; arXiv:0810.4315.

22. M. Ganesalingam and W. T. Gowers, 2013. A fully automatic problem solver with human-style output. Preprint; a revised version appeared as “A fully automatic theorem prover with human-style output,” J. Automated Reasoning 58(2):253–291, 2017. arXiv:1309.4501.

23. P. T. Johnstone, 2002. Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press.

24. P. T. Johnstone, 1977. Topos Theory. Academic Press.

25. J. Baez, 2021. Topos theory in a nutshell. https://math.ucr.edu/home/baez/topos.html.

26. J. Baez, 2020. Lecture notes on topos theory, Parts 1–8. Azimuth blog. https://johncarlosbaez.wordpress.com/2020/01/05/topos-theory-part-1/.

27. I. Blechschmidt, 2022. Exploring mathematical objects from custom-tailored mathematical universes. doi:10.1007/978-3-030-84706-7_4; arXiv:2204.00948.

28. R. P. Kostecki, 2011. An introduction to topos theory. Lecture notes. https://web.archive.org/web/20220823182043/https://www.fuw.edu.pl/~kostecki/ittt.pdf.

29. F. W. Lawvere and S. H. Schanuel, 2009. Conceptual Mathematics, 2nd ed. Cambridge University Press. doi:10.1017/CBO9780511804199.

30. M. La Palme Reyes, G. E. Reyes, and H. Zolfaghari, 2004. Generic Figures and Their Glueings: A Constructive Approach to Functor Categories. Polimetrica, Monza. https://marieetgonzalo.files.wordpress.com/2004/06/generic-figures.pdf.

31. M. La Palme Reyes et al., 1994. The non-boolean logic of natural language negation. Philosophia Mathematica. doi:10.1093/philmat/2.1.45.

32. R. Goldblatt, 1984. Topoi: The Categorial Analysis of Logic. North-Holland. https://projecteuclid.org/euclid.bia/1403013939.

33. S. Mac Lane and I. Moerdijk, 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer. doi:10.1007/978-1-4612-0927-0.