open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Diagram.Limit.Base where


The idea of limits generalises many concrete constructions in mathematics - from several settings, such as set theory, topology and algebra - to arbitrary categories. A limit, if it exists, is “the best solution” to an “equational problem”. For a first intuition, we can build them graphically, working directly “on top” of a diagram.


Note: Products are described explicitly in Cat.Diagram.Product. The description there might be easier to parse.

Consider a discrete diagram - one that has no interesting morphisms, only identities, such as the collection of objects below.

To consider a limit for this diagram, we first have to go through an intermediate step - a Cone. Draw a new object, the apex - let’s call it PP - and a family of maps from PP “down onto” all of the objects of the diagram. The new maps have to make everything in sight commute, but in the case of a discrete diagram, we can pick any maps. There are no obligations.

It’ll be helpful to think of the maps as projections - which is why they’re labelled with the greek letter π\pi, for projection. However, for an arbitrary cone, the maps are.. well, arbitrary. To consider a concrete example, we can pretend our diagram was in Set\id{Set} all along, and that AA was the set Q\bb{Q} and BB was the set R\bb{R}. Then the following is a cone over it:

Abstracting again, there is a canonical definition of cone homomorphism - A map between the apices that makes everything in sight commute. If PP' and PP were both apices for our original discrete diagram, we would draw a cone homomorphism f:PPf : P' \to P as the dashed arrow in following commutative Starfleet comms badge.

These assemble into a category, Cones, with composition and identity given by the composition and identity of ambient category. A Limit is, then, a terminal object in this category. For PP to be a limit in our diagram above, we require that, for any other cone PP' there exists a unique arrow PPP' \to P that makes everything commute.

The limit over a discrete diagram is called a product, and it’s important to note that the diagram need not be finite. Here are concrete examples of products in categories:

  • In Sets\id{Sets}, the limit is the Cartesian product of the objects of the diagram, and the arrows are the projections onto the factors.

  • In Top\id{Top}, the limit is the product space of the objects, and the arrows are projections, considered as continuous maps. The product topology can be defined as the coarsest topology that makes the projections continuous.

  • In a partially ordered set, considered as a category, the limit is the greatest lower bound of the objects - In a poset, we consider that there exists a map aba \to b whenever aba \le b.

    Normalising the definition of limit slightly, it’s works out to be an object pp such that pap \le a and pbp \le b, and if there are any other pp's satisfying that, then ppp' \le p.

This last example also demonstrates that, while we can always describe the limit over a diagram, it does not necessarily exist. Consider the poset (R0,)(\bb{R} \setminus {0}, \le) of real numbers except zero, with the usual ordering. Then the product indexed by {xR:x>0}\{ x \in \bb{R} : x > 0 \} - which is normally 00 - does not exist. Not every category has every limit. Some categories have no limits at all! If a category has every limit, it’s called complete.

Terminal objects🔗

Note: Terminal objects are described explicitly in Cat.Diagram.Terminal. The description there might be easier to parse.

Perhaps a simpler example of a limit is the one over the empty diagram. Since the empty diagram is discrete, what we’ll end up with is a kind of product - an empty product. A cone over the empty diagram is an object - the family of maps, indexed over the objects of the diagram, is empty.

In this case, a cone homomorphism works out to be a regular ol’ morphism, so the terminal object in the cone category is a terminal object in the ambient category: an object \top such that, for every other AA, there’s a unique arrow AA \to \top.


Cones are always considered over a diagram. Diagram just means “functor”, but it’s a concept with an attitude: Whereas, in general, functors can be a lot more involved than the name “diagram” would suggest, every functor can be considered a diagram! However, for the purpose of constructing limits, we generally work with functors out of “shapes”, tiny categories like \bullet \to \bullet \leftarrow \bullet.

module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} (F : Functor J C) where
    import Cat.Reasoning J as J
    import Cat.Reasoning C as C
    module F = Functor F

  record Cone : Type (o₁  o₂  h₁  h₂) where

A Cone over FF is given by an object (the apex) together with a family of maps ψ — one for each object in the indexing category J — such that “everything in sight commutes”.

      apex     : C.Ob
      ψ        : (x : J.Ob)  C.Hom apex (F.₀ x)

For every map f:xyf : x \to y in the indexing category, we require that the diagram below commutes. This encompasses “everything” since the only non-trivial composites that can be formed with the data at hand are of the form F(f)ψxF(f) \circ \psi_x.

      commutes :  {x y} (f : J.Hom x y)  F.₁ f C.∘ ψ x  ψ y

These non-trivial composites consist of following the left leg of the diagram below, followed by the bottom leg. For it to commute, that path has to be the same as following the right leg.

Since paths in Hom-spaces are propositions, to test equality of cones, it suffices for the apices to be equal, and for their ψ\psis to assign equal morphisms for every object in the shape category.

  Cone-path : {x y : Cone}
         (p : Cone.apex x  Cone.apex y)
         (∀ o  PathP  i  C.Hom (p i) (F.₀ o)) (Cone.ψ x o) (Cone.ψ y o))
         x  y
  Cone-path p q i .Cone.apex = p i
  Cone-path p q i .Cone.ψ o = q o i
  Cone-path {x = x} {y} p q i .Cone.commutes {x = a} {y = b} f =
    is-prop→pathp  i  C.Hom-set _ _ (F.₁ f C.∘ q a i) (q b i))
      (x .commutes f) (y .commutes f) i
    where open Cone

Cone maps🔗

  record Cone-hom (x y : Cone) : Type (o₁  h₂) where

A Cone homomorphism is – like the introduction says – a map hom in the ambient category between the apices, such that “everything in sight commutes”. Specifically, for any choice of object oo in the index category, the composition of hom with the domain cone’s ψ (at that object) must be equal to the codomain’s ψ.

      hom      : C.Hom (Cone.apex x) (Cone.apex y)
      commutes :  o  Cone.ψ y o C.∘ hom  Cone.ψ x o

Since cone homomorphisms are morphisms in the underlying category with extra properties, we can lift the laws from the underlying category to the category of Cones. The definition of compose is the enlightening part, since we have to prove that two cone homomorphisms again preserve all the commutativities.

  Cones : Precategory _ _
  Cones = cat where
    open Precategory

    compose : {x y z : _}  Cone-hom y z  Cone-hom x y  Cone-hom x z
    compose {x} {y} {z} F G = r where
      open Cone-hom
      r : Cone-hom x z
      r .hom = hom F C.∘ hom G
      r .commutes o =
        Cone.ψ z o C.∘ hom F C.∘ hom G ≡⟨ C.pulll (commutes F o) 
        Cone.ψ y o C.∘ hom G           ≡⟨ commutes G o 
        Cone.ψ x o                     

    cat : Precategory _ _
    cat .Ob = Cone
    cat .Hom = Cone-hom
    cat .id = record { hom = ; commutes = λ _  C.idr _ }
    cat ._∘_ = compose
    cat .idr f = Cone-hom-path (C.idr _)
    cat .idl f = Cone-hom-path (C.idl _)
    cat .assoc f g h = Cone-hom-path (C.assoc _ _ _)


At risk of repeating myself: A Limit is, then, a terminal object in this category.

  Limit : Type _
  Limit = Terminal Cones

  Limit-apex : Limit  C.Ob
  Limit-apex x = Cone.apex ( x)

  Limit-universal : (L : Limit)  (K : Cone)  C.Hom (Cone.apex K) (Limit-apex L)
  Limit-universal L K = Cone-hom.hom (Terminal.! L {K})

  is-limit : Cone  Type _
  is-limit K = is-terminal Cones K

Preservation of limits🔗

Since a cone is, in particular, a commutative diagram, and every functor preserves commutativity of diagrams, a functor F:CDF : \ca{C} \to \ca{D} acts on a cone over Dia\id{Dia} (in C\ca{C}), sending it to a cone over FDiaF \circ \id{Dia} (in D\ca{D}).

  F-map-cone : Cone Dia  Cone (F F∘ Dia)
  Cone.apex (F-map-cone x) = F₀ F (Cone.apex x)
  Cone.ψ (F-map-cone x) x₁ = F₁ F (Cone.ψ x x₁)
  Cone.commutes (F-map-cone x) {y = y} f =
    F.₁ (F₁ Dia f) D.∘ F.₁ (Cone.ψ x _)  ≡⟨ F.collapse (Cone.commutes x _) 
    F.₁ (Cone.ψ x y)                     

Note that this also lets us map morphisms between cones into D\ca{D}.

    : {X Y : Cone Dia}
     Cone-hom Dia X Y
     Cone-hom (F F∘ Dia) (F-map-cone X) (F-map-cone Y)
  F-map-cone-hom {X = X} {Y = Y} f = cone-hom
      module X = Cone X
      module Y = Cone Y
      module f = Cone-hom f

      cone-hom : Cone-hom (F F∘ Dia) (F-map-cone X) (F-map-cone Y)
      cone-hom .Cone-hom.hom = F .F₁ f.hom
      cone-hom .Cone-hom.commutes _ =
        F .F₁ (Y.ψ _) D.∘ (F .F₁ f.hom) ≡⟨ F.collapse (f .Cone-hom.commutes _) 
        F .F₁ (X.ψ _)                   

Suppose you have a limit LL of Dia\id{Dia} — which is, to reiterate, a terminal object in the category of cones over Dia\id{Dia}. We say that FF preserves LL if F(L)F(L), as defined right above, is a terminal object in the category of cones over FDiaF \circ \id{Dia}.

  Preserves-limit : Cone Dia  Type _
  Preserves-limit K = is-limit Dia K  is-limit (F F∘ Dia) (F-map-cone K)

This definition is necessary because D\ca{D} will not, in general, possess an operation assigning a limit to every diagram — therefore, there might not be a “canonical limit” of FDiaF\circ\id{Dia} we could compare F(L)F(L) to. However, since limits are described by a universal property (in particular, being terminal), we don’t need such an object! Any limit is as good as any other.

In more concise terms, we say a functor preserves limits if it takes limiting cones “upstairs” to limiting cones “downstairs”.

Reflection of limits🔗

Using our analogy from before, we say a functor reflects limits if it takes limiting cones “downstairs” to limiting cones “upstairs”.

More concretely, if we have some limiting cone in D\ca{D} of FDiaF \circ \id{Dia} with apex F(a)F(a), then aa was already the limit of Dia\id{Dia}!

  Reflects-limit : Cone Dia  Type _
  Reflects-limit K = is-limit (F F∘ Dia) (F-map-cone K)  is-limit Dia K

Creation of limits🔗

Finally, we say a functor creates limits of shape Dia\id{Dia} if it both preserves and reflects those limits. Intuitively, this means that the limits of shape Dia\id{Dia} in C\ca{C} are in a 1-1 correspondence with the limits FidDiaF \circ id{Dia} in D\ca{D}.

  record Creates-limit (K : Cone Dia) : Type (o₁  h₁  o₂  h₂  o₃  h₃) where
      preserves-limit : Preserves-limit K
      reflects-limit : Reflects-limit K


  :  {oshape hshape}
      {C : Precategory o₁ h₁}
      {D : Precategory o₂ h₂}
   Functor C D  Type _

A continuous functor is one that — for every shape of diagram J, and every diagram diagram of shape J in C — preserves the limit for that diagram.

is-continuous {oshape = oshape} {hshape} {C = C} F =
   {J : Precategory oshape hshape} {diagram : Functor J C}
   (K : Cone diagram)  Preserves-limit F K


Above, there has been mention of the limit. The limit of a diagram, if it exists, is unique up to isomorphism. We prove that here. The argument is as follows: Fixing a diagram FF, suppose that XX and YY are both limiting cones for for FF.

    : (X Y : Limit F) X Cones.≅ Y
  Limiting-cone-unique X Y = Cones.make-iso f g f∘g≡id g∘f≡id where
    X-cone = X
    Y-cone = Y

It follows from YY (resp. XX) being a terminal object that there is a unique cone homomorphism f:XYf : X \to Y (resp g:YXg : Y \to X).

    f : Cones.Hom X-cone Y-cone
    f = Terminal.! Y {X-cone}

    g : Cones.Hom Y-cone X-cone
    g = Terminal.! X {Y-cone}

To show that gg is an inverse to ff, consider the composition gfg \circ f (the other case is symmetric): It is a map gf:XXg \circ f : X \to X. Since XX is a terminal object, we have that the space of cone homomorphisms XXX \to X is contractible - and thus any two such maps are equal. Thus, gf=idX:XXg \circ f = \id{id}_{X} : X \to X.

    f∘g≡id : (f Cones.∘ g)
    f∘g≡id = Terminal.!-unique₂ Y (f Cones.∘ g)

    g∘f≡id : (g Cones.∘ f)
    g∘f≡id = Terminal.!-unique₂ X (g Cones.∘ f)

There is an evident functor from Cones to C, which sends cones to their apices and cone homomorphisms to their underlying maps. Being a functor, it preserves isomorphisms, so we get an isomorphism of the limit objects from the isomorphism of limit cones.

Contrary to the paragraph above, though, rather than defining a functor, there is a direct proof that an isomorphism of limits results in an isomorphism of apices. Fortunately, the direct proof Cone≅→apex≅ is exactly what one would get had they defined the functor and used the proof that it preserves isomorphisms.

  Cone≅→apex≅ : {X Y : Cone F}
               X Cones.≅ Y
               (Cone.apex X) C.≅ (Cone.apex Y)
  Cone≅→apex≅ c =
    C.make-iso (Cone-hom.hom (Cone-hom.hom c.from)
      (ap Cone-hom.hom c.invl)
      (ap Cone-hom.hom c.invr)
    where module c = Cones._≅_ c

  Cone-invertible→apex-invertible : {X Y : Cone F} {f : Cones.Hom X Y}
                          (Cone-hom.hom f)
  Cone-invertible→apex-invertible {f = f} f-invert =
    C.make-invertible (Cone-hom.hom inv) (ap Cone-hom.hom invl) (ap Cone-hom.hom invr)
    where open f-invert

    : {X Y : Limit F}
     Cone.apex ( X) C.≅ Cone.apex ( Y)
  Limit-unique {X} {Y} = Cone≅→apex≅ (Limiting-cone-unique X Y)

If the universal map KLK \to L between apexes of some limit is invertible, then that means that KK is also a limiting cone.

    : (K : Cone F)
      (L : Limit F) (Limit-universal F L K)
       is-limit F K
  apex-iso→is-limit K L invert K′ = limits
      module K = Cone K
      module K′ = Cone K′
      module L = Cone ( L)
      module universal {K} = Cone-hom (Terminal.! L {K})
      open invert

      limits : is-contr (Cones.Hom K′ K)
      limits .centre .Cone-hom.hom = inv C.∘ Limit-universal F L K′
      limits .centre .Cone-hom.commutes _ =
        (K.ψ _) C.∘ (inv C.∘ universal.hom)                   ≡˘⟨ ap ( C._∘ (inv C.∘ universal.hom)) (universal.commutes _) ≡˘
        (L.ψ _ C.∘ universal.hom) C.∘ (inv C.∘ universal.hom) ≡⟨ C.cancel-inner invl 
        L.ψ _ C.∘ universal.hom                               ≡⟨ universal.commutes _ 
        K′.ψ _                                                
      limits .paths f = Cone-hom-path F $ C.invertible→monic invert _ _ $
        universal.hom C.∘ (inv C.∘ universal.hom) ≡⟨ C.cancell invl 
        universal.hom                             ≡⟨ ap Cone-hom.hom (Terminal.!-unique L (Terminal.! L Cones.∘ f)) 
        universal.hom C.∘ Cone-hom.hom f          


A category is complete if admits for limits of arbitrary shape. However, in the presence of excluded middle, if a category admits products indexed by its class of morphisms, then it is automatically thin. Since excluded middle is independent of type theory, we can not prove that any non-thin categories have arbitrary limits.

Instead, categories are complete with respect to a pair of universes: A category is (o,)(o, \ell)-complete if it has limits for any diagram indexed by a precategory with objects in Type o\ty\ o and morphisms in Type \ty\ \ell.

is-complete :  {oc ℓc} o   Precategory oc ℓc  Type _
is-complete o  C =  {D : Precategory o } (F : Functor D C)  Limit F