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

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

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