Comprehension and Quotient Structures in the Language of 2-Categories

Authors Paul-André Melliès , Nicolas Rolland

Thumbnail PDF


  • Filesize: 0.6 MB
  • 18 pages

Document Identifiers

Author Details

Paul-André Melliès
  • CNRS, Institut de Recherche en Informatique Fondamentale (IRIF), Université de Paris, France
Nicolas Rolland
  • Institut de Recherche en Informatique Fondamentale (IRIF), Université de Paris, France

Cite AsGet BibTex

Paul-André Melliès and Nicolas Rolland. Comprehension and Quotient Structures in the Language of 2-Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (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:E→ 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:E→ 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 structure on a general morphism p:𝐄→𝐁 in a 2-category K. This conceptual point of view on comprehension structures enables us to revisit the work by Fumex, Ghani and Johann on the duality between comprehension structures and quotient structures on a given functor p:E→B. In particular, we show how to lift the comprehension and quotient structures on a functor p:E→ B to the categories of algebras or coalgebras associated to functors F_E:E→E and F_B:B→B of interest, in order to interpret reasoning by induction and coinduction in the traditional language of categorical logic, formulated in an appropriate 2-categorical way.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
  • Theory of computation → Linear logic
  • Comprehension structures
  • quotient structures
  • comprehension structures with section
  • comprehension structures with image
  • 2-categories
  • formal adjunctions
  • path objects
  • categorical logic
  • inductive reasoning on algebras
  • coinductive reasoning on coalgebras


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jon Beck. Distributive laws. In Seminar on triples and categorical homology theory, pages 119-140. Springer, 1969. Google Scholar
  2. Clément Fumex. Induction and coinduction schemes in category theory. PhD thesis, University of Strathclyde, 2012. Google Scholar
  3. 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. Google Scholar
  4. IEEE Computer Society. A Categorical Semantics of Constructions, 1988. URL:
  5. B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  6. Bart Jacobs. Comprehension categories and the semantics of type dependency. Theor. Comput. Sci., 107(2):169-207, 1993. URL:
  7. 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. Google Scholar
  8. 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:
  9. Max Kelly. Doctrinal adjunction. In Category Seminar, pages 257-280. Springer, 1974. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. Sean Moss. The Dialectica Models of Type Theory. PhD thesis, University of Cambridge, 2018. Google Scholar
  13. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. Google Scholar
  14. Lawvere William. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Proceedings of the AMS Symposium on Pure Mathematics XVII, pages 1-14. AMS, 1970. Google Scholar
  15. Ernst Zermelo. Untersuchungen über die grundlagen der mengenlehre. i. Mathematische Annalen, 65(2):261-281, 1908. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail