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 ])

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 limF\lim F. First, observe that we can Uncurry FF to obtain a functor F:D×ECF' : \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 ×Cat 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 KlimF(,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 (xfy)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=limF(,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:ECA : \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 xlimF(,x)x \mapsto \lim F(-, x). Similarly, the choice of map is essentially unique: we must map limF(,x)limF(,y)\lim F(-, x) \to \lim F(-, y), but the space of maps XlimF(,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 =
      map .commutes _ = C.idr _  C.introl F′.second-id
    the-apex .F-∘ {x} {y} {z} f g = ap hom (!-for-unique map)
        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 AF(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:(limF(,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 limF(,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 limF\lim F — to be limiting, we must, given some other cone KK, find a unique cone homomorphism KlimFK \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 limF(,x)\lim F(-,x) to find cone homs KxlimF(,x)K_x \to \lim F(-,x). Assuming these maps assemble to a natural transformation KxlimFK_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 (lim-for x)
    map x = !-for (Lift-cone K

    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 Liftcone(K,f)limF(,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  
        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 limF\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'))
      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
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 ])

  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))))

    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