Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Displayed Categories
Stockholm University, Faculty of Science, Department of Mathematics.
Number of Authors: 22019 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 15, no 1, article id 20Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2019. Vol. 15, no 1, article id 20
Keywords [en]
Category theory, Dependent type theory, Computer proof assistants, Coq, Univalent mathematics
National Category
Computer Sciences Algebra and Logic
Identifiers
URN: urn:nbn:se:su:diva-168464DOI: 10.23638/LMCS-15(1:20)2019ISI: 000463358400009OAI: oai:DiVA.org:su-168464DiVA, id: diva2:1313170
Available from: 2019-05-02 Created: 2019-05-02 Last updated: 2019-05-02Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Lumsdaine, Peter Lefanu
By organisation
Department of Mathematics
In the same journal
Logical Methods in Computer Science
Computer SciencesAlgebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 98 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf