module Cat.Instances.Slice.Twice {o β„“} {C : Precategory o β„“} where

Iterated slice categoriesπŸ”—

An iterated slice category, something like for (regarded as an object over is something slightly mind-bending to consider at face value: the objects are families of families-over-, indexed by the family 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 over is isomorphic to the slice by a functor which is remarkably simple to define, too. That’s because the data of an object in consists of a morphism a morphism and a proof But by contractibility of singletons, the pair is redundant! The only part that actually matters is the morphism

One direction of the isomorphism inserts the extra (redundant!) information, by explicitly writing out and setting 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 _)