##
**Displayed categories.**
*(English)*
Zbl 1419.18001

The article introduces the notion of display category. This concept is easily formalised as a category \(\mathcal{D}\) over \(\mathcal{C}\) together with a functor \(F: \mathcal{D} \to \mathcal{C}\) such that the objects of \(\mathcal{D}\) are given as a family indexed by \(\mathsf{Obj} \mathcal{C}\), and similarly for the morphisms, together with the obvious categorical constraints.

Then, the paper shows how creation of limits and Grothendieck fibrations, isofibrations, and discrete fibrations can be rendered by display categories. Finally, the article discusses how to use display categories within the univalent foundation framework.

At a first sight, the notion of display category appears to be very simple and unnecessary. However, the article convincingly shows that it should be understood as a natural, pragmatic tool, which encapsulates the core of most concrete examples of fibrations and their use. In this respect, the problematic issue of equality can be avoided, thus making the concept specifically useful in homotopy type theory, in which equality is a delicate notion requiring careful management. Moreover, the notion of display category is particularly well suited for computer formalisation and, in fact, all the results in the paper are also available as part of the \(\mathsf{UniMath}\) library for the \(\mathsf{Coq}\) proof assistant.

Summarising, this paper develops a natural and pragmatic tool which could be of interest to anyone working in univalent mathematics, and/or in the borderline between the formalisation and the semantics of type theories. The clean and sharp style of the article adds to the understanding and greatly helps whoever intends to apply the concept of display category in her own work.

Then, the paper shows how creation of limits and Grothendieck fibrations, isofibrations, and discrete fibrations can be rendered by display categories. Finally, the article discusses how to use display categories within the univalent foundation framework.

At a first sight, the notion of display category appears to be very simple and unnecessary. However, the article convincingly shows that it should be understood as a natural, pragmatic tool, which encapsulates the core of most concrete examples of fibrations and their use. In this respect, the problematic issue of equality can be avoided, thus making the concept specifically useful in homotopy type theory, in which equality is a delicate notion requiring careful management. Moreover, the notion of display category is particularly well suited for computer formalisation and, in fact, all the results in the paper are also available as part of the \(\mathsf{UniMath}\) library for the \(\mathsf{Coq}\) proof assistant.

Summarising, this paper develops a natural and pragmatic tool which could be of interest to anyone working in univalent mathematics, and/or in the borderline between the formalisation and the semantics of type theories. The clean and sharp style of the article adds to the understanding and greatly helps whoever intends to apply the concept of display category in her own work.

Reviewer: Marco Benini (Buccinasco)

### MSC:

18A15 | Foundations, relations to logic and deductive systems |

03B15 | Higher-order logic; type theory (MSC2010) |

### Keywords:

category theory; dependent type theory; computer proof assistants; Coq; univalent mathematics
PDFBibTeX
XMLCite

\textit{B. Ahrens} and \textit{P. Lefanu Lumsdaine}, Log. Methods Comput. Sci. 15, No. 1, Paper No. 20, 18 p. (2019; Zbl 1419.18001)

Full Text:
arXiv

### References:

[1] | [AHS90] 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, http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html. · Zbl 0695.18001 |

[2] | [AKS15] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman, Univalent categories and the Rezk completion, Mathematical Structures in Computer Science 25 (2015), 1010-1039, arXiv:1303.0584, doi:10.1017/S0960129514000486. · Zbl 1362.18003 |

[3] | [AL17]Benedikt Ahrens and Peter LeFanu Lumsdaine, Displayed categories (conference version), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (Dale Miller, ed.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, Leibniz-Zentrum für Informatik, 2017, pp. 5:1-5:16, arXiv:1705.04296v1, doi:10.4230/LIPIcs.FSCD.2017.5. · Zbl 1419.18001 |

[4] | [ALV18] Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky, Categorical structures for type theory in univalent foundations, Logical Methods in Computer Science 14(3) (2018), arXiv: 1705.04310, doi:10.23638/LMCS-14(3:18)2018, https://lmcs.episciences.org/4814. · Zbl 1496.03053 |

[5] | [Bén00]Jean Bénabou, Distributors at work, Notes by Thomas Streicher from lectures given at TU Darmstadt, 2000, http://www.mathematik.tu-darmstadt.de/ streicher/FIBR/DiWo.pdf. |

[6] | [Bla91]Javier Blanco, Relating categorical approaches to type theory, 1991, Master thesis, Univ. Nijmegen. |

[7] | [CD13]Thierry Coquand and Nils Anders Danielsson, Isomorphism is equality, Indagationes Mathematicae 24 (2013), no. 4, 1105 – 1120, In memory of N.G. (Dick) de Bruijn (1918-2012), doi:10.1016/j. indag.2013.09.002. · Zbl 1359.03010 |

[8] | [Jac99]Bart Jacobs, Categorical logic and type theory, Studies in Logic and the Foundations of Mathematics, vol. 141, Elsevier, 1999. · Zbl 0911.03001 |

[9] | [LW15]Peter LeFanu Lumsdaine and Michael A. Warren, The local universes model: an overlooked coherence construction for dependent type theories, ACM Trans. Comput. Log. 16 (2015), no. 3, Art. 23, 31, arXiv:1411.1736, doi:10.1145/2754931. · Zbl 1354.03101 |

[10] | [Uni13]The Univalent Foundations Program, Homotopy type theory: Univalent foundations of mathematics, Institute for Advanced Study, 2013, http://homotopytypetheory.org/book. · Zbl 1298.03002 |

[11] | [VAG+] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al., UniMath — a computer-checked library of univalent mathematics, https://github.com/UniMath/UniMath. 1. Introduction1.1. Outline1.2. Formalisation1.3. Revision notes2. Background2.1. Logical setting2.2. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.