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

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

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

6. 2-Congruences

7. Regular 2-categories

8. Classification of congruences

9. Exact 2-categories

10. Poly-congruences

11. Coherent 2-categories

12. Extensive 2-categories

13. 2-pretoposes

14. Heyting 2-categories

15. Additional levels of structure

16. Cores and enough groupoids

17. Natural numbers objects in 2-categories

18. exponentials in a 2-category

19. Duality involutions

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

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

22. Truncated 2-toposes

23. Geometric morphisms between 2-toposes

24. Truncation and factorization systems

25. Truncation

26. The comprehensive factorization system

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

28. The Cauchy factorization system

29. Aspects of first-order structure

30. colimits in an n-pretopos

31. balancedness in n-pretoposes

32. Regular and exact completions

33. 3-sheaf conditions?

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

35. internal logic of a 2-category

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

37. adjunctions in 2-logic

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

39. category theory in a 2-pretopos?

40. syntactic 2-categories?

41. classifying 2-toposes?

42. Classifying objects

43. size structures

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

45. on the possibility of a category of all sets

46. Logic with a classifying discrete opfibration

47. the logic of size?

48. internal logic of stacks?

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

50. definitional equality for 2-logic

51. product types in a 2-category

52. coproduct types in a 2-category?

53. quotient types in a 2-category?

54. dependent types in a 2-category

55. functorially dependent types and dependent sums and products

56. directional identity type?s

57. Speculations on n-toposes for $n\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.

Revised on June 12, 2012 11:10:00 by Andrew Stacey? (129.241.15.200)