open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Prelude

import Cat.Reasoning

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 $(\mathcal{C}/B)/f$ for $f:A\to B$ (regarded as an object over $B\text{),}$ is something slightly mind-bending to consider at face value: the objects are families of families-over-$B$, indexed by the family $f\text{?}$ 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 $\mathcal{C}/B$ over $f$ is isomorphic to the slice $\mathcal{C}/A\text{,}$ by a functor which is remarkably simple to define, too. That’s because the data of an object in $(\mathcal{C}/B)/f$ consists of a morphism $h:X\to B\text{,}$ a morphism $g:X\to A\text{,}$ and a proof $p:h=fg\text{.}$ But by contractibility of singletons, the pair $(h,p)$ is redundant! The only part that actually matters is the morphism $g:X\to A\text{.}$

One direction of the isomorphism inserts the extra (redundant!) information, by explicitly writing out $h=fg$ and setting $p=\mathrm{refl}\text{.}$ 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 _)