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))