CATEGORICAL LOGIC
Logics formulated or given semantics inside category theory: systems whose connectives, quantifiers, and proofs are read as universal constructions, functors, and natural transformations. The organizing insight is that a logic is the internal language of a class of categories, and a class of categories is a semantics for a logic.
Entries treat the general machinery (categorical logic, internal logic, the Yoneda lemma, fibrations and fibered categories, hyperdoctrines, doctrines, Lawvere theories, adjunctions, monads), the topos-theoretic strand (topos theory and logic, geometric and coherent logic, locally cartesian closed categories), the higher-categorical and homotopical strand (higher categories, homotopy and cubical type theory), and the denotational and resource strands (domain and denotational semantics, Dialectica categories, polynomial functors, algebraic effects, ludics, coalgebraic logic cross-listed with Applications/Computation).
The subdivision holds two kinds of entry, and the second is an exception the criteria state rather than hide. Most entries are categorical formulations of a logic or its semantics. A minority—Yoneda, adjunctions, monads, fibrations—are constructions of category theory rather than logics, and they are here because the semantics cannot be stated without them. They are admitted for that role and not for themselves, which is why the exception is bounded: a construction earns a place by carrying logical structure somewhere in this collection, not by being category theory.