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