License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.6
URN: urn:nbn:de:0030-drops-123282
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12328/
Melliès, Paul-André ;
Rolland, Nicolas
Comprehension and Quotient Structures in the Language of 2-Categories
Abstract
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.
BibTeX - Entry
@InProceedings{mellis_et_al:LIPIcs:2020:12328,
author = {Paul-Andr{\'e} Melli{\`e}s and Nicolas Rolland},
title = {{Comprehension and Quotient Structures in the Language of 2-Categories}},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-155-9},
ISSN = {1868-8969},
year = {2020},
volume = {167},
editor = {Zena M. Ariola},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12328},
URN = {urn:nbn:de:0030-drops-123282},
doi = {10.4230/LIPIcs.FSCD.2020.6},
annote = {Keywords: 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}
}
|
Keywords: |
|
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 |
|
Collection: |
|
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
28.06.2020 |
