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

open Cat.Reasoning C open Functor open /-Obj open /-Hom open _=>_ open _β£_ private variable a b : Ob

# Iterated slice categoriesπ

An **iterated slice category**, something like
$(C/B)/f$
for
$f:Aβ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βB,$
a morphism
$g:XβA,$
and a proof
$p:h=fg.$
But by contractibility of
singletons, the pair
$(h,p)$
is redundant! The only part that actually matters is the morphism
$g:XβA.$

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