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.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Closed
open import Cat.Diagram.Duals
open import Cat.Prelude

module Cat.Instances.Functor.Limits where

Limits in functor categories🔗

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

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

  open Functor
  open _=>_

  import Cat.Reasoning C as C
  import Cat.Reasoning D as D
  import Cat.Reasoning E as E

  private
    module F = Functor F

Let $F:\mathcal{D}\to [\mathcal{E},\mathcal{C}]$ be a diagram, and suppose $\mathcal{C}$ admits limits of $\mathcal{D}\text{-shaped}$ diagrams; We wish to compute the limit $\lim F\text{.}$ First, observe that we can Uncurry $F$ to obtain a functor $F^{\prime }:\mathcal{D}\times \mathcal{E}\to \mathcal{C}\text{;}$ By fixing the value of the $\mathcal{E}$ coordinate (say, to $x\text{),}$ we obtain a family $F(-,x)$ of $\mathcal{D}\text{-shaped}$ diagrams in $\mathcal{C}\text{,}$ 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 $F(-,x)$ — taken in $\mathcal{C}$ — lim-for, and similarly the unique, “terminating” cone homomorphism $K\to \lim F(-,x)$ 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 eta p .η x = D-lim.universal x
      (λ j → eta j .η x)
      (λ f → ap₂ C._∘_ (C.elimr (F.₀ _ .F-id)) refl ∙ p f ηₚ x)
    ml .universal eta 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 (eta j .is-natural x y f))
    ml .factors eta p = ext λ j →
      D-lim.factors j _ _
    ml .unique eta p other q = ext λ x →
      D-lim.unique _ _ _ _ λ j → q j ηₚ x

As a corollary, if $\mathcal{D}$ is an $(o,\ell )\text{-complete}$ category, then so is $[\mathcal{C},\mathcal{D}]\text{.}$

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

module _
  {o₁ ℓ₁} {C : Precategory o₁ ℓ₁}
  {o₂ ℓ₂} {D : Precategory o₂ ℓ₂}
  {o₃ ℓ₃} {E : Precategory o₃ ℓ₃}
  (has-D-colims : ∀ (F : Functor D C) → Colimit F)
  (F : Functor D Cat[ E , C ])
  where

  functor-colimit : Colimit F
  functor-colimit = colim where
    F' : Functor (D ^op) Cat[ E ^op , C ^op ]
    F' = op-functor→ F∘ Functor.op F

    F'-lim : Limit F'
    F'-lim = functor-limit
      (λ f → subst Limit F^op^op≡F (Colimit→Co-limit (has-D-colims (Functor.op f))))
      F'

    LF'' : Limit (op-functor← {C = E} {D = C} F∘ (op-functor→ F∘ Functor.op F))
    LF'' = right-adjoint-limit (is-equivalence.F⊣F⁻¹ op-functor-is-equiv) F'-lim

    LFop : Limit (Functor.op F)
    LFop = subst Limit (F∘-assoc ∙ ap (_F∘ Functor.op F) op-functor←→ ∙ F∘-idl) LF''

    colim : Colimit F
    colim = Co-limit→Colimit LFop

Functor-cat-is-cocomplete :
  ∀ {o ℓ} {o₁ ℓ₁} {C : Precategory o₁ ℓ₁} {o₂ ℓ₂} {D : Precategory o₂ ℓ₂}
  → is-cocomplete o ℓ D → is-cocomplete o ℓ Cat[ C , D ]
Functor-cat-is-cocomplete D-cocomplete = functor-colimit D-cocomplete