Category theory MOC

Displayed category theory MOC

From one perspective, the theory of displayed categories is redundant, since a displayed category 𝖤 over 𝖢 contains the same information as a “category-over”, that is an ordinary category ∫𝖤 (the total category) equipped with a functor ∫𝖤 →𝖢. There are, however, two main advantages to the displayed approach:

1. The traditional approach would have you construct ∫𝖤 from scratch, and then build a functor to 𝖢. Displayed categories are appropriate precisely when ∫𝖤 is built from 𝖢, by adding additional structure, and a “forgetful” functor is built simultaneously.
2. Displayed categories are in some sense ”externally” stronger than categories-over, since they have finer-grained control of definitional equality. Evil notions are often exorcised when formulated in the displayed setting, see for example Cartesian fibration. This is especially useful in type theory and in particular, Univalent Foundations.

Categories

• Displayed category
  • Total category of a displayed category
  • Fibre category

Examples

• Canonical self-indexing
  • 𝖲𝗎𝖻 ⇥𝖢

Morphisms of categories

• Displayed functor
• Displayed natural transformation

Fibrations of categories

• Cartesian morphism
• Cartesian fibration

#MOC | #state/develop | #lang/en | #SemBr