INCLUSION CRITERIA
An entry belongs in this subdivision if and only if it formulates a logic, its semantics, or its proof theory in category-theoretic terms, so that logical structure is carried by objects, morphisms, functors, and universal properties.
Required: At least one of the following:
- A categorical semantics for a logic or type theory (topos, hyperdoctrine, fibration, CCC/LCCC)
- An internal-language correspondence between a logic and a class of categories
- A categorical account of proofs, connectives, or effects (monads, adjunctions, Dialectica, ludics)
- A construction of category theory that the collection's categorical semantics rest on (Yoneda, fibrations, higher structures, polynomial functors), entered for its role in those semantics rather than for itself
Not sufficient: A logic merely admitting a categorical model without the category theory as its subject. Set-theoretic model theory (Model-Theory). Syntactic proof calculi (Proof-Systems).
Boundary: Homotopy and cubical type theory are cross-listed with Type/Dependent and Algebraic/Heyting. Denotational semantics and domain theory are cross-listed with Applications/Computation. The categorical formulation lives here; the syntax and its uses live in the paired subdivisions.