Displayed Categories

Authors Benedikt Ahrens, Peter LeFanu Lumsdaine

Thumbnail PDF


  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Benedikt Ahrens
Peter LeFanu Lumsdaine

Cite AsGet BibTex

Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to "a category D and functor F : D -> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
  • Category theory
  • Dependent type theory
  • Computer proof assistants
  • Coq
  • Univalent mathematics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. Pure and Applied Mathematics (New York). John Wiley &Sons, Inc., New York, 1990. URL: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 2015. http://arxiv.org/abs/1303.0584, URL: http://dx.doi.org/10.1017/S0960129514000486.
  3. Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical structures for type theory in univalent foundations, 2017. To be published in proceedings of Computer Science Logic (CSL) 2017. URL: http://arxiv.org/abs/1705.04310.
  4. Jean Bénabou. Distributors at work. Notes by Thomas Streicher from lectures given at TU Darmstadt, 2000. URL: http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  5. Javier Blanco. Relating categorical approaches to type theory, 1991. Master thesis, Univ. Nijmegen. Google Scholar
  6. Bart Jacobs. Comprehension categories and the semantics of type dependency. Theor. Comput. Sci., 107(2):169-207, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90169-T.
  7. Bart Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1999. Google Scholar
  8. Tom Leinster. Basic Category Theory, volume 143 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2014. Google Scholar
  9. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  10. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: Univalent Mathematics. Available at URL: https://github.com/UniMath.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail