open import 1Lab.HLevel open import 1Lab.Path open import 1Lab.Type hiding (id ; _β_) open import Cat.Base module Cat.Displayed.Base where

# Displayed Categoriesπ

The core idea behind displayed categories is that we want to capture the idea of being able to place extra structure over some sort of βbaseβ category. For instance, we can think of categories of algebraic objects (monoids, groups, rings, etc) as being extra structure placed atop the objects of Set, and extra conditions placed atop the morphisms of Set.

We start by defining a displayed category over a base category $\mathcal{B}$ which will act as the category we add the extra structure to.

record Displayed {o β} (B : Precategory o β) (oβ² ββ² : Level) : Type (o β β β lsuc oβ² β lsuc ββ²) where no-eta-equality open Precategory B

For each object of the base category, we associate a type of objects.
Going back to our original example of algebraic structures over
${{\mathbf{Sets}}}$,
this would be something like `Monoid-on : Set β Type`

. This
highlights an important point for intuition: we should think of the
objects of the displayed category as *structures* over the
objects of the base.

field Ob[_] : Ob β Type oβ²

We do a similar thing for morphisms: For each morphism
`f : Hom x y`

in the base category, there is a
**set** of morphisms between objects in the displayed
category. Keeping with our running example, given a function
`f : X β Y`

and monoid structures
`M : Monoid-on X`

, `N : Monoid-on Y`

, then
`Hom[ f ] M N`

is the proposition that βf is a monoid
homomorphismβ. Again, we should best think of these as
*structures* over morphisms.

Hom[_] : β {x y} β Hom x y β Ob[ x ] β Ob[ y ] β Type ββ² Hom[_]-set : β {a b} (f : Hom a b) (x : Ob[ a ]) (y : Ob[ b ]) β is-set (Hom[ f ] x y)

We also have identity and composition of displayed morphisms, but
this is best thought of as witnessing that the identity morphism in the
base *has* some structure, and that composition
*preserves* that structure. For monoids, this would be a proof
that the identity function is a monoid homomorphism, and that the
composition of homomorphisms is indeed a homomorphism.

idβ² : β {a} {x : Ob[ a ]} β Hom[ id ] x x _ββ²_ : β {a b c x y z} {f : Hom b c} {g : Hom a b} β Hom[ f ] y z β Hom[ g ] x y β Hom[ f β g ] x z

Now, for the difficult part of displayed category theory: equalities.
If we were to naively try to write out the right-identity law, we would
immediately run into trouble. The problem is that
`fβ² ββ² idβ² : Hom[ f β id ] x y`

, but
`fβ² : Hom [ f ] x y`

! IE: the laws only hold relative to
equalities in the base category. Therefore, instead of using
`_β‘_`

, we *must* use `PathP`

. Letβs provide
some helpful notation for doing so.

infixr 40 _ββ²_ _β‘[_]_ : β {a b x y} {f g : Hom a b} β Hom[ f ] x y β f β‘ g β Hom[ g ] x y β Type ββ² _β‘[_]_ {a} {b} {x} {y} fβ² p gβ² = PathP (Ξ» i β Hom[ p i ] x y) fβ² gβ² infix 30 _β‘[_]_

Finally, the laws. These are mostly what one would expect, just done over the equalities in the base.

field idrβ² : β {a b x y} {f : Hom a b} β (fβ² : Hom[ f ] x y) β (fβ² ββ² idβ²) β‘[ idr f ] fβ² idlβ² : β {a b x y} {f : Hom a b} β (fβ² : Hom[ f ] x y) β (idβ² ββ² fβ²) β‘[ idl f ] fβ² assocβ² : β {a b c d w x y z} {f : Hom c d} {g : Hom b c} {h : Hom a b} β (fβ² : Hom[ f ] y z) β (gβ² : Hom[ g ] x y) β (hβ² : Hom[ h ] w x) β fβ² ββ² (gβ² ββ² hβ²) β‘[ assoc f g h ] ((fβ² ββ² gβ²) ββ² hβ²)