Descent theory of locally internal categories (Q1588061)

Once a finitely-complete category \({\mathcal C}\) is embedded into the bicategory Span\({\mathcal C}\), categories internal to \({\mathcal C}\) are nothing but monads in Span\({\mathcal C}\). The author uses the notion of module (= profunctor or distributor in the sense of \textit{J. Bénabou}, = bimodule in the sense of \textit{F. W. Lawvere}) of internal categories to describe descent data for a morphism \(p\) in \({\mathcal C}\). This description and the emerging elementary theory depend only on the Span\({\mathcal C}\)-adjunction \(p\dashv p^0\) and therefore extend to more sophisticated contexts, such as locally internal categories and existential hyperdoctrines.