Displayed categories
From MaRDI portal
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.
Recommendations
Cites work
- Categorical logic and type theory
- Categorical structures for type theory in univalent foundations
- Displayed categories
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 195102 (Why is no real title available?)
- Isomorphism is equality
- The local universes model: an overlooked coherence construction for dependent type theories
- Univalent categories and the Rezk completion
Cited in
(22)- The construction of set-truncated higher inductive types
- Displayed categories
- Constructing higher inductive types as groupoid quotients
- scientific article; zbMATH DE number 7379288 (Why is no real title available?)
- Bicategories in univalent foundations
- Bicategories in univalent foundations
- Displayed Categories
- Bicategorical type theory: semantics and syntax
- What should a generic object be?
- Semantics for two-dimensional type theory
- mathlib4 Module Mathlib/CategoryTheory/ConcreteCategory/Basic
- Towards univalent reference types: the impact of univalence on denotational semantics
- Formalizing the algebraic small object argument in UniMath
- Displayed type theory and semi-simplicial types
- Bicategories of automata, automata in bicategories
- The categorical contours of the Chomsky-Schützenberger representation theorem
- The formal theory of monads, univalently
- Universal algebra in UniMath
- The univalence principle
- Reflexive graph lenses in univalent foundations
- Hofmann-Streicher lifting of fibred categories (extended version)
- Scott's representation theorem and the univalent Karoubi envelope
This page was built for publication: Displayed categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3121521)
