open import Cat.Displayed.Base open import Cat.Prelude import Cat.Reasoning as CR module Cat.Displayed.Instances.Slice {o β} (B : Precategory o β) where open Displayed open CR B

# Slices as a Displayed Categoryπ

There is a canonical way of viewing any category as displayed over itself. Recall that the best way to think about displayed categories is adding extra structure over each of the objects of the base. Here, we only really have one natural choice of extra structure for objects: morphisms into that object!

record Slice (x : Ob) : Type (o β β) where constructor slice field over : Ob index : Hom over x open Slice

As a point of intuition: the name `Slice`

should evoke the feeling of βslicing upβ `over`

. If we restrict ourselves to Set, we can view a map `over β x`

as a partition of `over`

into `x`

different fibres. In other words, this provides an x-indexed collection of sets. This view of viewing slices as means of indexing is a very fruitful one, and should be something that you keep in the back of your head.

Now, the morphisms:

record Slice-hom {x y} (f : Hom x y) (px : Slice x) (py : Slice y) : Type (o β β) where constructor slice-hom private module px = Slice px module py = Slice py field to : Hom px.over py.over commute : f β px.index β‘ py.index β to open Slice-hom

Going back to our intuition of βslices as a means of indexing,β a morphism of slices performs a sort of reindexing operation. The morphism in the base performs our re-indexing, and then we ensure that we have some morphism between the indexed collections that preserves indexing, relative to the re-indexing operation.

## Slice Lemmasπ

Before we show this thing is a displayed category, we need to prove some lemmas. These are extremely unenlightening, so the reader should feel free to skip these (and probably ought to!).

module _ {x y} {f g : Hom x y} {px : Slice x} {py : Slice y} {fβ² : Slice-hom f px py} {gβ² : Slice-hom g px py} where

Paths of slice morphisms are determined by paths between the base morphisms, and paths between the βupperβ morphisms.

Slice-pathp : (p : f β‘ g) β (fβ² .to β‘ gβ² .to) β PathP (Ξ» i β Slice-hom (p i) px py) fβ² gβ² Slice-pathp p pβ² i .to = pβ² i Slice-pathp p pβ² i .commute = is-propβpathp (Ξ» i β Hom-set _ _ (p i β px .index) (py .index β (pβ² i))) (fβ² .commute) (gβ² .commute) i

module _ {x y} (f : Hom x y) (px : Slice x) (py : Slice y) where Slice-is-set : is-set (Slice-hom f px py) Slice-is-set = is-hlevelβ 2 (IsoβEquiv eqv eβ»ΒΉ) (hlevel 2) where open HLevel-instance

## Pulling it all togetherπ

Now that we have all the ingredients, the proof that this is all a displayed category follows rather easily. Itβs useful to reinforce what weβve actually done here though! We can think of morphisms into some object `x`

as βstructures on `x`

,β and then commuting squares as βstructures over morphisms.β

Slices : Displayed B (o β β) (o β β) Slices .Ob[_] = Slice Slices .Hom[_] = Slice-hom Slices .Hom[_]-set = Slice-is-set Slices .idβ² = slice-hom id id-comm-sym Slices ._ββ²_ {x = x} {y = y} {z = z} {f = f} {g = g} px py = slice-hom (px .to β py .to) $ (f β g) β x .index β‘β¨ pullr (py .commute) β©β‘ f β (index y β py .to) β‘β¨ extendl (px .commute) β©β‘ z .index β (px .to β py .to) β Slices .idrβ² {f = f} fβ² = Slice-pathp (idr f) (idr (fβ² .to)) Slices .idlβ² {f = f} fβ² = Slice-pathp (idl f) (idl (fβ² .to)) Slices .assocβ² {f = f} {g = g} {h = h} fβ² gβ² hβ² = Slice-pathp (assoc f g h) (assoc (fβ² .to) (gβ² .to) (hβ² .to))