nLab 2-categorical logic

Idea

Where

• categorical logic is formal logic/type theory regarded as the internal logic/internal language of categories, notably of categories well-suited for this purposes, such as elementary toposes,

so

• 2-categorical logic, or 2-logic for short, as understood in this entry here, is (or should be, once developed) the categorification of this situation, namely the study of the internal logic/language of two-dimensional categories (understood in the generality including 2-categories, bicategories, double categories, virtual double categories, etc.), and notably of two-dimensional categories well-suited for this purpose, such as those one will want to call elementary 2-toposes.

Therefore, the step from formal logic/categorical logic to formal 2-logic/2-categorical logic is analogous to the step from the former to homotopy type theory, where one instead considers the internal language of $(\infty,1)$-categories.

This means that 2-logic is a genuine extension of ordinary logic with new logical constructions and phenomena (largely still to be isolated properly) — analogous to how homotopy type theory enhances ordinary logical types to homotopy types, so 2-logic will be speaking about “1-types” of sorts (meaning: $(1,1)$-types also known as small categories, as opposed to the more restrictive homotopy $(1,0)$-types also known as groupoids, both generalizing the 0-types also known as sets).

For example:

• where subobject classifiers in ordinary elementary toposes serve as universes of propositions for their first order internal logic,

• where object classifiers in $(\infty,1)$-toposes serve as type universes for their homotopy internal logic,

• so 2-toposes have fibration classifiers which should serve as universes of “2-types” for their internal 2-logic.

  Accordingly, powersets in ordinary logic/set theory become categories of presheaves in 2-logic, and the Cantor embedding becomes the Yoneda embedding, etc.

In fact, there should be a joint generalization and unification of 2-logic of “2-types” with the “$(\infty,1)$-logic” of homotopy types, namely given by the internal language of $(\infty,2)$-categories (notably of $(\infty,2)$-toposes): This $(\infty,2)$-logic is currently being developed under the name directed homotopy type theory and as such, even if itself nascent, may be the most developed form of syntactic 2-logic that has found attention so far.

This means that 2-logic in the sense of this page here is not about the related but different idea of using general tools from 2-category theory in the study of ordinary 1-categorical logic, hence is not along the lines of how formal category theory uses 2-category theory to study 1-categories.

Of course, there may be relation and overlap between 2-logic proper and such “formal categorical logic” using 2-categorical methods in 1-logic. With genuine 2-logic not being developed much at all at this point, most of the references listed below actually fall on the side of 2-categorical methods in 1-logic.

For instance, for a suitable 2-dimensional sketch-like object its 2-category of models in Cat is a category of 1-theories: coherent categories, regular categories, lex categories. Thus, on one side we have the study of 2-sketch like objects, of 2-monads on Cat and Lex, and on 2-functorial semantics. This is the adagio that 2-theories are logics. On the other we have the study of 2-categories of (1)-theories, i.e. the idea that 2-models are 1-theories.

Related concepts

• type theory, logic

• 2-type theory

• (∞,1)-type theory, (∞,1)-logic

References

An early explicit logic for a class of structured 2-categories (namely lax cartesian closed 2-categories) may be found in:

• R. A. G. Seely: Modelling Computations: a 2-categorical Framework, Proceedings of LICS 1987 (1987) 65-71 [pdf, lics.siglog]

Remarks on geometric 2-logic:

• John Bourke, Richard Garner, Remks. 42 & 47 in: Two-dimensional regularity and exactness, Journal of Pure and Applied Algebra, 218 7 (2014) 1346–1371 [doi:10.1016/j.jpaa.2013.11.021, arXiv:1304.5275]

On further aspects of elementary 2-topoi:

• Mark Weber: Yoneda structures from 2-toposes, Appl Categor Struct 15 (2007) 259–323 [doi:10.1007/s10485-007-9079-2, pdf]

  (introduces a notion of elementary 2-topos but explicitly disregards discussion of logical aspects)

• Steve Awodey, Jacopo Emmenegger, Toward the effective 2-topos (2025) [arXiv:2503.24279]

  (a 2-dimensional version of the effective topos)

Specifically on higher classifiers (higher analogs of what is the subobject classifier in ordinary elementary toposes):

• Luca Mesiti: Pointwise Kan extensions along 2-fibrations and the 2-category of elements, Theory and Applications of Categories 41 30 960–994 (2024) [arXiv:2302.04566, doi:10.70930/tac/b9u5z003]

  (via a 2-Grothendieck construction)

• Elena Caviglia, Luca Mesiti, Indexed Grothendieck construction, Theory and Applications of Categories 41 28 (2024) 894–926 [arXiv:2307.16076, doi:10.70930/tac/xzio144a]

  (via the indexed Grothendieck construction)

• Luca Mesiti, 2-classifiers via dense generators and Hofmann-Streicher universe in stacks, Canadian Journal of Mathematics (2025) 1–52 [arXiv:2401.16900, doi:10.4153/S0008414X24000865]

• Calum Hughes, Adrian Miranda: The elementary theory of the 2-category of small categories, Theory and Applications of Categories 43 8 (2025) 196–242 [arXiv:2403.03647, doi:10.70930/tac/c97jx7g2]

  (via ET2CC)

On 2-functorial semantics:

• John Power: Why tricategories?, Information and Computation 120 2 (1995) 251–262 [doi:10.1006/inco.1995.1112]

  (in a context of tricategories)

• John Power: Enriched Lawvere theories, Theory and Applications of Categories 6 7 (1999) 83–93 [tac:6-07, doi:10.70930/tac/soye1d6v]

• John Power: Categories with algebraic structure, International Workshop on Computer Science Logic, Springer (1997) 389–405 [doi:10.1007/BFb0028027]

• Renato Betti, Marco Grandis, Complete theories in 2-categories, Cahiers 29 1 (1988) 9–57 [numdam:CTGDC_1988__29_1_9_0]

• Nathanael Arkor, John Bourke, Joanna Ko, Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation [arXiv:2412.07475]

• Ivan Di Liberti, Axel Osmond: Bi-accessible and bipresentable 2-categories, Applied Categorical Structures 33 3 (2025) [arXiv:2203.07046, doi:10.1007/s10485-024-09794-9]

  (not on 2-logic but on locally presentable 2-categories)

On 2-categories as 2-theories:

• Richard Garner: Two-dimensional models of type theory, Mathematical Structures in Computer Science 19 4 (2009) 687-736 [doi:10.1017/S0960129509007646, pdf]

• Greta Coraglia, Ivan Di Liberti: Context, judgement, deduction (2021) [arXiv:2111.09438]

• Benedikt Ahrens, Paige Randall North, Niels van der Weide: Semantics for two-dimensional type theory, LICS ‘22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, 12 (2022) 1–14, [doi:10.1145/3531130.3533334]

• Vít Jelínek: Type theory and its semantics, Master thesis, Masaryk University (2024) [is.muni.cz:th/fl75q/]

• Jonathan Osser: A 2‑Sketchy Approach to Type Theory, Master thesis, University of Amsterdam (2025) [scripties:56899]

On rewriting:

• John Power: An abstract formulation for rewrite systems, In Category Theory and Computer Science, Springer Berlin Heidelberg (1989) 300–312 [doi:10.1007/BFb0018358]

• Tom Hirschowitz: Cartesian closed 2-categories and permutation equivalence in higher-order rewriting, Logical Methods in Computer Science 9 3 (2013) pp.10 [pdf, arXiv:1307.6318, doi:10.2168/LMCS-9(3:10)2013]

• Samuel Mimram, Categorical Coherence from Term Rewriting Systems, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Leibniz International Proceedings in Informatics (LIPIcs) 260 (2023) 16:1–16:17 [doi:10.4230/LIPIcs.FSCD.2023.16]

• Samuel Mimram: Rewriting techniques for relative coherence, Logical Methods in Computer Science 21 3 (2025) [arXiv:2402.18170, doi:10.46298/lmcs-21(3:7)20252025)]

On 2-categories of 1-theories:

• Richard Garner, Stephen Lack: Lex colimits, Journal of Pure and Applied Algebra 216 6 (2012) 1372–1396 [arXiv:1107.0778, doi:10.1016/j.jpaa.2012.01.003]

• Ivan Di Liberti, Gabriele Lobbia: Sketches and Classifying Logoi (2024) [arXiv:2403.09264]

• Greta Coraglia, Jacopo Emmenegger, A 2-categorical analysis of context comprehension, Theory and Applications of Categories 41 42 (2024) 1476–1512 [arXiv:2403.03085, doi:10.70930/tac/dcvkbg9f]

• Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North: Comparing semantic frameworks for dependently-sorted algebraic theories, Asian Symposium on Programming Languages and Systems (APLAS 2024), Lect. Notes Comp. Sci. 15194 (2024) 3–22 [arXiv:2412.19946, doi:10.1007/978-981-97-8943-6_1]

• Greta Coraglia, Jacopo Emmenegger: Categorical models of subtyping, 29th International Conference on Types for Proofs and Programs (TYPES 2023), Leibniz International Proceedings in Informatics (LIPIcs) 303 (2024) 3:1–3:19 [arXiv:2312.14600, doi:10.4230/LIPIcs.TYPES.2023.3]

• Ivan Di Liberti, Lingyuan Ye: Logics and concepts in the 2-category of Topoi (2025) [arXiv:2504.16690]

On (∞,2)-topoi:

• Fernando Abellán, Louis Martini: $(\infty,2)$-Topoi and descent [arXiv:2410.02014]

On directed type theory and ends and coends as directed quantifiers:

• Andrea Laretto, Fosco Loregian, Niccolò Veltri, Directed equality with dinaturality [arXiv:2409.10237]

A treatment of doctrines in terms of double categories:

• Michael Lambert, Evan Patterson, Cartesian double theories: A double-categorical framework for categorical doctrines [arXiv:2310.05384]

Notes on assorted topics related to 2-categorical logic:

• Mike Shulman: 2-categorical logic (Unfinished notes, 2009)

  (also includes exposition of other aspects of 2-logic, such as exactness and Grothendieck 2-topoi).