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

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