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

# Ideaπ

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.

## Productsπ

**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 $P$ - and a family of maps from $P$ β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 **p**rojection. However, for an arbitrary cone, the
maps are.. well, arbitrary. To consider a concrete example, we can
pretend our diagram was in
${\mathrm{Set}}$
all along, and that
$A$
was the set
${\mathbb{Q}}$
and
$B$
was the set
${\mathbb{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
$P'$
and
$P$
were both apices for our original discrete diagram, we would draw a cone
homomorphism
$f : 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
$P$
to be a limit in our diagram above, we require that, for any other cone
$P'$
there exists a *unique* arrow
$P' \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 ${\mathrm{Sets}}$, the limit is the

*Cartesian product*of the objects of the diagram, and the arrows are the projections onto the factors.In ${\mathrm{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 $a \to b$ whenever $a \le b$.Normalising the definition of limit slightly, itβs works out to be an object $p$ such that $p \le a$ and $p \le b$, and if there are any other $p'$s satisfying that, then $p' \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
$({\mathbb{R}} \setminus {0}, \le)$
of real numbers except zero, with the usual ordering. Then the product
indexed by
$\{ x \in {\mathbb{R}} : x > 0 \}$
- which is normally
$0$
- 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 $A$, thereβs a unique arrow $A \to \top$.

# Constructionπ

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 private import Cat.Reasoning J as J import Cat.Reasoning C as C module F = Functor F record Cone : Type (oβ β oβ β hβ β hβ) where no-eta-equality

A Cone over $F$ 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β.

field apex : C.Ob Ο : (x : J.Ob) β C.Hom apex (F.β x)

For every map $f : 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) \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 $\psi$s 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 no-eta-equality

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 $o$ in the index category, the composition of hom with the domain coneβs Ο (at that object) must be equal to the codomainβs Ο.

field 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 = C.id ; 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 _ _ _)

## Limitsπ

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 (Terminal.top 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 : \mathcal{C} \to \mathcal{D}$ acts on a cone over ${\mathrm{Dia}}$ (in $\mathcal{C}$), sending it to a cone over $F \circ {\mathrm{Dia}}$ (in $\mathcal{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 $\mathcal{D}$.

F-map-cone-hom : {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 where 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
$L$
of
${\mathrm{Dia}}$
β which is, to reiterate, a terminal object in the category of cones
over
${\mathrm{Dia}}$.
We say that
$F$
*preserves
$L$*
if
$F(L)$,
as defined right above, is a terminal object in the category of cones
over
$F \circ {\mathrm{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
$\mathcal{D}$
will not, in general, possess an operation assigning a limit to every
diagram β therefore, there might not be a βcanonical limitβ of
$F\circ{\mathrm{Dia}}$
we could compare
$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
$\mathcal{D}$
of
$F \circ {\mathrm{Dia}}$
with apex
$F(a)$,
then
$a$
was *already the limit* of
${\mathrm{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
${\mathrm{Dia}}$
if it both preserves *and* reflects those limits. Intuitively,
this means that the limits of shape
${\mathrm{Dia}}$
in
$\mathcal{C}$
are in a 1-1 correspondence with the limits
$F \circ {\mathrm{Dia}}$
in
$\mathcal{D}$.

record Creates-limit (K : Cone Dia) : Type (oβ β hβ β oβ β hβ β oβ β hβ) where field preserves-limit : Preserves-limit K reflects-limit : Reflects-limit K

## Continuityπ

is-continuous : β {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

# Uniquenessπ

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
$F$,
suppose that
$X$
and
$Y$
are both limiting cones for for
$F$.

Limiting-cone-unique : (X Y : Limit F) β Terminal.top X Cones.β Terminal.top Y Limiting-cone-unique X Y = Cones.make-iso f g fβgβ‘id gβfβ‘id where X-cone = Terminal.top X Y-cone = Terminal.top Y

It follows from $Y$ (resp. $X$) being a terminal object that there is a unique cone homomorphism $f : X \to Y$ (resp $g : 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 $g$ is an inverse to $f$, consider the composition $g \circ f$ (the other case is symmetric): It is a map $g \circ f : X \to X$. Since $X$ is a terminal object, we have that the space of cone homomorphisms $X \to X$ is contractible - and thus any two such maps are equal. Thus, $g \circ f = {{\mathrm{id}}_{}}{X} : X \to X$.

fβgβ‘id : (f Cones.β g) β‘ Cones.id fβgβ‘id = Terminal.!-uniqueβ Y (f Cones.β g) Cones.id gβfβ‘id : (g Cones.β f) β‘ Cones.id gβfβ‘id = Terminal.!-uniqueβ X (g Cones.β f) Cones.id

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 c.to) (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} β Cones.is-invertible f β C.is-invertible (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 Cones.is-invertible f-invert Limit-unique : {X Y : Limit F} β Cone.apex (Terminal.top X) C.β Cone.apex (Terminal.top Y) Limit-unique {X} {Y} = Coneβ βapexβ (Limiting-cone-unique X Y)

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

apex-isoβis-limit : (K : Cone F) (L : Limit F) β C.is-invertible (Limit-universal F L K) β is-limit F K apex-isoβis-limit K L invert Kβ² = limits where module K = Cone K module Kβ² = Cone Kβ² module L = Cone (Terminal.top L) module universal {K} = Cone-hom (Terminal.! L {K}) open C.is-invertible 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 β

## Completenessπ

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 a poset. 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, \ell)$-complete**
if it has limits for any diagram indexed by a precategory with objects
in
${{\mathrm{Type}}}\ o$
and morphisms in
${{\mathrm{Type}}}\
\ell$.

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