open import Cat.Functor.Adjoint.Continuous
open import Cat.Instances.Functor.Duality
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Equaliser
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Diagram.Duals
open import Cat.Prelude

module Cat.Instances.Functor.Limits where

Limits in functor categoriesπŸ”—

Let C\ca{C} be a category admitting D\ca{D}-shaped limits. Then the functor category [E,S][\ca{E},\ca{S}], for E\ca{E} any category, also admits D\ca{D}-shaped limits. In particular, if C\ca{C} is (ΞΉ,ΞΊ)(\iota,\kappa)-complete, then so is [E,C][\ca{E},\ca{C}].

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 F:Dβ†’[E,C]F : \ca{D} \to [\ca{E},\ca{C}] be a diagram, and suppose C\ca{C} admits limits of D\ca{D}-shaped diagrams; We wish to compute the limit lim⁑F\lim F. First, observe that we can Uncurry FF to obtain a functor Fβ€²:DΓ—Eβ†’CF' : \ca{D} \times \ca{E} \to \ca{C}; By fixing the value of the E\ca{E} coordinate (say, to xx), we obtain a family F(βˆ’,x)F(-, x) of D\ca{D}-shaped diagrams in C\ca{C}, 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β€²

Let us call the limit of F(βˆ’,x)F(-, x) β€” taken in C\ca{C} β€” lim-for, and similarly the unique, β€œterminating” cone homomorphism Kβ†’lim⁑F(βˆ’,x)K \to \lim F(-, x) will be called !-for.

    lim-for : βˆ€ x β†’ _
    lim-for x = has-D-lims (Fβ€².Left x) .top

    !-for : βˆ€ {x} K β†’ _
    !-for {x} K = has-D-lims (Fβ€².Left x) .has⊀ K .centre

    !-for-unique : βˆ€ {x} {K} h β†’ !-for K ≑ h
    !-for-unique {x} {K} = has-D-lims (Fβ€².Left x) .has⊀ K .paths

The two fundamental β€” and very similar looking! β€” constructions are Lift-cone and map-cone below. Lift-cone lets us take a component of a cone for FF β€” in the functor category β€” into a cone for F(y)F(y), in C\ca{C}. Furthermore, at the same time as we perform this lifting, we can β€œadjust” the cone by a map (xβ†’fy)∈E(x \xto{f} y) \in \ca{E}.

  Lift-cone : βˆ€ {x y} (K : Cone F) (f : E.Hom x y) β†’ Cone (Fβ€².Left y)
  Lift-cone {x} {y} K f .apex = K .apex .Fβ‚€ x
  Lift-cone {x} {y} K f .ψ z  = Fβ€².second f C.∘ K .ψ z .Ξ· _
  Lift-cone {x} {y} K g .commutes f =
    Fβ€².first f C.∘ Fβ€².second g C.∘ K .ψ _ .Ξ· x β‰‘βŸ¨ C.extendl Fβ€².first∘second βŸ©β‰‘
    Fβ€².second g C.∘ Fβ€².first f C.∘ K .ψ _ .Ξ· x β‰‘βŸ¨ ap (Fβ€².second _ C.∘_) (apβ‚‚ C._∘_ (C.elimr (F-id (F.β‚€ _))) refl βˆ™ ap (Ξ» e β†’ e .Ξ· x) (K .commutes f)) βŸ©β‰‘
    Fβ€².second g C.∘ K .ψ _ .Ξ· x                ∎

The function map-cone is Lift-cone, but specialised to the case where K=lim⁑F(βˆ’,x)K = \lim F(-, x) is the lim-for a particular point in E\ca{E}.

  map-cone : βˆ€ {x y} (f : E.Hom x y) β†’ Cone (Fβ€².Left y)
  map-cone {x} f .apex       = lim-for x .apex
  map-cone {x} f .ψ z        = Fβ€².second f C.∘ lim-for x .ψ z
  map-cone {x} f .commutes g =
    Fβ€².first g C.∘ Fβ€².second f C.∘ lim-for x .ψ _ β‰‘βŸ¨ C.extendl Fβ€².first∘second βŸ©β‰‘
    Fβ€².second f C.∘ Fβ€².first g C.∘ lim-for x .ψ _ β‰‘βŸ¨ ap (Fβ€².second _ C.∘_) (lim-for x .commutes _) βŸ©β‰‘
    Fβ€².second f C.∘ lim-for x .ψ _                ∎

The coneπŸ”—

We are now ready to build a universal cone over FF, in the category [E,C][ \ca{E}, \ca{C} ], meaning the apex will be given by a functor A:Eβ†’CA : \ca{E} \to \ca{C}. Using the fact that C\ca{C} was assumed to have D\ca{D}-shaped limits, the-apex will be given by x↦lim⁑F(βˆ’,x)x \mapsto \lim F(-, x). Similarly, the choice of map is essentially unique: we must map lim⁑F(βˆ’,x)β†’lim⁑F(βˆ’,y)\lim F(-, x) \to \lim F(-, y), but the space of maps Xβ†’lim⁑F(βˆ’,y)X \to \lim F(-, y) is contractible.

  functor-cone : Cone F
  functor-cone .apex  = the-apex where
    the-apex : Functor E C
    the-apex .Fβ‚€ x = lim-for x .apex
    the-apex .F₁ {x} {y} f = !-for (map-cone f) .hom
We use that contractibility of mapping spaces to prove the-apex is actually a functor.
    the-apex .F-id = ap hom (!-for-unique map) where
      map : Cone-hom _ _ _
      map .hom = C.id
      map .commutes _ = C.idr _ βˆ™ C.introl Fβ€².second-id
    the-apex .F-∘ {x} {y} {z} f g = ap hom (!-for-unique map)
      where
        map : Cone-hom _ _ _
        map .hom = the-apex .F₁ f C.∘ the-apex .F₁ g
        map .commutes o =
          (lim-for z .ψ o C.∘ _ C.∘ _)                               β‰‘βŸ¨ C.extendl (!-for (map-cone f) .commutes _) βŸ©β‰‘
          (Fβ€².second f C.∘ lim-for y .ψ o C.∘ _)                     β‰‘βŸ¨ ap (Fβ€².second f C.∘_) (!-for (map-cone g) .commutes _) βŸ©β‰‘
          (Fβ€².second f C.∘ Fβ€².second g C.∘ lim-for x .ψ o)           β‰‘βŸ¨ C.pulll (sym Fβ€².second∘second) βŸ©β‰‘
          (Fβ€².second (f E.∘ g) C.∘ has-D-lims (Fβ€².Left x) .top .ψ o) ∎

We must now give the construction of the actual cone, i.e.Β the natural ψxβ€²\psi'_x transformations Aβ‡’F(x)A \To F(x). The natural transformations are defined componentwise by taking (ψxβ€²)y(\psi'_x)_y to be the map underlying the cone homomorphism ψx:(lim⁑F(βˆ’,y))β†’F(x)(y)\psi_x : (\lim F(-,y)) \to F(x)(y); This is natural because ψ\psi is a family of cone homomorphisms, and the cone commutes since each limiting cone lim⁑F(βˆ’,x)\lim F(-,x) is indeed a cone.

  functor-cone .ψ x .η y              = lim-for y .ψ x
  functor-cone .ψ x .is-natural y z f =
    !-for (map-cone f) .commutes _ βˆ™ apβ‚‚ C._∘_ (C.eliml (Ξ» i β†’ F.F-id i .Ξ· z)) refl
  functor-cone .commutes f = Nat-path Ξ» x β†’
      apβ‚‚ C._∘_ (C.intror (F-id (F.β‚€ _))) refl βˆ™ lim-for _ .commutes f

The mapsπŸ”—

For the functor-cone β€” our candidate for lim⁑F\lim F β€” to be limiting, we must, given some other cone KK, find a unique cone homomorphism Kβ†’lim⁑FK \to \lim F. We’ll be fine, though: We can (using Lift-cone) explode KK into a bunch of cones KxK_x, each lying over F(βˆ’,x)F(-,x), and use the universal property of lim⁑F(βˆ’,x)\lim F(-,x) to find cone homs Kxβ†’lim⁑F(βˆ’,x)K_x \to \lim F(-,x). Assuming these maps assemble to a natural transformation Kxβ†’lim⁑FK_x \to \lim F, we can show they commute with everything in sight:

  functor-! : βˆ€ K β†’ Cone-hom F K functor-cone
  functor-! K = ch where
    map : βˆ€ x β†’ Cone-hom (Fβ€².Left x) (Lift-cone K E.id) (lim-for x)
    map x = !-for (Lift-cone K E.id)

    ch : Cone-hom F K functor-cone
    ch .hom .Ξ· x = map _ .hom
    ch .commutes _ = Nat-path Ξ» x β†’ map _ .commutes _ βˆ™ C.eliml Fβ€².second-id

The hard part, then, is showing that this is a natural transformation. We’ll do this in a roundabout way: We’ll show that both composites in the naturality square inhabit the same contractible space of cone homomorphisms, namely that of Liftβˆ’cone(K,f)β†’lim⁑F(βˆ’,y)\id{Lift-cone}(K,f) \to \lim F(-,y), and thus conclude that they are unique. This isn’t too hard, but it is quite tedious:

    ch .hom .is-natural x y f =
      map y .hom C.∘ K .apex .F₁ f            β‰‘βŸ¨ (Ξ» i β†’ is-contrβ†’is-prop (has-D-lims (Fβ€².Left y) .has⊀ (Lift-cone K f)) h1 h2 i .hom) βŸ©β‰‘
      !-for (map-cone f) .hom C.∘ map x .hom  ∎
      where
        h1 : Cone-hom (Fβ€².Left y) (Lift-cone K f) (lim-for y)
        h1 .hom = map y .hom C.∘ K .apex .F₁ f
        h1 .commutes o =
          lim-for y .ψ o C.∘ map y .hom C.∘ K .apex .F₁ f  β‰‘βŸ¨ C.pulll (map y .commutes _ βˆ™ C.eliml Fβ€².second-id) βŸ©β‰‘
          K .ψ _ .Ξ· _ C.∘ K .apex .F₁ f                    β‰‘βŸ¨ K .ψ _ .is-natural _ _ _ βŸ©β‰‘
          F₁ (F.β‚€ o) f C.∘ K .ψ o .Ξ· x                     β‰‘βŸ¨ ap (C._∘ K .ψ o .Ξ· x) (C.introl (ap (Ξ» e β†’ e .Ξ· y) (F-id F))) βŸ©β‰‘
          Fβ€².second f C.∘ K .ψ o .Ξ· x                      ∎

        h2 : Cone-hom (Fβ€².Left y) (Lift-cone K f) (lim-for y)
        h2 .hom = has-D-lims (Fβ€².Left y) .has⊀ (map-cone f) .centre .hom C.∘ map x .hom
        h2 .commutes o =
          lim-for y .ψ o C.∘ !-for (map-cone f) .hom C.∘ map x .hom  β‰‘βŸ¨ C.pulll (has-D-lims (Fβ€².Left y) .has⊀ (map-cone f) .centre .commutes _) βŸ©β‰‘
          (Fβ€².second f C.∘ lim-for x .ψ o) C.∘ map x .hom            β‰‘βŸ¨ C.pullr (map x .commutes _ βˆ™ C.eliml Fβ€².second-id) βŸ©β‰‘
          Fβ€².second f C.∘ K .ψ o .Ξ· x                                ∎

Since we built the natural transformation underlying functor-! out of the unique maps !-for, we can appeal to that uniqueness here to conclude that functor-! is itself unique, showing that we put together a limit lim⁑F\lim F.

  functor-!-unique : βˆ€ {K} (h : Cone-hom F K functor-cone) β†’ functor-! K ≑ h
  functor-!-unique h = Cone-hom-path _ (Nat-path Ξ» x β†’ ap hom (!-for-unique hom'))
    where
      hom' : βˆ€ {x} β†’ Cone-hom (Fβ€².Left x) _ _
      hom' {x} .hom = h .hom .Ξ· x
      hom' {x} .commutes o = ap (Ξ» e β†’ e .Ξ· _) (h .commutes o) βˆ™ C.introl Fβ€².second-id

  functor-limit : Limit F
  functor-limit .top            = functor-cone
  functor-limit .has⊀ x .centre = functor-! x
  functor-limit .has⊀ x .paths  = functor-!-unique

As a corollary, if D\ca{D} is an (o,β„“)(o,\ell)-complete category, then so is [C,D][\ca{C},\ca{D}].

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