English

Logic and Concepts in the 2-category of Topoi

Logic 2025-05-22 v2 Logic in Computer Science Category Theory

Abstract

We use Kan injectivity to axiomatise concepts in the 2-category of topoi. We showcase the expressivity of this language through many examples, and we establish some aspects of the formal theory of Kan extension in this 2-category (pointwise Kan extensions, fully faithful morphisms, etc.). We use this technology to introduce fragments of geometric logic, and we accommodate essentially algebraic, disjunctive, regular, and coherent logic in our framework, together with some more exotic examples. We show that each fragment H\mathcal{H} in our sense identifies a lax-idempotent (relative) pseudomonad TH\mathsf{T}^{\mathcal{H}} on lex\mathsf{lex}, the 22-category of finitely complete categories. We show that the algebras for TH\mathsf{T}^{\mathcal{H}} admit a notion of classifying topos, for which we deliver several Diaconescu-type results. The construction of classifying topoi allows us to define conceptually complete fragments of geometric logic.

Keywords

Cite

@article{arxiv.2504.16690,
  title  = {Logic and Concepts in the 2-category of Topoi},
  author = {Ivan Di Liberti and Lingyuan Ye},
  journal= {arXiv preprint arXiv:2504.16690},
  year   = {2025}
}