module Cat.Instances.Presheaf.Limits {o } (κ : Level) (C : Precategory o ) where

Limits in presheaf categories🔗

We present an explicit construction of finite limits in the category of presheaves on These are computed pointwise, with the value of e.g.  being the set Therefore, the constructions below are mostly rote.

First, the terminal presheaf is constantly the unit set, and all the laws (functoriality, naturality, universality) are trivial:

⊤PSh :  PSh κ C 
⊤PSh .F₀ x = el! (Lift κ )
⊤PSh .F₁ _ _ = lift tt
⊤PSh .F-id = refl
⊤PSh .F-∘ _ _ = refl

PSh-terminal : Terminal (PSh κ C)
PSh-terminal = record { has⊤ = uniq } where
  uniq : is-terminal (PSh κ C) ⊤PSh
  uniq x .centre .η _ _ = lift tt
  uniq x .centre .is-natural _ _ _ = refl
  uniq x .paths f = trivial!

The product presheaf is as described in the introduction, now with all the laws being componentwise; the projection maps are componentwise the product projections from and the pairing is, componentwise, pairing.

_×PSh_ :  PSh κ C    PSh κ C    PSh κ C 
(A ×PSh B) .F₀ x = el! ( A .F₀ x  ×  B .F₀ x )
(A ×PSh B) .F₁ f (x , y) = A .F₁ f x , B .F₁ f y
(A ×PSh B) .F-id i (x , y) = A .F-id i x , B .F-id i y
(A ×PSh B) .F-∘ f g i (x , y) = A .F-∘ f g i x , B .F-∘ f g i y

PSh-products : (A B :  PSh κ C )  Product (PSh κ C) A B
PSh-products A B = prod where
  open is-product
  open Product

  prod : Product (PSh _ C) A B
  prod .apex = A ×PSh B
  prod .π₁ = NT  x  fst)  _ _ _  refl)
  prod .π₂ = NT  x  snd)  _ _ _  refl)
  prod .has-is-product .⟨_,_⟩ f g =
    NT  i x  f .η i x , g .η i x) λ x y h i a 
      f .is-natural x y h i a , g .is-natural x y h i a
  prod .has-is-product .π₁∘⟨⟩ = trivial!
  prod .has-is-product .π₂∘⟨⟩ = trivial!
  prod .has-is-product .unique p q = ext λ i x  unext p i x ,ₚ unext q i x

Finally, we also construct pullbacks. As above, the construction is straightforwardly given by the relevant constructions on componentwise.

  pb : Pullback (PSh κ C) f g
  pb .apex .F₀ i = el! (Σ[ x  X.₀ i ] Σ[ y  Y.₀ i ] f.η i x  g.η i y)
  pb .apex .F₁ {x} {y} h (a , b , p) = X.₁ h a , Y.₁ h b , path where abstract
    path : f.η y (X.₁ h a)  g.η y (Y.₁ h b)
    path = happly (f.is-natural _ _ _) _
        ∙∙  i  Z.₁ h (p i))
        ∙∙ sym (happly (g.is-natural _ _ _) _)
  pb .apex .F-id = funext λ (a , b , _)  pb-path (X.F-id $ₚ a) (Y.F-id $ₚ b)
  pb .apex .F-∘ f g = funext λ (a , b , _)  pb-path (X.F-∘ f g $ₚ a) (Y.F-∘ f g $ₚ b)
  pb .p₁ .η idx (a , b , _) = a
  pb .p₁ .is-natural _ _ _ = refl
  pb .p₂ .η x (a , b , _) = b
  pb .p₂ .is-natural _ _ _ = refl
  pb .has-is-pb .square = ext λ _ _ _ p  p
  pb .has-is-pb .universal path .η idx arg = _ , _ , unext path _ _
  pb .has-is-pb .universal {p₁' = p₁'} {p₂'} path .is-natural x y f = funext λ x 
    pb-path (happly (p₁' .is-natural _ _ _) _) (happly (p₂' .is-natural _ _ _) _)
  pb .has-is-pb .p₁∘universal = trivial!
  pb .has-is-pb .p₂∘universal = trivial!
  pb .has-is-pb .unique p q = ext λ _ _ 
    pb-path (unext p _ _) (unext q _ _)

Continuity of evaluation🔗

We can also show abstractly that every limit of presheaves is computed pointwise, in line with the finitary constructions above. First, note that the operation for a fixed is functorial on presheaves; this is the evaluation functor.

private
  ev :  {ℓs} (c :  C )  Functor (PSh ℓs C) (Sets ℓs)
  ev c .F₀ F    = F · c
  ev c .F₁ h i  = h .η _ i
  ev c .F-id    = refl
  ev c .F-∘ f g = refl

This functor has a left adjoint, and since right adjoints preserve limits, we conclude that if is any limit of a diagram then we can conclude that is the limit of the

  clo :  {ℓs} (c :  C )  Functor (Sets ℓs) (PSh (ℓs  ) C)
  clo c .F₀ A = λ where
    .F₀ d          el! ( A  × Hom d c)
    .F₁ g (a , f)  a , f  g
    .F-id          ext λ a h  refl ,ₚ idr h
    .F-∘ f g       ext λ a h  refl ,ₚ assoc h g f

  clo c .F₁ f .η i (a , g) = f a , g
  clo c .F₁ f .is-natural x y g = refl
  clo c .F-id = trivial!
  clo c .F-∘ f g = trivial!

  clo⊣ev : (c :  C )  clo {} c  ev c
  clo⊣ev c = hom-iso→adjoints  f x  f .η _ (x , id)) (is-iso→is-equiv iiso) λ g h x  refl where
    open is-iso

    iiso :  {x : Set } {y :  PSh  C }  is-iso {A = clo c · x => y}  f x  f .η c (x , id))
    iiso {y = y} .inv f .η x (a , g) = y  g  (f a)
    iiso {y = y} .inv f .is-natural x z g = ext λ a h  PSh.expand y refl
    iiso {y = y} .rinv x = ext λ a  PSh.F-id y
    iiso {y = y} .linv x = ext  i y h  sym (x .is-natural _ _ _ $ₚ _)  ap (x .η i) (refl ,ₚ idl h))

As an important consequence is that if a natural transformation is monic, then so are all of its components — this follows from the above and from the observation that being a monomorphism is a limit property.

is-monic→is-embedding-at
  :  {X Y :  PSh  C } {m : X => Y}
   Cat.is-monic (PSh  C) m
    {i}  is-embedding (m .η i)
is-monic→is-embedding-at {Y = Y} {m} mono {i} =
  monic→is-embedding (hlevel 2) λ {C} g h 
    right-adjoint→is-monic _ (clo⊣ev i) mono {C} g h