# 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

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

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