2020/05/20 by Melliès, Paul-André, Rolland, Nicolas
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2005.10015
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:\mathscrE→\mathscrB 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:\mathscrE→\mathscrB, 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:E\toB in a 2-category \mathscrK. 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:\mathscrE→\mathscrB. In particular, we show how to lift the comprehension and quotient structures on a functor p:\mathscrE→\mathscrB to the categories of algebras or coalgebras associated to functors F_\mathscrE:\mathscrE→\mathscrE and F_\mathscrB:\mathscrB→\mathscrB 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.