README⤓ .txt 2026-10-22T090724.000 000000000012448 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.
Adjunctions⤓ .md 2026-10-22T084838.000 000000000039840 Kan (1958). Fundamental concept of category theory. F ⊣ G: left adjoint to right. Universal property characterization. Unifies constructions across mathematics. Foundation for categorical logic.
Algebraic Effects⤓ .md 2026-08-20T010456.000 000000000043288 Plotkin and Power introduced algebraic effects across a sequence of papers (2001–2003): effects arise as operations generating a free algebra, and the monad is determined by the operations and their equations rather than assumed. Handlers are Plotkin and Pretnar, "Handlers of Algebraic Effects" (ESOP 2009) — joint work, not Pretnar's alone; Pretnar's thesis (2010) and the Eff language with Bauer are the follow-on. Effects as operations with equations. Handlers as interpreters for effects. Foundation for effect systems in programming languages.
Artin Gluing⤓ .md 2026-08-20T081215.000 000000000053280 The gluing construction is Artin's, from SGA4 (1972), where it assembles a topos from an open and its closed complement. Peter Freyd, "Aspects of topoi" (1972), used it to prove the disjunction and existence properties for intuitionistic logic categorically. Lambek and Scott's Introduction to Higher Order Categorical Logic (1986) is where the logical technique was systematized; Taylor's Practical Foundations (1999) and Streicher's later work extend it to type theory.
Categorical Logic⤓ .md 2026-10-22T180154.561 000000000000872 F. William Lawvere pioneered categorical logic (1960s), showing logical systems correspond to categorical structures. The topos concept (Grothendieck for algebraic geometry, Lawvere-Tierney for logic) provides a universe for mathematics beyond sets. Unifies logic, type theory, and geometry. Foundational for Homotopy Type Theory.
Chu Spaces⤓ .md 2026-10-22T224238.000 000000000074888 Po-Hsiang Chu, "Constructing -autonomous categories", the appendix (103–138) to Michael Barr, -Autonomous Categories (Lecture Notes in Mathematics 752, Springer 1979), written up from Chu's master's thesis under Barr; Barr returned to the construction as a semantics for linear logic (1991). Lafont and Streicher, "Games semantics for linear logic" (LICS 1991, 43–50), treated the case over Set, reading the spaces as games. Vaughan Pratt made them a program: "Chu spaces: automata with quantum aspects" (PhysComp '94, IEEE 1994, 186–195), "The Stone gamut: a coordinatization of mathematics" (LICS 1995, 444–454), "Chu spaces from the representational viewpoint" (Annals of Pure and Applied Logic 96, 1999, 319–333). Barwise and Seligman, Information Flow: The Logic of Distributed Systems (Cambridge Tracts in Theoretical Computer Science 44, Cambridge University Press 1997), built the logic of distributed systems on the same objects under the name classifications.
Coalgebraic Logic⤓ .md 2026-08-20T013045.000 000000000050984 Coalgebra as a general theory of state-based systems: Aczel (non-well-founded sets, 1988), Rutten (universal coalgebra, 2000). Coalgebraic modal logic: Moss (1999), Pattinson, Kupke, Cîrstea. The uniform framework in which transition systems, automata, streams, and probabilistic systems are all coalgebras, and modal logics are their specification languages.
Coherent Logic⤓ .md 2026-10-22T092920.000 000000000050264 Emerged from the Grothendieck school's topos theory (SGA4, 1972); Makkai and Reyes, First Order Categorical Logic (1977), gave the model theory; Johnstone's Sketches of an Elephant (2002) is the reference. Bezem and Coquand (2005) revived it for automated theorem proving. Part of the geometric/coherent hierarchy from categorical logic. Formulas: atoms, ∧, ∨ (finite), ∃, ⊤, ⊥. No → or ∀ except in sequents. Preserved by inverse images of geometric morphisms. Semi-decidable, not decidable — see below.
Cubical Type Theory⤓ .md 2026-08-20T014418.000 000000000038352 Cohen, Coquand, Huber, Mörtberg (2015-2018). Computational interpretation of univalence. Paths as functions from interval. Kan operations for composition. Implemented in Cubical Agda.
Denotational Semantics⤓ .md 2026-10-22T165042.936 000000000000928 Scott and Strachey (1970s). Mathematical meaning of programs. Domains as semantic spaces. Compositionality: meaning from parts. Foundation for language semantics.
Dialectica Categories⤓ .md 2026-10-22T180154.561 000000000000904 de Paiva (1987), based on Gödel's Dialectica. Categorical models. Linear logic semantics. Interaction structure.
Dialectica Interpretation⤓ .md 2026-10-22T090631.000 000000000056480 Gödel, "Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes", published in the journal Dialectica in 1958, from which the interpretation takes its name. The paper was written to extend Hilbert's finitary standpoint far enough to give a consistency proof for arithmetic, replacing quantification over infinite domains by computable functionals of finite type. Diller and Nahm (1974) gave the bounded variant that avoids deciding the matrix; Shoenfield (1967) recast the interpretation for classical arithmetic directly; Kohlenbach's monotone functional interpretation (1996) turned it into the working tool of proof mining.
Domain Theory⤓ .md 2026-10-22T090413.000 000000000046272 Dana Scott introduced domains (1969-70) to give semantics to the lambda calculus. Solves: D ≅ D → D (types isomorphic to their function space). Continuous lattices and dcpos provide mathematical foundation. Scott and Strachey developed denotational semantics. Foundational for programming language semantics.
ETCS⤓ .md 2026-10-22T090034.000 000000000045856 F. William Lawvere, "An elementary theory of the category of sets" (PNAS, 1964), written the year after his thesis and rejected by referees who could not see that it was a set theory. Lawvere and Rosebrugh's Sets for Mathematics (2003) is the textbook; Tom Leinster's "Rethinking set theory" (2014) is the readable case for it. The structural alternative to the cumulative hierarchy.
Fibrations⤓ .md 2026-08-20T022448.000 000000000037576 Grothendieck (SGA1, 1961); Bénabou systematized the theory (1985). Also called fibered categories. Indexed categories via fibered categories. Dependent types categorically. Foundation for categorical type theory.
Geometric Logic⤓ .md 2026-08-20T022541.000 000000000049096 Emerged from topos theory and categorical logic (1970s). Formulas preserved by geometric morphisms (topos maps). Characterizes constructively well-behaved theories. Important in algebraic geometry and classifying toposes. Related to regular and coherent logic.
Geometry of Interaction⤓ .md 2026-08-20T023021.000 000000000049440 Jean-Yves Girard, "Geometry of interaction I: interpretation of System F" (1989), and the sequence through GoI V (1989–2011). Danos and Regnier's "Local and asynchronous beta-reduction" (1993, 1995) gave the path-algebra reading; Abramsky, Haghverdi, and Scott's "Geometry of interaction and linear combinatory algebras" (2002) gave the categorical axiomatization; Mackie's The Geometry of Interaction Machine (1995) built a compiler from it.
Higher Categories⤓ .md 2026-08-20T023208.000 000000000051640 Bénabou, "Introduction to bicategories" (1967), gave the first systematic weak higher structure. Grothendieck's Pursuing Stacks (1983) posed the two organizing problems: define weak n-categories, and prove the homotopy hypothesis identifying ∞-groupoids with homotopy types. Boardman and Vogt's weak Kan complexes (1973) were rediscovered as quasicategories by Joyal (2002); Baez and Dolan, "Higher-dimensional algebra and topological quantum field theory" (1995), gave both a definition of weak n-category and the cobordism hypothesis. Lurie's Higher Topos Theory (2009) made (∞,1)-category theory a working tool.
Homotopy Type Theory⤓ .md 2026-08-20T023838.000 000000000041032 Voevodsky, Awodey, Warren (2006-2012). Univalent Foundations program. Identity types as paths. Types as spaces. Univalence: equivalent types are equal. Foundation connecting type theory and homotopy theory.
Hyperdoctrines⤓ .md 2026-08-20T023759.000 000000000038864 Lawvere (1969), who called the general pattern a doctrine. Categorical semantics for predicate logic. Indexed categories for substitution. Adjoints for quantifiers. Foundation for categorical logic.
Internal Logic⤓ .md 2026-08-20T082130.000 000000000045664 Lawvere, Kock, and others (1960s-1970s). Logic interpreted inside a category. Subobject classifier replaces truth values. Intuitionistic in general topoi. Foundation for categorical proof theory.
Intuitionistic Linear Logic⤓ .md 2026-10-22T092734.000 000000000049304 Implicit in Girard (1987) as the intuitionistic fragment; Girard and Lafont, "Linear logic and lazy computation" (1987), gave the first term calculus; Benton, Bierman, de Paiva, and Hyland, "A term calculus for intuitionistic linear logic" (1993), gave the one that stuck, and Bierman's thesis (1994) the categorical semantics. Hyland and de Paiva's FILL (1993) is the full-intuitionistic variant.
Lawvere Theories⤓ .md 2026-08-20T024722.000 000000000036632 Lawvere (1963). Categorical universal algebra. Theories as categories with products. Algebras as product-preserving functors. Foundation for algebraic theories.
Locally Cartesian Closed Categories⤓ .md 2026-08-20T024818.000 000000000044488 Seely (1984) connected LCCCs to dependent type theory. Each slice category is cartesian closed. Models dependent products and sums. Foundation for MLTT semantics.
Ludics⤓ .md 2026-10-22T090048.000 000000000039240 Girard introduced ludics (2001). Foundation for logic via interactive games. Designs as basic objects, not formulas. Orthogonality defines behavior/type. Unifies logic, computation, and game semantics. "Logic from interaction."
Monads⤓ .md 2026-08-20T025338.000 000000000048952 Godement (1958), Eilenberg-Moore (1965). Endofunctor with unit and multiplication. Encapsulates computational effects. Kleisli category for sequencing. Foundation for effectful programming.
Polynomial Functors⤓ .md 2026-10-22T085419.000 000000000050600 Joyal's analytic functors and combinatorial species (1981) are the ancestor. Abbott, Altenkirch and Ghani, "Containers: constructing strictly positive types" (2005), gave the type-theoretic form; Gambino and Hyland, "Wellfounded trees and dependent polynomial functors" (2004), the dependent one over a locally cartesian closed base; Gambino and Kock, "Polynomial functors and polynomial monads" (2013), the general theory. Moerdijk and Palmgren connected the initial algebras to Martin-Löf's W-types.
Realizability⤓ .md 2026-10-22T092654.000 000000000061896 Kleene introduced realizability (1945) to interpret intuitionistic logic via computable functions. A formula is true if "realized" by a computation. Connects constructive logic to computability theory. Extended by Kreisel, Troelstra, and others. Foundation for program extraction from proofs.
Sheaf Semantics⤓ .md 2026-10-22T090413.000 000000000053960 Grothendieck's sites and sheaves (SGA4, 1963–64, published 1972) supplied the machinery; Lawvere and Tierney's elementary topos (1970) made it logic. Kripke–Joyal forcing is Joyal's reformulation of Kripke's semantics inside a topos; Fourman and Scott, "Sheaves and logic" (1979), and Fourman and Hyland's sheaf models of intuitionistic analysis (1979) are where the model theory was built. Van Dalen and Troelstra's Constructivism in Mathematics (1988) is the standard exposition.
Topos Logic⤓ .md 2026-10-22T165042.936 000000000000824 Lawvere and Tierney developed topos theory (1960s-70s). Toposes generalize both sets and sheaves. Internal logic of a topos is intuitionistic. Provides categorical semantics for higher-order intuitionistic logic. Unifies algebraic geometry, logic, and category theory.
Topos Theory⤓ .md 2026-08-20T110105.000 000000000051312 Grothendieck and the SGA4 seminar (1963–64) introduced sheaf toposes as generalized spaces for étale cohomology. Lawvere and Tierney (1970) axiomatized the elementary topos, dropping the site and keeping the subobject classifier, which turned a tool of geometry into a setting for logic. Lawvere's ETCS (1964) had already proposed a category of sets as a foundation. Lambek and Scott (1986) established the correspondence with higher-order intuitionistic type theory.
Univalent Foundations⤓ .md 2026-08-20T033039.000 000000000052040 Vladimir Voevodsky proposed the programme from about 2005, first in circulation as "A very short note on homotopy λ-calculus" (2006), and named it univalent foundations. The precedents are Hofmann and Streicher's groupoid model (1998) and Awodey and Warren's homotopy-theoretic reading of identity types (2009). Voevodsky's own contributions are the definition of h-levels, the univalence axiom, the simplicial set model, and the Coq library Foundations (2010), continued as UniMath. The special year at the Institute for Advanced Study (2012–13) produced Homotopy Type Theory: Univalent Foundations of Mathematics (2013).
Yoneda Lemma⤓ .md 2026-08-20T032826.000 000000000042328 Nobuo Yoneda (1954), via correspondence reported by Saunders Mac Lane. The central lemma of category theory: an object is determined, up to isomorphism, by the pattern of maps into (or out of) it. Underlies representability, universal properties, and categorical semantics of logic.
CRITERIA⤓ .txt 2026-07-16T002328.000 000000000010144 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).