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.

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