open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Shape.Interval
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Coherence
open import Cat.Instances.Functor
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Prelude

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

module Cat.Diagram.Colimit.Base where

private variable
o β o' β' : Level


# Colimitsπ

## Ideaπ

Colimits are dual to limits; much like their duals, they generalize constructions in several settings to arbitrary categories. A colimit (if it exists), is the βbest solutionβ to an βidentification problemβ. This is in contrast to the limit, which acts as a solution to an βequational problemβ.

Therefore, we define colimits in a similar way to limits. the only difference being that we define the colimit of a diagram as a left Kan extension instead of a right Kan extension. This gives us the expected βmapping outβ universal property, as opposed to the βmapping inβ property associated to limits.

Note that approach to colimits is not what normally presented in introductory material. Instead, most books opt to define colimits via cocones, as they are less abstract, though harder to work with in the long run.

private variable
oβ oβ oβ hβ hβ hβ : Level

module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} (Diagram : Functor J C) where
private
module C = Precategory C

is-colimit : (x : C.Ob) β Diagram => Const x β Type _
is-colimit x cocone =
is-lan !F Diagram (!Const x) cocone

Colimit : Type _
Colimit = Lan !F Diagram


## Concretelyπ

As mentioned, our definition is very abstract, meaning we can directly re-use definitions and theorems about Kan extensions in the setting of colimits. The trade-off is that while working with colimits in general is easier, working with specific colimits becomes more difficult, as the data we actually care about has been obfuscated.

One particularly egregious failure isβ¦ actually constructing colimits. The definition in terms of Lan hides the concrete data behind a few abstractions, which would be very tedious to write out each time. To work around this, we provide an auxiliary record type, make-is-colimit, as an intermediate step in constructing left extensions.

module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ}
where
private
module J = Precategory J
module C = Cat.Reasoning C

record make-is-colimit
(Diagram : Functor J C) (coapex : C.Ob)
: Type (oβ β hβ β oβ β hβ)
where
no-eta-equality
open Functor Diagram


First, we require morphisms from the every value of the diagram to the coapex; taken as a family, we call it Moreover, if is a morphism in the βshapeβ category we require which encodes the relevant naturality.

    field
Ο : (j : J.Ob) β C.Hom (Fβ j) coapex
commutes : β {x y} (f : J.Hom x y) β Ο y C.β Fβ f β‘ Ο x


The rest of the data ensures that is the universal family of maps with this property; if is another natural family, then each factors through the coapex by a unique universal morphism:

      universal
: β {x : C.Ob}
β (eta : β j β C.Hom (Fβ j) x)
β (β {x y} (f : J.Hom x y) β eta y C.β Fβ f β‘ eta x)
β C.Hom coapex x
factors
: β {j : J.Ob} {x : C.Ob}
β (eta : β j β C.Hom (Fβ j) x)
β (p : β {x y} (f : J.Hom x y) β eta y C.β Fβ f β‘ eta x)
β universal eta p C.β Ο j β‘ eta j
unique
: β {x : C.Ob}
β (eta : β j β C.Hom (Fβ j) x)
β (p : β {x y} (f : J.Hom x y) β eta y C.β Fβ f β‘ eta x)
β (other : C.Hom coapex x)
β (β j β other C.β Ο j β‘ eta j)
β other β‘ universal eta p

    uniqueβ
: β {x : C.Ob}
β (eta : β j β C.Hom (Fβ j) x)
β (p : β {x y} (f : J.Hom x y) β eta y C.β Fβ f β‘ eta x)
β β {o1} β (β j β o1 C.β Ο j β‘ eta j)
β β {o2} β (β j β o2 C.β Ο j β‘ eta j)
β o1 β‘ o2
uniqueβ eta p q r = unique eta p _ q β sym (unique eta p _ r)


Once we have this data, we can use it to construct a value of type is-colimit. The naturality condition we required above may seem too weak, but the full naturality condition can be derived from it and the rest of the data.

  open _=>_

to-cocone
: β {D : Functor J C} {coapex}
β make-is-colimit D coapex
β D => Const coapex
to-cocone ml .Ξ· = ml .make-is-colimit.Ο
to-cocone ml .is-natural x y f = (ml .make-is-colimit.commutes f) β sym (C.idl _)

  to-is-colimit
: β {Diagram : Functor J C} {coapex}
β (mc : make-is-colimit Diagram coapex)
β is-colimit Diagram coapex (to-cocone mc)
to-is-colimit {Diagram} {coapex} mkcolim = colim where
open make-is-colimit mkcolim
open is-lan
open Functor

colim : is-colimit Diagram coapex (to-cocone mkcolim)
colim .Ο {M = M} Ξ± .Ξ· _ =
universal (Ξ± .Ξ·) (Ξ» f β Ξ± .is-natural _ _ f β C.eliml (M .F-id))
colim .Ο {M = M} Ξ± .is-natural _ _ _ = C.idr _ β C.introl (M .F-id)
colim .Ο-comm {Ξ± = Ξ±} = ext Ξ» j β factors (Ξ± .Ξ·) _
colim .Ο-uniq {Ξ± = Ξ±} {Ο' = Ο'} p = ext Ξ» _ β
sym $unique (Ξ± .Ξ·) _ (Ο' .Ξ· _) (Ξ» j β sym (p Ξ·β j))   -- We often find ourselves working with something that isn't a colimit -- on the nose due to some annoying extensionality reasons involving -- functors 'β€Cat β C' -- We could use some general theorems of Kan extensions to adjust the -- colimit, but this has better definitional behaviour. generalize-colimitp : β {D : Functor J C} {K : Functor β€Cat C} β {eta : D => (Const (Functor.Fβ K tt))} {eta' : D => K Fβ !F} β is-lan !F D (!Const (Functor.Fβ K tt)) eta β (β {j} β eta .Ξ· j β‘ eta' .Ξ· j) β is-lan !F D K eta' generalize-colimitp {D} {K} {eta} {eta'} lan q = lan' where module lan = is-lan lan open is-lan open Functor lan' : is-lan !F D K eta' lan' .Ο Ξ± = !constβΏ (lan.Ο Ξ± .Ξ· tt) lan' .Ο-comm {M} {Ξ±} = ext Ξ» j β ap (_ C.β_) (sym q) β lan.Ο-comm {Ξ± = Ξ±} Ξ·β _ lan' .Ο-uniq {M} {Ξ±} {Ο'} r = ext Ξ» j β lan.Ο-uniq {Ο' = !constβΏ (Ο' .Ξ· tt)} (ext Ξ» j β r Ξ·β j β ap (_ C.β_) (sym q)) Ξ·β j to-is-colimitp : β {D : Functor J C} {K : Functor β€Cat C} {eta : D => K Fβ !F} β (mk : make-is-colimit D (K # tt)) β (β {j} β to-cocone mk .Ξ· j β‘ eta .Ξ· j) β is-lan !F D K eta to-is-colimitp {D} {K} {eta} mkcolim p = generalize-colimitp (to-is-colimit mkcolim) p  The concrete interface of make-is-colimit is also handy for consuming specific colimits. To enable this use case, we provide a function which unmakes a colimit.  unmake-colimit : β {D : Functor J C} {F : Functor β€Cat C} {eta} β is-lan !F D F eta β make-is-colimit D (Functor.Fβ F tt) unmake-colimit {D} {F} {eta} colim = mc module unmake-colimit where coapex = Functor.Fβ F tt module eta = _=>_ eta open is-lan colim open Functor D open make-is-colimit open _=>_ module _ {x} (eta : β j β C.Hom (Fβ j) x) (p : β {x y} (f : J.Hom x y) β eta y C.β Fβ f β‘ eta x) where eta-nt : D => Const x eta-nt .Ξ· = eta eta-nt .is-natural _ _ f = p f β sym (C.idl _) hom : C.Hom coapex x hom = Ο {M = !Const x} eta-nt .Ξ· tt mc : make-is-colimit D coapex mc .Ο = eta.Ξ· mc .commutes f = eta.is-natural _ _ f β C.eliml (F .Functor.F-id) mc .universal = hom mc .factors e p = Ο-comm {Ξ± = eta-nt e p} Ξ·β _ mc .unique {x = x} eta p other q = sym$ Ο-uniq {Ο' = other-nt} (ext Ξ» j β sym (q j)) Ξ·β tt
where
other-nt : F => !Const x
other-nt .Ξ· _ = other
other-nt .is-natural _ _ _ = C.elimr (F .Functor.F-id) β sym (C.idl _)

  to-colimit
: β {D : Functor J C} {K : Functor β€Cat C} {eta : D => K Fβ !F}
β is-lan !F D K eta
β Colimit D
to-colimit c .Lan.Ext = _
to-colimit c .Lan.eta = _
to-colimit c .Lan.has-lan = c

module is-colimit
{J : Precategory oβ hβ} {C : Precategory oβ hβ}
{D : Functor J C} {F : Functor β€Cat C} {eta : D => F Fβ !F}
(t : is-lan !F D F eta)
where

open make-is-colimit (unmake-colimit {F = F} t) public


We also provide a similar interface for the bundled form of colimits.

module Colimit
{J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} (L : Colimit D)
where

  private
import Cat.Reasoning J as J
import Cat.Reasoning C as C
module Diagram = Functor D
open Functor
open _=>_

open Lan L public


The coapex of the colimit can be obtained by applying the extension functor to the single object of β€Cat.

  coapex : C.Ob
coapex = Ext .Fβ tt


Furthermore, we can show that the apex is the colimit, in the sense of is-colimit, of the diagram. Youβd think this is immediate, but unfortunately, proof assistants: is-colimit asks for the constant functor functor with value coapex to be a Kan extension, but Colimit, being an instance of Lan, packages an arbitrary functor

Since Agda does not compare functors for we have to shuffle our data around manually. Fortunately, this isnβt a very long computation.

  cocone : D => Const coapex
cocone .Ξ· = eta .Ξ·
cocone .is-natural x y f =
eta .is-natural x y f β ap (C._β _) (Ext .F-id)

has-colimit : is-colimit D coapex cocone
has-colimit .is-lan.Ο Ξ± .Ξ· = Ο Ξ± .Ξ·
has-colimit .is-lan.Ο Ξ± .is-natural x y f =
ap (_ C.β_) (sym (Ext .F-id)) β Ο Ξ± .is-natural tt tt tt
has-colimit .is-lan.Ο-comm = ext (Ο-comm Ξ·β_)
has-colimit .is-lan.Ο-uniq {M = M} {Ο' = Ο'} p =
ext (Ξ» _ β Ο-uniq {Ο' = nt} (reext! p) Ξ·β _)
where
nt : Ext => M
nt .Ξ· = Ο' .Ξ·
nt .is-natural x y f = ap (_ C.β_) (Ext .F-id) β Ο' .is-natural x y f

open is-colimit has-colimit public


# Uniquenessπ

Much like limits, colimits are unique up to isomorphism. This all follows from general properties of Kan extensions, combined with the fact that natural isomorphisms between functors correspond with isomorphisms in

module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ}
{Diagram : Functor J C}
{x y} {etay : Diagram => Const y} {etax : Diagram => Const x}
(Cy : is-colimit Diagram y etay)
(Cx : is-colimit Diagram x etax)
where
private
module J = Precategory J
module C = Cat.Reasoning C
module Diagram = Functor Diagram
open is-lan
open _=>_

module Cy = is-colimit Cy
module Cx = is-colimit Cx

  colimitsβinversesp
: β {f : C.Hom x y} {g : C.Hom y x}
β (β {j : J.Ob} β f C.β Cx.Ο j β‘ Cy.Ο j)
β (β {j : J.Ob} β g C.β Cy.Ο j β‘ Cx.Ο j)
β C.Inverses f g

colimitsβinvertiblep
: β {f : C.Hom x y}
β (β {j : J.Ob} β f C.β Cx.Ο j β‘ Cy.Ο j)
β C.is-invertible f

colimits-unique     : x C.β y
colimitsβinvertible : C.is-invertible (Cx.universal Cy.Ο Cy.commutes)
colimitsβinverses
: C.Inverses (Cx.universal Cy.Ο Cy.commutes) (Cy.universal Cx.Ο Cx.commutes)

  colimitsβinversesp {f = f} {g = g} f-factor g-factor =
inversesβΏβinverses {Ξ± = !constβΏ f} {Ξ² = !constβΏ g}
(Lan-unique.Ο-inversesp Cx Cy
(ext Ξ» j β f-factor {j})
(ext Ξ» j β g-factor {j}))
tt

colimitsβinvertiblep {f = f} f-factor =
is-invertibleβΏβis-invertible {Ξ± = !constβΏ f}
(Lan-unique.Ο-is-invertiblep
Cx Cy (ext Ξ» j β f-factor {j}))
tt

colimitsβinverses =
colimitsβinversesp (Cx.factors Cy.Ο Cy.commutes) (Cy.factors Cx.Ο Cx.commutes)

colimitsβinvertible =
colimitsβinvertiblep (Cx.factors Cy.Ο Cy.commutes)

colimits-unique = isoβΏβiso (Lan-unique.unique Cx Cy) tt


Furthermore, if the universal map is invertible, then that means its domain is also a colimit of the diagram. This also follows from a general theorem of Kan extensions, though some golfing is required to obtain the correct inverse definitionally.

module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ}
{D : Functor J C} {K : Functor β€Cat C}
{etay : D => Const (Functor.Fβ K tt)}
(Cy : is-colimit D (Functor.Fβ K tt) etay)
where
private
module J = Precategory J
module C = Cat.Reasoning C
module D = Functor D
open is-ran
open Functor
open _=>_

module Cy = is-colimit Cy

familyβcocone
: β {x}
β (eta : β j β C.Hom (D.β j) x)
β (β {x y} (f : J.Hom x y) β eta y C.β D.β f β‘ eta x)
β D => Const x
familyβcocone eta p .Ξ· = eta
familyβcocone eta p .is-natural _ _ _ = p _ β sym (C.idl _)

  is-invertibleβis-colimitp
: β {K' : Functor β€Cat C} {eta : D => K' Fβ !F}
β (eta' : β j β C.Hom (D.β j) (K' .Fβ tt))
β (p : β {x y} (f : J.Hom x y) β eta' y C.β D.β f β‘ eta' x)
β (β {j} β eta' j β‘ eta .Ξ· j)
β C.is-invertible (Cy.universal eta' p)
β is-lan !F D K' eta
is-invertibleβis-colimitp {K' = K'} {eta = eta} eta' p q invert =
generalize-colimitp
(is-invertibleβis-lan Cy $invertibleβinvertibleβΏ _ Ξ» _ β invert) q  Another useful fact is that if is a colimit of some diagram and is naturally isomorphic to some other diagram then the coapex of is also a colimit of  natural-iso-diagramβis-colimitp : β {D' : Functor J C} {eta : D' => K Fβ !F} β (isos : D β βΏ D') β (β {j} β Cy.Ο j C.β IsoβΏ.from isos .Ξ· j β‘ eta .Ξ· j) β is-lan !F D' K eta natural-iso-diagramβis-colimitp {D' = D'} isos q = generalize-colimitp (natural-iso-ofβis-lan Cy isos) q  module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D D' : Functor J C} where natural-isoβcolimit : D β βΏ D' β Colimit D β Colimit D' natural-isoβcolimit isos C .Lan.Ext = Lan.Ext C natural-isoβcolimit isos C .Lan.eta = Lan.eta C βnt IsoβΏ.from isos natural-isoβcolimit isos C .Lan.has-lan = natural-iso-ofβis-lan (Lan.has-lan C) isos  module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} {x} {eta : Diagram => Const x} where private module J = Precategory J module C = Cat.Reasoning C module Diagram = Functor Diagram open is-lan open _=>_ is-colimit-is-prop : is-prop (is-colimit Diagram x eta) is-colimit-is-prop = is-lan-is-prop  Since is-colimit is a proposition, and the colimiting cocones are all unique (βup to isomorphismβ), if weβre talking about univalent categories, then Colimit itself is a proposition. This is also an instance of the more general uniqueness of Kan extensions. module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} where   Colimit-is-prop : is-category C β is-prop (Colimit Diagram) Colimit-is-prop cat = Lan-is-prop cat  # Preservation and reflection of colimitsπ The definitions here are the same idea as preservation of limits, just dualised. module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) (Diagram : Functor J C) where   preserves-colimit : Type _ preserves-colimit = β {K : Functor β€Cat C} {eta : Diagram => K Fβ !F} β (colim : is-lan !F Diagram K eta) β preserves-lan F colim reflects-colimit : Type _ reflects-colimit = β {K : Functor β€Cat C} {eta : Diagram => K Fβ !F} β (lan : is-lan !F (F Fβ Diagram) (F Fβ K) (nat-assoc-to (F βΈ eta))) β reflects-lan F lan  module preserves-colimit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F : Functor C D} {Dia : Functor J C} (preserves : preserves-colimit F Dia) where private module D = Precategory D module C = Precategory C module J = Precategory J module F = Func F module Dia = Func Dia universal : {x : C.Ob} β {K : Functor β€Cat C} {eta : Dia => K Fβ !F} β {eta' : (j : J.Ob) β C.Hom (Dia.Fβ j) x} β {p : β {i j} (f : J.Hom i j) β eta' j C.β Dia.Fβ f β‘ eta' i} β (colim : is-lan !F Dia K eta) β F.Fβ (is-colimit.universal colim eta' p) β‘ is-colimit.universal (preserves colim) (Ξ» j β F.Fβ (eta' j)) (Ξ» f β F.collapse (p f)) universal colim = is-colimit.unique (preserves colim) _ _ _ (Ξ» j β F.collapse (is-colimit.factors colim _ _)) colimit : Colimit Dia β Colimit (F Fβ Dia) colimit colim = to-colimit (preserves (Colimit.has-colimit colim)) module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F F' : Functor C D} {Dia : Functor J C} where private module D = Cat.Reasoning D open Func open _=>_ natural-isoβpreserves-colimits : F β βΏ F' β preserves-colimit F Dia β preserves-colimit F' Dia natural-isoβpreserves-colimits Ξ± F-preserves {K = K} {eta} colim = natural-isosβis-lan idni (Ξ± βni Dia) (Ξ± βni K) (ext Ξ» j β β F' .Fβ (K .Fβ tt) D.β Ξ±.to .Ξ· _ β D.β (F .Fβ (eta .Ξ· j) D.β Ξ±.from .Ξ· _) β‘β¨ ap! (eliml F' (K .F-id)) β©β‘ Ξ±.to .Ξ· _ D.β (F .Fβ (eta .Ξ· j) D.β Ξ±.from .Ξ· _) β‘β¨ D.pushr (sym (Ξ±.from .is-natural _ _ _)) β©β‘ ((Ξ±.to .Ξ· _ D.β Ξ±.from .Ξ· _) D.β F' .Fβ (eta .Ξ· j)) β‘β¨ D.eliml (Ξ±.invl Ξ·β _) β©β‘ F' .Fβ (eta .Ξ· j) β) (F-preserves colim) where module Ξ± = IsoβΏ Ξ±  ## Cocontinuityπ is-cocontinuous : β (oshape hshape : Level) {C : Precategory oβ hβ} {D : Precategory oβ hβ} β Functor C D β Type _  A cocontinuous functor is one that, for every shape of diagram J, and every diagram diagram of shape J in C, preserves the colimit for that diagram. is-cocontinuous oshape hshape {C = C} F = β {J : Precategory oshape hshape} {Diagram : Functor J C} β preserves-colimit F Diagram  # Cocompletenessπ A category is cocomplete if it admits colimits for diagrams of arbitrary shape. However, in the presence of excluded middle, if a category admits coproducts 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 colimits. Instead, categories are cocomplete with respect to a pair of universes: A category is if it has colimits for any diagram indexed by a precategory with objects in and morphisms in is-cocomplete : β {oc βc} o β β Precategory oc βc β Type _ is-cocomplete oj βj C = β {J : Precategory oj βj} (F : Functor J C) β Colimit F  While this condition might sound very strong, and thus that it would be hard to come by, it turns out we can get away with only two fundamental types of colimits: coproducts and coequalisers. In order to construct the colimit for a diagram of shape we will require coproducts indexed by type of objects and by its type of morphisms. module _ {o β} {C : Precategory o β} where private module C = Cat.Reasoning C open Indexed-coproduct open make-is-colimit open Coequaliser   colimit-as-coequaliser-of-coproduct : β {oj βj} {J : Precategory oj βj} β has-coproducts-indexed-by C β J β β has-coproducts-indexed-by C (Arrows J) β has-coequalisers C β (F : Functor J C) β Colimit F colimit-as-coequaliser-of-coproduct {oj} {βj} {J} has-Ob-cop has-Arrows-cop has-coeq F = to-colimit (to-is-colimit colim) where   module J = Cat.Reasoning J open Functor F  Given a diagram we start by building the coproduct of all the objects appearing in the diagram.  Obs : Indexed-coproduct C Ξ» o β Fβ o Obs = has-Ob-cop _  Our colimit will arise as a quotient object of this coproduct-of-objects, namely the coequaliser of two carefully chosen morphisms. As a guiding example, the pushout of and should be the quotient of by the equivalence relation generated by In full generality, for each arrow in our diagram, we should have that injecting into the component of our coproduct should give the same result as precomposing with and injecting into the component. This suggests to build another indexed coproduct of all the domains of arrows in the diagram, taking the first morphism to be the injection into the domain component and the second morphism to be the injection into the codomain component precomposed with  Dom : Indexed-coproduct C {Idx = Arrows J} Ξ» (a , b , f) β Fβ a Dom = has-Arrows-cop _ s t : C.Hom (Dom .Ξ£F) (Obs .Ξ£F) s = Dom .match Ξ» (a , b , f) β Obs .ΞΉ b C.β Fβ f t = Dom .match Ξ» (a , b , f) β Obs .ΞΉ a coequ : Coequaliser C s t coequ = has-coeq _ _ colim : make-is-colimit F (coequ .coapex)  The rest of the proof amounts to repackaging the data of the coequaliser and coproducts as the data for a colimit.  colim .Ο c = coequ .coeq C.β Obs .ΞΉ c colim .commutes {a} {b} f = (coequ .coeq C.β Obs .ΞΉ b) C.β Fβ f β‘Λβ¨ C.extendr (Dom .commute) β©β‘Λ β coequ .coeq C.β s β C.β Dom .ΞΉ (a , b , f) β‘β¨ ap! (coequ .coequal) β©β‘ (coequ .coeq C.β t) C.β Dom .ΞΉ (a , b , f) β‘β¨ C.pullr (Dom .commute) β©β‘ coequ .coeq C.β Obs .ΞΉ a β colim .universal {x} e comm = coequ .universal comm' where e' : C.Hom (Obs .Ξ£F) x e' = Obs .match e comm' : e' C.β s β‘ e' C.β t comm' = Indexed-coproduct.uniqueβ Dom Ξ» i@(a , b , f) β (e' C.β s) C.β Dom .ΞΉ i β‘β¨ C.extendr (Dom .commute) β©β‘ β e' C.β Obs .ΞΉ b β C.β Fβ f β‘β¨ ap! (Obs .commute) β©β‘ e b C.β Fβ f β‘β¨ comm f β©β‘ e a β‘Λβ¨ Obs .commute β©β‘Λ e' C.β Obs .ΞΉ a β‘Λβ¨ C.pullr (Dom .commute) β©β‘Λ (e' C.β t) C.β Dom .ΞΉ i β colim .factors {j} e comm = colim .universal e comm C.β (coequ .coeq C.β Obs .ΞΉ j) β‘β¨ C.pulll (coequ .factors) β©β‘ Obs .match e C.β Obs .ΞΉ j β‘β¨ Obs .commute β©β‘ e j β colim .unique e comm u' fac = coequ .unique$ Obs .unique _
Ξ» i β sym (C.assoc _ _ _) β fac i


This implies that a category with coequalisers and large enough indexed coproducts has all colimits.

  coproducts+coequalisersβcocomplete
: β {oj βj}
β has-indexed-coproducts C (oj β βj)
β has-coequalisers C
β is-cocomplete oj βj C
coproducts+coequalisersβcocomplete {oj} {βj} has-cop has-coeq =
colimit-as-coequaliser-of-coproduct
(Ξ» _ β Lift-Indexed-coproduct C βj (has-cop _))
(Ξ» _ β has-cop _)
has-coeq