open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
open import Cat.Instances.Elements
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 a presheaf, we have an isomorphism where denotes the category of elements of

private
variable ΞΊ : Level
module C = Precategory C
open Precategory
open Element-hom
open Element
open Functor
open /-Obj
open /-Hom
open _=>_


An object in the slice consists of a functor together with a natural transformation To transform this data into a functor observe that for each element in the fibre is a set. But why this choice in particular? Well, observe that is essentially the total space of β 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 that latter equivalence is a special case of the one constructed here β where in the calculation below, denotes the constant presheaf The category of elements of a presheaf consists of pairs where of which there is only one choice, and

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) = el! (fibre (sl .map .Ξ· x) s)

slice-obβpresheaf sl .Fβ eh (i , p) =
sl .domain .Fβ (eh .hom) i
, happly (sl .map .is-natural _ _ _) _ Β·Β· ap (P.β _) p Β·Β· eh .commute

  slice-obβpresheaf sl .F-id =
funext Ξ» x β Ξ£-prop-path! (happly (sl .domain .F-id) _)
slice-obβpresheaf sl .F-β f g =
funext Ξ» x β Ξ£-prop-path! (happly (sl .domain .F-β _ _) _)

private abstract
lemma
: β (y : Functor (β« C P ^op) (Sets ΞΊ))
{o o'} {s} {s'} {el : y Κ» (elem o s)}
{f : C .Hom o' o} (p : P .Fβ f s β‘ s')
β subst (Ξ» e β y Κ» elem o' e) p (y .Fβ (elem-hom f refl) el)
β‘ y .Fβ (elem-hom f p) el
lemma y {o = o} {o' = o'} {el = it} {f = f} =
J (Ξ» s' p β subst (Ξ» e β y Κ» (elem o' e)) p (y .Fβ (elem-hom f refl) it)
β‘ y .Fβ (elem-hom f p) it)
(transport-refl _)


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 Κ» elem c sect
obj .domain .Fβ c .is-tr = hlevel 2
obj .domain .Fβ f (x , p) = P.β f x , y .Fβ (elem-hom f refl) p
obj .map .Ξ· x = fst

    obj .domain .F-id {ob} = funext Ξ» { (x , p) β Ξ£-path (happly (P.F-id) x) (lemma y _ β happly (y .F-id) _) }
obj .domain .F-β f g = funext Ξ» { (x , p) β
Ξ£-path (happly (P.F-β f g) x)
( lemma y _
Β·Β· ap (Ξ» e β y .Fβ (elem-hom (g C.β f) e) p) (P.β _ .is-tr _ _ _ _)
Β·Β· happly (y .F-β (elem-hom f refl) (elem-hom g refl)) _) }
obj .map .is-natural _ _ _ = refl


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) , h .commutes Ξ·β _ \$β arg .fst β arg .snd
func .Fβ {x} {y} h .is-natural _ _ _ = funext Ξ» i β
Ξ£-prop-path! (happly (h .map .is-natural _ _ _) _)

func .F-id    = ext Ξ» x y p β Ξ£-prop-path! refl
func .F-β f g = ext Ξ» x y p β Ξ£-prop-path! 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! refl)
β ap fst (happly (nt .is-natural _ _
(elem-hom f (happly (sym (x .map .is-natural _ _ _)) _))) _)

inv nt .commutes = ext Ξ» z w β
nt .Ξ· (elem _ (x .map .Ξ· _ _)) (w , refl) .snd

rinv : is-right-inverse inv (Fβ sliceβtotal)
rinv nt = ext Ξ» where
o z p β Ξ£-prop-path! Ξ» i β
nt .Ξ· (elem (o .ob) (p i)) (z , Ξ» j β p (i β§ j)) .fst

linv : is-left-inverse inv (Fβ sliceβtotal)
linv sh = trivial!

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.

    isom .rinv x =
Functor-path
(Ξ» i β n-ua (Fibre-equiv (Ξ» a β x Κ» elem (i .ob) a) (i .section)))
Ξ» f β uaβ Ξ» { ((a , b) , p) β pathβua-pathp _ (lemma x _ β lemma' _ _ _) }
where abstract
lemma'
: β {o o'} {sect : P Κ» o .ob}
(f : Hom (β« C P ^op) o o')
(b : x Κ» elem (o .ob) sect)
(p : sect β‘ o .section)
β x .Fβ (elem-hom (f .hom) (ap (P.β (f .hom)) p β f .commute)) b
β‘ x .Fβ f (subst (Ξ» e β x Κ» elem (o .ob) e) p b)
lemma' {o = o} {o' = o'} f b p =
J (Ξ» _ p β β f b β x .Fβ (elem-hom (f .hom) (ap (P.β (f .hom)) p β f .commute)) b
β‘ x .Fβ f (subst (Ξ» e β x Κ» elem (o .ob) e) p b))
(Ξ» f b β apβ (x .Fβ) (ext refl) (sym (transport-refl b)))
p f b

isom .linv x =
/-Obj-path
(Functor-path (Ξ» x β n-ua (Total-equiv _ eβ»ΒΉ))
Ξ» f β uaβ Ξ» a β pathβua-pathp _ refl)
(Nat-pathp _ _ (Ξ» x β uaβ (Ξ» x β sym (x .snd .snd))))

-- downgrade to an equivalence for continuity/cocontinuity
sliceβtotal-is-equiv : is-equivalence sliceβtotal
sliceβtotal-is-equiv = is-precat-isoβis-equivalence sliceβtotal-is-iso

totalβslice : Functor Cat[ (β« C P) ^op , Sets ΞΊ ] (Slice Cat[ C ^op , Sets ΞΊ ] P)
totalβslice = sliceβtotal-is-equiv .is-equivalence.Fβ»ΒΉ