With acknowledgements to David Corfield and others, this project is grandiosely entitled
However, probably not all the hopes that might be aroused by such a title will be fulfilled. See the introduction for caveats.
Introduction:
On the meaning of “categorified logic”
Conventions on terminology and the meaning of $n$-category
The role of the axiom of choice
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.
Additional levels of structure
Cores and enough groupoids
Natural numbers objects in 2-categories
Grothendieck 2-toposes (also due to StreetCBS, see also the work of Igor Bakovic)
2-sheaves (stacks) on a 2-site
The 2-Giraud theorem
Truncation and factorization systems
The comprehensive factorization system
full morphisms and the (eso+full, faithful) factorization system
The Cauchy factorization system
Aspects of first-order structure
3-sheaf conditions?
First-order and geometric logic in a 2-category
the functor comprehension principle, and the description of faithful, ff, eso morphisms in the internal logic
Kripke-Joyal semantics in a 2-category?
category theory in a 2-pretopos?
syntactic 2-categories?
classifying 2-toposes?
Classifying objects
2-quasitopoi, aka “2-categories of classes”
on the possibility of a category of all sets
Logic with a classifying discrete opfibration
the logic of size?
internal logic of stacks?
More type constructors and higher-order aspects of logic (highly speculative, mostly scratchwork)
coproduct types in a 2-category?
quotient types in a 2-category?
functorially dependent types and dependent sums and products
directional identity type?s
Speculations on n-toposes for $n\gt 2$.
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.