The Azimuth Project
Displayed category

Definition. A displayed category is a lax functor π’žβ†’π•Špan(Set)\mathcal{C} \to \mathbb{S}\mathsf{pan}(\mathsf{Set}).

The following theorem is a generalization of the equivalence given by the Grothendieck construction between indexed categories and fibred categories. It can be found as Proposition 4 in Pavlovic-Abramsky, where they say they could not find the proof in any published work.

Theorem. π’ž/Cβ‰…[C,Span] lax\mathcal{C}/C \cong [C, \mathsf{Span}]_{lax}.


  • D. Pavlovic? and S. Abramsky?, Specifying interaction categories?, In: Moggi E., Rosolini G. (eds) Category Theory and Computer Science. CTCS 1997. Lecture Notes in Computer Science, vol 1290. Springer, Berlin, Heidelberg, 1997. DOI

  • Jean B ́enabou. Distributors at work, 2000. Lecture notes taken by Thomas Streicher. PDF

The term was introduced in: