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 $F$ 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
    no-eta-equality
    constructor cocone
    field
      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
    no-eta-equality
    constructor cocone-hom
    field
      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 $F$ contains the same data as natural transformation from $F$ 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.

  is-initial-cocone→is-colimit
    : ∀ {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.

  is-colimit→is-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)))