open import Cat.Diagram.Limit.Finite
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.

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 = /-Hom-path (F .F-id)
Sliced F X .F-∘ f g = /-Hom-path (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 = /-Hom-path (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 = /-Hom-path (equiv→counit eqv _)
isom .is-iso.linv x = /-Hom-path (equiv→unit eqv _)


# Left exactness🔗

If $F$ is lex (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 {{\mathrm{id}}_{}}$ — but $F$ preserves this isomorphism, so we have $F(T) \cong F({{\mathrm{id}}_{}})$. But $F({{\mathrm{id}}_{}})$ is ${{\mathrm{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)
(record { has⊤ = 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 = /-Hom-path (adj.unit.is-natural _ _ _)

  adj′ .unit .η x .commutes =