publication . Preprint . 2020

Comprehension and quotient structures in the language of 2-categories

Melliès, Paul-André; Rolland, Nicolas;
Open Access English
  • Published: 20 May 2020
Lawvere observed in his celebrated work on hyperdoctrines that the set-theoretic schema of comprehension can be elegantly expressed in the functorial language of categorical logic, as a comprehension structure on the functor $p:\mathscr{E}\to\mathscr{B}$ defining the hyperdoctrine. In this paper, we formulate and study a strictly ordered hierarchy of three notions of comprehension structure on a given functor $p:\mathscr{E}\to\mathscr{B}$, which we call (i) comprehension structure, (ii) comprehension structure with section, and (iii) comprehension structure with image. Our approach is 2-categorical and we thus formulate the three levels of comprehension structur...
free text keywords: Mathematics - Category Theory, Computer Science - Logic in Computer Science
Funded by
Duality in Formal Languages and Logic - a unifying approach to complexity and semantics
  • Funder: European Commission (EC)
  • Project Code: 670624
  • Funding stream: H2020 | ERC | ERC-ADG
Download from

Jon Beck. Distributive laws. In Seminar on triples and categorical homology theory, pages 119-140. Springer, 1969.

Clément Fumex. Induction and coinduction schemes in category theory. PhD thesis, University of Strathclyde, 2012. doi:10.1016/0304-3975(93)90169-T.

Clément Fumex, Neil Ghani, and Patricia Johann. Indexed induction and coinduction, fibrationally. In Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, Proceedings, volume 6859, page 176. Springer Science & Business Media, 2011.

IEEE Computer Society. A Categorical Semantics of Constructions, 1988. URL: https: //

B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.

Sci., 107(2):169-207, 1993. URL:, doi: 10.1016/0304-3975(93)90169-T.

Farzad Jafarrahmani. Induction in the Fibred Multicategory. Master's thesis, LSV of ENS Cachan, and Theory Group within the School of Computer Science of University of Birmingham, 2020. supervised by Gilles Dowek and Noam Zeilberger.

G. M. Kelly and Ross Street. Review of the elements of 2-categories. In GregoryM Kelly, editor, Category Seminar, volume 420 of Lecture Notes in Mathematics, pages 75-103. Springer Berlin / Heidelberg, 1974. URL:, doi:10.1007/ bfb0063101. [OpenAIRE]

Max Kelly. Doctrinal adjunction. In Category Seminar, pages 257-280. Springer, 1974.

Paul-André Melliès. Categorical semantics of linear logic, pages 1 - 196. Number 27 in Panoramas et Synthèses. Société Mathématique de France, 2009.

Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015., 2015.

Sean Moss. The Dialectica Models of Type Theory. PhD thesis, University of Cambridge, 2018.

Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. [OpenAIRE]

In Proceedings of the AMS Symposium on Pure Mathematics XVII, pages 1-14. AMS, 1970.

Ernst Zermelo. Untersuchungen über die grundlagen der mengenlehre. i. Mathematische Annalen, 65(2):261-281, 1908. [OpenAIRE]

Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue