open import Cat.Diagram.Limit.Finite
open import Cat.Functor.Properties
open import Cat.Diagram.Terminal
open import Cat.Functor.Pullback
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Slice where


# Slicing functorsπ

Let $F : \mathcal{C} \to \mathcal{D}$ be a functor and $X : \mathcal{C}$ an object. By a standard tool in category theory (namely βwhacking an entire commutative diagram with a functorβ), $F$ restricts to a functor $F/X : \mathcal{C}/X \to \mathcal{D}/F(X)$. We call this βslicingβ the functor $F$. This module investigates some of the properties of sliced functors.

open Functor
open /-Obj
open /-Hom
open _=>_
open _β£_

Sliced : β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β (F : Functor C D)
β (X : Precategory.Ob 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 $f : x \to y \in \mathcal{C}$ from a map $h : F(x) \to F(y) \in \mathcal{D}/F(X)$, it does not necessarily restrict to a map in $\mathcal{C}/X$. Weβd have to show $F(y)h=F(x)$ and $h=F(f)$ implies $yf=x$, which is possible only if $F$ is faithful.

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


However, if $F$ is faithful, then so are any of its slices $F/X$, and additionally, if $F$ 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 $F$ is left exact (meaning it preserves pullbacks and the terminal object), then $F/X$ is lex as well. We note that it (by definition) preserves products, since products in $\mathcal{C}/X$ are equivalently pullbacks in $\mathcal{C}/X$. Pullbacks are also immediately shown to be preserved, since a square in $\mathcal{C}/X$ is a pullback iff it is a pullback in $\mathcal{C}$.

Sliced-lex
: β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β {F : Functor C D} {X : Precategory.Ob 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 $T$ is terminal, we know that $T \cong \operatorname{id}_{}$ β but $F$ preserves this isomorphism, so we have $F(T) \cong F(\operatorname{id}_{})$. But $F(\operatorname{id}_{})$ is $\operatorname{id}_{}$ again, now in $\mathcal{D}$, so $F(T)$, 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 $L \dashv R$, then $R/X$ is also a right adjoint. The left adjoint isnβt quite $L/X$, because the types there donβt match, nor is it $L/R(x)$ β but itβs quite close. We can adjust that functor by postcomposition with the counit $\varepsilon : LR(x) \to x$A to get a functor left adjoint to $R/X$.

Sliced-adjoints
: β {o β o' β'} {C : Precategory o β} {D : Precategory o' β'}
β {L : Functor C D} {R : Functor D C} (adj : L β£ R) {X : Precategory.Ob 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 _ _ _)

adj' .counit .is-natural x y f = ext (adj.counit.is-natural _ _ _)


  adj' .unit .Ξ· x .commutes =