Michael Shulman 2-categorical logic

Important Note: This is a collection of preliminary personal notes from approximately 2009-2012. None of them has been published or peer-reviewed, and in the years since they were written, a number of other authors have pushed the theory forward in published papers. I am keeping these notes available for reference, since they have already been cited by others. However, I recommend that when published references exist, they should be cited in preference to these notes.

As with pages on the main nLab, these notes are publicly editable. In particular, I encourage readers to add citations to published references on individual topic pages, for the convenience of later readers. (I simply do not have the time or knowledge to do that myself.) Some such references can be found on pages in the main nLab such as 2-logic and 2-sheaf.

– Mike Shulman

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.

Contents

1. Introduction:

   1. What is a 2-topos?
   2. On the meaning of “categorified logic”
   3. Conventions on terminology and the meaning of $n$-category
   4. The role of the axiom of choice

2. 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.

   1. slice 2-categories and fibrational slices
   2. 2-Congruences
   3. Regular 2-categories
   4. Classification of congruences
   5. Exact 2-categories
   6. Poly-congruences
   7. Coherent 2-categories
   8. Extensive 2-categories
   9. 2-pretoposes
   10. Heyting 2-categories

3. Additional levels of structure

   1. Cores and enough groupoids
   2. Natural numbers objects in 2-categories
   3. exponentials in a 2-category
   4. Duality involutions

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

   1. 2-sheaves (stacks) on a 2-site
   2. The 2-Giraud theorem
   3. Truncated 2-toposes
   4. Geometric morphisms between 2-toposes

5. Truncation and factorization systems

   1. Truncation
   2. The comprehensive factorization system
   3. full morphisms and the (eso+full, faithful) factorization system
   4. The Cauchy factorization system

6. Aspects of first-order structure

   1. colimits in an n-pretopos
   2. balancedness in n-pretoposes
   3. Regular and exact completions
   4. 3-sheaf conditions?
   5. The axiom of 2-choice

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

   1. internal logic of a 2-category
   2. the functor comprehension principle, and the description of faithful, ff, eso morphisms in the internal logic
   3. adjunctions in 2-logic
   4. Kripke-Joyal semantics in a 2-category?
   5. category theory in a 2-pretopos?
   6. syntactic 2-categories?
   7. classifying 2-toposes?

8. Classifying objects

   1. classifying discrete opfibrations
   2. classifying cosieves
   3. size structures
   4. 2-quasitopoi, aka “2-categories of classes”
   5. on the possibility of a category of all sets

9. Logic with a classifying discrete opfibration

   1. the logic of size?
   2. internal logic of stacks?

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

    1. definitional equality for 2-logic
    2. product types in a 2-category
    3. coproduct types in a 2-category?
    4. quotient types in a 2-category?
    5. dependent types in a 2-category
    6. functorially dependent types and dependent sums and products
    7. directional identity type?s

11. Speculations on n-toposes for $n\gt 2$.