module Cat.Instances.Slice.Twice {o ℓ} {C : Precategory o ℓ} where

Iterated slice categories🔗

An iterated slice category, something like $(C / B) / f$ for $f : A \to B$ (regarded as an object over $B),$ is something slightly mind-bending to consider at face value: the objects are families of families-over- $B$ , indexed by the family $f ?$ It sounds like there’s a lot of room for complexity here, and that’s only considering one iteration!

Fortunately, there’s actually no such thing. The slice of $C / B$ over $f$ is isomorphic to the slice $C / A,$ by a functor which is remarkably simple to define, too. That’s because the data of an object in $(C / B) / f$ consists of a morphism $h : X \to B,$ a morphism $g : X \to A,$ and a proof $p : h = f g .$ But by contractibility of singletons, the pair $(h, p)$ is redundant! The only part that actually matters is the morphism $g : X \to A .$

One direction of the isomorphism inserts the extra (redundant!) information, by explicitly writing out $h = f g$ and setting $p = refl .$ Its inverse simply discards the redundant information. We construct both of the functors here, in components.

Slice-twice : (f : Hom a b) → Functor (Slice C a) (Slice (Slice C b) (cut f))
Slice-twice f .F₀ g .domain .domain = g .domain
Slice-twice f .F₀ g .domain .map    = f ∘ g .map

Slice-twice f .F₀ g .map .map      = g .map
Slice-twice f .F₀ g .map .commutes = refl

Slice-twice f .F₁ h .map .map      = h .map
Slice-twice f .F₁ h .map .commutes = pullr (h .commutes)
Slice-twice f .F₁ h .commutes      = ext (h .commutes)

Slice-twice f .F-id    = trivial!
Slice-twice f .F-∘ g h = trivial!

Twice-slice : (f : Hom a b) → Functor (Slice (Slice C b) (cut f)) (Slice C a)
Twice-slice _ .F₀ x .domain = x .domain .domain
Twice-slice _ .F₀ x .map    = x .map .map

Twice-slice _ .F₁ h .map      = h .map .map
Twice-slice _ .F₁ h .commutes = ap map (h .commutes)

Twice-slice _ .F-id = trivial!
Twice-slice _ .F-∘ _ _ = trivial!

We will also need the fact that these inverses are also adjoints.

Twice⊣Slice : (f : Hom a b) → Twice-slice f ⊣ Slice-twice f
Twice⊣Slice f = adj where
  adj : Twice-slice f ⊣ Slice-twice f
  adj .unit .η x .map .map      = id
  adj .unit .η x .map .commutes = idr _ ∙ x .map .commutes
  adj .unit .η x .commutes      = ext (idr _)
  adj .unit .is-natural x y f   = ext id-comm-sym

  adj .counit .η x .map         = id
  adj .counit .η x .commutes    = idr _
  adj .counit .is-natural x y f = ext id-comm-sym

  adj .zig = ext (idr _)
  adj .zag = ext (idr _)