README⤓ .txt 2026-07-17T121634.146 000000000000792 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-07-15T065155.000 000000000015008 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-07-15T063450.000 000000000018760 Plotkin and Power introduced algebraic effects (2001-2003). Pretnar developed handlers (2010). Effects as operations with equations. Handlers as interpreters for effects. Foundation for effect systems in programming languages.
Artin Gluing⤓ .md 2026-07-16T004442.000 000000000035304 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-07-15T054120.000 000000000031128 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.
Coalgebraic Logic⤓ .md 2026-07-17T120407.600 000000000000872 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-07-15T235628.000 000000000020592 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. Decidable fragment with good computational properties.
Cubical Type Theory⤓ .md 2026-07-15T064236.000 000000000016296 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-07-15T065148.000 000000000014544 Scott and Strachey (1970s). Mathematical meaning of programs. Domains as semantic spaces. Compositionality: meaning from parts. Foundation for language semantics.
Dialectica Categories⤓ .md 2026-07-17T120407.600 000000000000904 de Paiva (1987), based on Gödel's Dialectica. Categorical models. Linear logic semantics. Interaction structure. Foundational semantics.
Dialectica Interpretation⤓ .md 2026-07-15T064727.000 000000000014112 Gödel (1958) for consistency of arithmetic. Interprets formulas as games between ∃ and ∀. Extracts computational content. Foundation for proof mining.
Domain Theory⤓ .md 2026-07-15T060302.000 000000000023312 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-07-16T004442.000 000000000034680 F. William Lawvere, "An elementary theory of the category of sets" (PNAS, 1964), written two years 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-07-17T120407.600 000000000000816 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-07-15T060049.000 000000000020760 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-07-16T001736.000 000000000034408 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-07-17T120407.600 000000000000872 Bénabou (bicategories, 1967), Baez-Dolan, Lurie. n-categories. Weak structures. Homotopy types. Foundation of higher structures.
Homotopy Type Theory⤓ .md 2026-07-15T063639.000 000000000018360 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-07-17T120407.600 000000000000848 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-07-15T064539.000 000000000015952 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-07-16T004643.000 000000000035304 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 (1993) the categorical semantics. Hyland and de Paiva's FILL (1993) is the full-intuitionistic variant.
Lawvere Theories⤓ .md 2026-07-15T071430.000 000000000014200 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-07-15T064545.000 000000000015728 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-07-15T063259.000 000000000017992 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-07-15T065308.000 000000000014872 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-07-17T120407.600 000000000000888 Gambino, Kock (2010s). Containers/species. Type theory connection. Data type semantics. Dependent polynomial functors.
Realizability⤓ .md 2026-07-15T055807.000 000000000022232 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-07-17T121634.146 000000000000856 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-07-15T060040.000 000000000022824 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-07-17T120407.600 000000000000832 Grothendieck (1960s geometry), Lawvere-Tierney (1970s logic). Categories like Set. Internal logic. Sheaves. Foundation of categorical logic.
Univalent Foundations⤓ .md 2026-07-17T120407.600 000000000000904 Vladimir Voevodsky (2006+). Homotopy type theory. Univalence axiom. Synthetic homotopy. Foundation of mathematics.
Yoneda Lemma⤓ .md 2026-07-17T120407.600 000000000000832 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-17T120407.600 000000000000808 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).