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 structure on a general morphism $p:\mathrm{ \mathbf{ E}}\to\mathrm{ \mathbf{ B}}$ in a 2-category $\mathscr{ 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:\mathscr{ E}\to\mathscr{ B}$. In particular, we show how to lift the comprehension and quotient structures on a functor $p:\mathscr{ E}\to\mathscr{ B}$ to the categories of algebras or coalgebras associated to functors $F_{ \mathscr{ E}}:\mathscr{ E}\to\mathscr{ E}$ and $F_{ \mathscr{ B}}:\mathscr{ B}\to\mathscr{ 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.
Categories: math.CT cs.LO