module Cat.Diagram.Colimit.Cocone where

Colimits via coconesπŸ”—

As noted in the main page on colimits, most introductory texts opt to define colimits via categorical gadgets called cocones. A Cocone over is given by an object (the coapex) together with a family of maps ψ β€” one for each object in the indexing category J β€” such that β€œeverything in sight commutes”.

  record Cocone : Type (o βŠ” β„“ βŠ” o' βŠ” β„“') where
    constructor cocone
      coapex : C.Ob
      ψ      : (x : J.Ob) β†’ C.Hom (F.β‚€ x) coapex
      commutes : βˆ€ {x y} (f : J.Hom x y) β†’ ψ y C.∘ F.₁ f ≑ ψ x

Cocone mapsπŸ”—

To express the universal property of a colimit in terms of cocones, we now have to define the notion of cocone homomorphism. We define a cocone homomorphism to be a map between the coapices which commutes with the family

  record Cocone-hom (x y : Cocone) : Type (o βŠ” β„“') where
    constructor cocone-hom
      hom      : C.Hom (x .coapex) (y .coapex)
      commutes : βˆ€ o β†’ hom C.∘ x .ψ o ≑ y .ψ o

Since cocone homomorphisms are closed under composition in the base category, it’s immediate that they form a category.

  Cocones : Precategory _ _
  Cocones = cat where
    open Precategory

    compose : βˆ€ {x y z} β†’ Cocone-hom y z β†’ Cocone-hom x y β†’ Cocone-hom x z
    compose K L .hom = K .hom C.∘ L .hom
    compose {x = x} {y = y} {z = z} K L .commutes o =
      (K .hom C.∘ L .hom) C.∘ x .ψ o β‰‘βŸ¨ C.pullr (L .commutes o) βŸ©β‰‘
      K .hom C.∘ y .ψ o              β‰‘βŸ¨ K .commutes o βŸ©β‰‘
      z .ψ o                         ∎

Initial cocones as colimitsπŸ”—

A cocone over some diagram contains the same data as natural transformation from to a constant functor. Since we have defined a colimit to consist of (a functor equipped with) a natural transformation into a constant functor, there is an equivalence between the cocones defined here and those considered in the definition of colimit.

  Cocone→cocone : (K : Cocone) → F => Const (Cocone.coapex K)
  Coconeβ†’cocone K .Ξ· = K .Cocone.ψ
  Coconeβ†’cocone K .is-natural x y f = K .Cocone.commutes f βˆ™ sym (C.idl _)

We can then rephrase the universality from the definition of left Kan extension by asking that a particular cocone be initial in the category we have just constructed.

    : βˆ€ {K : Cocone}
    β†’ is-initial Cocones K
    → is-colimit F (Cocone.coapex K) (Cocone→cocone K)
  is-initial-cocone→is-colimit {K = K} init = to-is-colimitp colim refl where
    open make-is-colimit
    open Cocone
    open Cocone-hom

    colim : make-is-colimit F (Cocone.coapex K)
    colim .ψ = K .ψ
    colim .commutes = K .commutes
    colim .universal eta p = init (cocone _ eta p) .centre .hom
    colim .factors eta p = init (cocone _ eta p) .centre .commutes _
    colim .unique eta p other q =
      ap hom (sym (init (cocone _ eta p) .paths (cocone-hom other q)))

To finish concretising the correspondence, note that this process is invertible: From a colimit, we can extract an initial cocone.

    : βˆ€ {x} {eta : F => Const x}
    β†’ (L : is-colimit F x eta)
    β†’ is-initial Cocones (cocone x (is-colimit.ψ L) (is-colimit.commutes L))
The proof consists of more data shuffling, so we omit it.
  is-colimit→is-initial-cocone {x  = x} L K = init where
    module L = is-colimit L
    module K = Cocone K
    open Cocone-hom

    init : is-contr (Cocone-hom (cocone x L.ψ L.commutes) K)
    init .centre .hom = L.universal K.ψ K.commutes
    init .centre .commutes _ = L.factors K.ψ K.commutes
    init .paths f =
      Cocone-hom-path (sym (L.unique K.ψ K.commutes (f .hom) (f .commutes)))