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. What is a 2-topos?

3. On the meaning of “categorified logic”

4. Conventions on terminology and the meaning of $n$-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\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.