Displayed Categories

Benedikt Ahrens 1, 2 Peter Lumsdaine 3
1 GALLINETTE - GALLINETTE
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : 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.
Type de document :
Communication dans un congrès
Dale Miller. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Sep 2017, Oxford, United Kingdom. Leibniz International Proceedings in Informatics (LIPIcs), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), 84 (5:1--5:16), 2017, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). 〈10.4230/LIPIcs.FSCD.2017.5〉
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01584770
Contributeur : Benedikt Ahrens <>
Soumis le : samedi 9 septembre 2017 - 16:38:55
Dernière modification le : jeudi 11 janvier 2018 - 06:28:16

Fichier

LIPIcs-FSCD-2017-5.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Benedikt Ahrens, Peter Lumsdaine. Displayed Categories. Dale Miller. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Sep 2017, Oxford, United Kingdom. Leibniz International Proceedings in Informatics (LIPIcs), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), 84 (5:1--5:16), 2017, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). 〈10.4230/LIPIcs.FSCD.2017.5〉. 〈hal-01584770〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

10