Michael Shulman
2-categorical logic

With acknowledgements to David Corfield and others, this project is grandiosely entitled

The internal logic of a 2-topos

However, probably not all the hopes that might be aroused by such a title will be fulfilled. See the introduction for caveats.


  1. Introduction:

  2. What is a 2-topos?

  3. On the meaning of “categorified logic

  4. Conventions on terminology and the meaning of nn-category

  5. The role of the axiom of choice

  6. First-order structure. This stuff is not really original; I learned about it from StreetCBS but versions of it appear elsewhere too, e.g. the work of Mathieu Dupont.

  7. slice 2-categories and fibrational slices

  8. 2-Congruences

  9. Regular 2-categories

  10. Classification of congruences

  11. Exact 2-categories

  12. Poly-congruences

  13. Coherent 2-categories

  14. Extensive 2-categories

  15. 2-pretoposes

  16. Heyting 2-categories

  17. Additional levels of structure

  18. Cores and enough groupoids

  19. Natural numbers objects in 2-categories

  20. exponentials in a 2-category

  21. Duality involutions

  22. Grothendieck 2-toposes (also due to StreetCBS, see also the work of Igor Bakovic)

  23. 2-sheaves (stacks) on a 2-site

  24. The 2-Giraud theorem

  25. Truncated 2-toposes

  26. Geometric morphisms between 2-toposes

  27. Truncation and factorization systems

  28. Truncation

  29. The comprehensive factorization system

  30. full morphisms and the (eso+full, faithful) factorization system

  31. The Cauchy factorization system

  32. Aspects of first-order structure

  33. colimits in an n-pretopos

  34. balancedness in n-pretoposes

  35. Regular and exact completions

  36. 3-sheaf conditions?

  37. The axiom of 2-choice

  38. First-order and geometric logic in a 2-category

  39. internal logic of a 2-category

  40. the functor comprehension principle, and the description of faithful, ff, eso morphisms in the internal logic

  41. adjunctions in 2-logic

  42. Kripke-Joyal semantics in a 2-category?

  43. category theory in a 2-pretopos?

  44. syntactic 2-categories?

  45. classifying 2-toposes?

  46. Classifying objects

  47. classifying discrete opfibrations

  48. classifying cosieves

  49. size structures

  50. 2-quasitopoi, aka “2-categories of classes”

  51. on the possibility of a category of all sets

  52. Logic with a classifying discrete opfibration

  53. the logic of size?

  54. internal logic of stacks?

  55. More type constructors and higher-order aspects of logic (highly speculative, mostly scratchwork)

  56. definitional equality for 2-logic

  57. product types in a 2-category

  58. coproduct types in a 2-category?

  59. quotient types in a 2-category?

  60. dependent types in a 2-category

  61. functorially dependent types and dependent sums and products

  62. directional identity type?s

  63. Speculations on n-toposes for n>2n\gt 2.

About this project

In the course of investigating unbounded quantifiers in topos theory, I found myself forced into deploying an internal logic in a 2-category. Eventually I realized that the subject deserved an independent treatment.

I’m experimenting with using this private section of the nLab for this project. My goal is to share ideas with this wonderful community, stimulate discussion, and perhaps get feedback (and corrections) from people who are interested in higher-categorical stuff. Please go ahead and leave comments (the query syntax from the main nLab works here) and make corrections as you see fit. Also please give me references to other work in this direction that I may be unaware of. Currently my plan is to write a paper about this myself, with acknowledgements of any help I get from readers of these pages. If it becomes clear for any reason that this plan would be inappropriate, we’ll work something else out.

Last revised on June 12, 2012 at 11:10:00. See the history of this page for a list of all contributions to it.