open import Cat.Functor.Equivalence
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Prelude

module Cat.Instances.Slice.Presheaf {o ℓ} {C : Precategory o ℓ} where


# Slices of presheaf categories🔗

We prove that slices of a presheaf category are again presheaf categories. Specifically, for $P$ a presheaf, we have an isomorphism $\psh(\ca{C})/P \cong \psh(\int P)$, where $\int$ denotes the category of elements of $P$.

An object in the slice $\psh(\ca{C})/P$ consists of a functor $Q$ together with a natural transformation $\eta : P \to Q$. To transform this data into a functor $\int P \to \sets$, observe that for each element $(x, s)$ in $\int P$, the fibre $\eta_x^*(s)$ is a set. But why this choice in particular? Well, observe that $\int P$ is essentially the total space of $P$ — so that what we’re doing here is proving an equivalence between fibrations and dependent functions! This is in line with the existence of object classifiers, and in the 1-categorical level, with slices of Sets.

In fact, since we have $\sets = \psh(*)$, that latter equivalence is a special case of the one constructed here — where in the calculation below, $c$ denotes the constant presheaf $* \mapsto S$. The category of elements of a presheaf $* \mapsto S$ consists of pairs $(x, e)$ where $x : *$, of which there is only one choice, and $e : S$.

$\sets/S \cong \psh(*)/c(S) \cong \psh(\textstyle\int c(S)) \cong \psh(\id{Disc}(S))$

module _ {P : Functor (C ^op) (Sets κ)} where
private module P = Functor P

slice-ob→presheaf
: Ob (Slice Cat[ C ^op , Sets κ ] P)
→ Functor (∫ C P ^op) (Sets κ)
slice-ob→presheaf sl .F₀ (elem x s) =
fibre (sl .map .η x) s
, Σ-is-hlevel 2 (sl .domain .F₀ _ .is-tr) λ _ → is-prop→is-set (P.₀ _ .is-tr _ _)

slice-ob→presheaf sl .F₁ eh (i , p) =
sl .domain .F₁ (eh .hom) i
, happly (sl .map .is-natural _ _ _) _ ·· ap (P.₁ _) p ·· eh .commute


Keeping with the theme, in the other direction, we take a total space rather than a family of fibres, with fibration being the first projection fst:

  presheaf→slice-ob : Functor (∫ C P ^op) (Sets κ) → Ob (Slice Cat[ C ^op , Sets κ ] P)
presheaf→slice-ob y = obj where
obj : /-Obj {C = Cat[ _ , _ ]} P
obj .domain .F₀ c =
Σ[ sect ∈ ∣ P.₀ c ∣ ] ∣ y .F₀ (elem c sect) ∣
, Σ-is-hlevel 2 (P.₀ _ .is-tr) λ _ → y .F₀ _ .is-tr
obj .domain .F₁ f (x , p) = P.₁ f x , y .F₁ (elem-hom f refl) p
obj .map .η x = fst


Since the rest of the construction is routine calculation, we present it without comment.

  slice→total : Functor (Slice Cat[ C ^op , Sets κ ] P) Cat[ (∫ C P) ^op , Sets κ ]
slice→total = func where
func : Functor (Slice Cat[ C ^op , Sets κ ] P) Cat[ (∫ C P) ^op , Sets κ ]
func .F₀ = slice-ob→presheaf
func .F₁ {x} {y} h .η i arg =
h .map .η (i .ob) (arg .fst) , ap (λ e → e .η _ (arg .fst)) (h .commutes) ∙ arg .snd
func .F₁ {x} {y} h .is-natural _ _ _ = funext λ i →
Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) (happly (h .map .is-natural _ _ _) _)

func .F-id    = Nat-path (λ x → funext λ y → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) refl)
func .F-∘ f g = Nat-path (λ x → funext λ y → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) refl)

slice→total-is-ff : is-fully-faithful slice→total
slice→total-is-ff {x} {y} = is-iso→is-equiv (iso inv rinv linv) where
inv : Hom Cat[ ∫ C P ^op , Sets _ ] _ _
→ Slice Cat[ C ^op , Sets _ ] P .Hom _ _
inv nt .map .η i o = nt .η (elem _ (x .map .η i o)) (o , refl) .fst

inv nt .map .is-natural _ _ f = funext λ z →
ap (λ e → nt .η _ e .fst) (Σ-prop-path (λ _ → P.₀ _ .is-tr _ _) refl)
∙ ap fst (happly (nt .is-natural _ _
(elem-hom f (happly (sym (x .map .is-natural _ _ _)) _))) _)

inv nt .commutes = Nat-path λ z → funext λ w →
nt .η (elem _ (x .map .η _ _)) (w , refl) .snd

rinv : is-right-inverse inv (F₁ slice→total)
rinv nt = Nat-path λ o → funext λ where
(z , p) → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _)
(λ i → nt .η (elem (o .ob) (p i)) (z , (λ j → p (i ∧ j))) .fst)

linv : is-left-inverse inv (F₁ slice→total)
linv sh = /-Hom-path (Nat-path (λ z → refl))

open is-precat-iso
slice→total-is-iso : is-precat-iso slice→total
slice→total-is-iso .has-is-ff = slice→total-is-ff
slice→total-is-iso .has-is-iso = is-iso→is-equiv isom where
open is-iso
isom : is-iso slice-ob→presheaf
isom .inv = presheaf→slice-ob


Proving that the constructions presheaf→slice-ob and slice-ob→presheaf are inverses is mosly incredibly fiddly path algebra, so we omit the proof.