open import Cat.Diagram.Limit.Base
open import Cat.Instances.Comma
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cat
module Cat.Instances.Comma.Limits where
open make-is-limit
open ↓Obj
open ↓Hom
open _=>_

Limits in comma categoriesπŸ”—

This short note proves the following fact about limits in comma categories of the form If has a limit for and preserves limits the size of shape then can be made into an object of and this object is the limit of 

module
  _ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'} {d}
    (F : Functor C D) {lo lβ„“} (F-cont : is-continuous lo lβ„“ F)
    {J : Precategory lo lβ„“} {G : Functor J (d ↙ F)}
  where

  private
    module G = Functor G
    module D = Cat D
    module C = Cat C
    module F = Fr F
  Cod-lift-limit : Limit (Cod _ F F∘ G) β†’ Limit G
  Cod-lift-limit limf = to-limit (to-is-limit lim') where
    module limf = Limit limf

    flimf = F-cont limf.has-limit
    module flimf = is-limit flimf

The family of maps can be given componentwise, since is a limit in it suffices to give a family of maps at each But sends objects of to pairs which include a map and it does so in a way compatible with by definition.

    apex : ⌞ d ↙ F ⌟
    apex .x = tt
    apex .y = limf.apex
    apex .map = flimf.universal (Ξ» j β†’ G.β‚€ j .map) Ξ» f β†’ sym (G.₁ f .sq) βˆ™ D.elimr refl

Similarly short calculations show that we can define maps in into componentwise, and these satisfy the universal property.

    lim' : make-is-limit G apex
    lim' .ψ j .α = tt
    lim' .ψ j .β = limf.ψ j
    lim' .ψ j .sq = sym (flimf.factors _ _ βˆ™ D.intror refl)
    lim' .commutes f = ext (sym (limf.eps .is-natural _ _ _) βˆ™ C.elimr limf.Ext.F-id)
    lim' .universal eta p .Ξ± = tt
    lim' .universal eta p .Ξ² = limf.universal (Ξ» j β†’ eta j .Ξ²) Ξ» f β†’ ap Ξ² (p f)
    lim' .universal eta p .sq = D.elimr refl βˆ™ sym (flimf.unique _ _ _ Ξ» j β†’ F.pulll (limf.factors _ _) βˆ™ sym (eta j .sq) βˆ™ D.elimr refl)
    lim' .factors eta p = ext (limf.factors _ _)
    lim' .unique eta p other q = ext (limf.unique _ _ _ Ξ» j β†’ ap Ξ² (q j))

As an easy corollary, we get: if is small-complete and small-continuous, then is small-complete as well.

module
  _ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
    (F : Functor C D) (c-compl : is-complete β„“ β„“ C) (F-cont : is-continuous β„“ β„“ F)
    where
  private
    module C = Cat C
    module D = Cat D
    module F = Fr F
  comma-is-complete : βˆ€ {d} β†’ is-complete β„“ β„“ (d ↙ F)
  comma-is-complete G = Cod-lift-limit F F-cont (c-compl (Cod _ F F∘ G))