module Cat.Functor.Slice where

# Slicing functorsπ

Let be a functor and an object. By a standard tool in category theory (namely βwhacking an entire commutative diagram with a functorβ), restricts to a functor We call this βslicingβ the functor This module investigates some of the properties of sliced functors.

Sliced : β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β (F : Functor C D) (X : β C β)
β Functor (Slice C X) (Slice D (F .Fβ X))
Sliced F X .Fβ ob = cut (F .Fβ (ob .map))
Sliced F X .Fβ sh = sh' where
sh' : /-Hom _ _
sh' .map = F .Fβ (sh .map)
sh' .commutes = sym (F .F-β _ _) β ap (F .Fβ) (sh .commutes)
Sliced F X .F-id = ext (F .F-id)
Sliced F X .F-β f g = ext (F .F-β _ _)

# Faithful, fully faithfulπ

Slicing preserves faithfulness and fully-faithfulness. It does not preserve fullness: Even if, by fullness, we get a map from a map it does not necessarily restrict to a map in Weβd have to show and implies which is possible only if is faithful.

module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
{F : Functor C D} {X : β C β} where
private
module D = Cat.Reasoning D

However, if is faithful, then so are any of its slices and additionally, if is full, then the sliced functors are also fully faithful.

Sliced-faithful : is-faithful F β is-faithful (Sliced F X)
Sliced-faithful faith p = ext (faith (ap map p))

Sliced-ff : is-fully-faithful F β is-fully-faithful (Sliced F X)
Sliced-ff eqv = is-isoβis-equiv isom where
isom : is-iso _
isom .is-iso.inv sh = record
{ map = equivβinverse eqv (sh .map)
; commutes = ap fst \$ is-contrβis-prop (eqv .is-eqv _)
(_ , F .F-β _ _ β apβ D._β_ refl (equivβcounit eqv _) β sh .commutes) (_ , refl)
}
isom .is-iso.rinv x = ext (equivβcounit eqv _)
isom .is-iso.linv x = ext (equivβunit eqv _)

# Left exactnessπ

If is left exact (meaning it preserves pullbacks and the terminal object), then is lex as well. We note that it (by definition) preserves products, since products in are equivalently pullbacks in Pullbacks are also immediately shown to be preserved, since a square in is a pullback iff it is a pullback in

Sliced-lex
: β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β {F : Functor C D} {X : β C β}
β is-lex F
β is-lex (Sliced F X)
Sliced-lex {C = C} {D = D} {F = F} {X = X} flex = lex where
module D = Cat.Reasoning D
module Dx = Cat.Reasoning (Slice D (F .Fβ X))
module C = Cat.Reasoning C
open is-lex
lex : is-lex (Sliced F X)
lex .pres-pullback = pullback-aboveβpullback-below
β flex .pres-pullback
β pullback-belowβpullback-above

That the slice of lex functor preserves the terminal object is slightly more involved, but not by a lot. The gist of the argument is that we know what the terminal object is: Itβs the identity map! So we can cheat: Since we know that is terminal, we know that β but preserves this isomorphism, so we have But is again, now in so being isomorphic to the terminal object, is itself terminal!

lex .pres-β€ {T = T} term =
is-terminal-iso (Slice D (F .Fβ X))
(subst (Dx._β cut (F .Fβ (T .map))) (ap cut (F .F-id))
(F-map-iso (Sliced F X)
(β€-unique (Slice C X) Slice-terminal-object (record { hasβ€ = term }))))
Slice-terminal-object'

A very important property of sliced functors is that, if then is also a right adjoint. The left adjoint isnβt quite because the types there donβt match, nor is it β but itβs quite close. We can adjust that functor by postcomposition with the counit to get a functor left adjoint to

: β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β {L : Functor C D} {R : Functor D C} (adj : L β£ R) {X : β D β}
β (Ξ£f (adj .counit .Ξ· _) Fβ Sliced L (R .Fβ X)) β£ Sliced R X
module L = Functor L
module R = Functor R
module C = Cat.Reasoning C
module D = Cat.Reasoning D

adj' : (Ξ£f (adj .counit .Ξ· _) Fβ Sliced L (R .Fβ X)) β£ Sliced R X
adj' .unit .is-natural x y f = ext (adj.unit.is-natural _ _ _)