module Cat.Instances.Functor.Limits where

Limits in functor categoriesπŸ”—

Let be a category admitting limits. Then the functor category for any category, also admits limits. In particular, if is then so is

module _
  {o₁ ℓ₁} {C : Precategory o₁ ℓ₁}
  {oβ‚‚ β„“β‚‚} {D : Precategory oβ‚‚ β„“β‚‚}
  {o₃ ℓ₃} {E : Precategory o₃ ℓ₃}
  (has-D-lims : (F : Functor D C) β†’ Limit F)
  (F : Functor D Cat[ E , C ])
  where

Let be a diagram, and suppose admits limits of diagrams; We wish to compute the limit First, observe that we can Uncurry to obtain a functor By fixing the value of the coordinate (say, to we obtain a family of diagrams in which, by assumption, all have limits.

    F-uncurried : Functor (D Γ—αΆœ E) C
    F-uncurried = Uncurry {C = D} {D = E} {E = C} F

    import Cat.Functor.Bifunctor {C = D} {D = E} {E = C} F-uncurried as F'
    module D-lim x = Limit (has-D-lims (F'.Left x))

Let us call the limit of β€” taken in β€” lim-for, and similarly the unique, β€œterminating” cone homomorphism will be called !-for.

    !-for : βˆ€ {x y} (f : E.Hom x y) β†’ C.Hom (D-lim.apex x) (D-lim.apex y)
    !-for {x} {y} f =
      D-lim.universal y
        (Ξ» j β†’ F'.Right j .F₁ f C.∘ D-lim.ψ x j)
        (Ξ» g β†’
          C.extendl F'.first∘second
          βˆ™ apβ‚‚ C._∘_ refl (D-lim.commutes x g))

    functor-apex : Functor E C
    functor-apex .Fβ‚€ x = D-lim.apex x
    functor-apex .F₁ {x} {y} f = !-for f
    functor-apex .F-id =
      sym $ D-lim.unique _ _ _ _ Ξ» j β†’
        C.idr _ βˆ™ sym (D-lim.commutes _ _)
    functor-apex .F-∘ f g =
      sym $ D-lim.unique _ _ _ _ Ξ» j β†’
        C.pulll (D-lim.factors _ _ _)
        βˆ™ C.pullr (D-lim.factors _ _ _)
        βˆ™ C.pulll (sym (F'.Right _ .F-∘ _ _))

  functor-limit : Limit F
  functor-limit = to-limit $ to-is-limit ml where
    open make-is-limit

    ml : make-is-limit F functor-apex
    ml .ψ j .η x = D-lim.ψ x j
    ml .ψ j .is-natural x y f =
      D-lim.factors _ _ _ βˆ™ apβ‚‚ C._∘_ (C.eliml (F.F-id Ξ·β‚š _)) refl
    ml .commutes f = ext Ξ» j β†’
      C.pushr (C.introl (F.β‚€ _ .F-id)) βˆ™ D-lim.commutes j f
    ml .universal eps p .Ξ· x = D-lim.universal x
      (Ξ» j β†’ eps j .Ξ· x)
      (Ξ» f β†’ apβ‚‚ C._∘_ (C.elimr (F.β‚€ _ .F-id)) refl βˆ™ p f Ξ·β‚š x)
    ml .universal eps p .is-natural x y f = D-lim.uniqueβ‚‚ y _
      (Ξ» g β†’ C.pulll (apβ‚‚ C._∘_ (C.elimr (F.β‚€ _ .F-id)) refl βˆ™ p g Ξ·β‚š y))
      (Ξ» j β†’ C.pulll (D-lim.factors _ _ _))
      (Ξ» j β†’
          C.pulll (D-lim.factors _ _ _)
        βˆ™ C.pullr (D-lim.factors _ _ _)
        βˆ™ apβ‚‚ C._∘_ (C.eliml (F.F-id Ξ·β‚š _)) refl
        βˆ™ sym (eps j .is-natural x y f))
    ml .factors eps p = ext Ξ» j β†’
      D-lim.factors j _ _
    ml .unique eps p other q = ext Ξ» x β†’
      D-lim.unique _ _ _ _ Ξ» j β†’ q j Ξ·β‚š x

As a corollary, if is an category, then so is

Functor-cat-is-complete :
  βˆ€ {o β„“} {o₁ ℓ₁} {C : Precategory o₁ ℓ₁} {oβ‚‚ β„“β‚‚} {D : Precategory oβ‚‚ β„“β‚‚}
  β†’ is-complete o β„“ D β†’ is-complete o β„“ Cat[ C , D ]
Functor-cat-is-complete D-complete = functor-limit D-complete