open import Cat.Diagram.Initial
open import Cat.Prelude

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

module Cat.Diagram.Colimit.Base where

IdeaπŸ”—

Colimits are dual to limits limit; much like their cousins, 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.”

ConstructionπŸ”—

Every concrete colimit (coproducts, coequalisers, initial objects) we have seen so far consists of roughly the same data. We begin with some collection of objects and morphisms, and then state that the colimit of that collection is some object with a universal property relating all of those objects and morphisms.

It would be convienent to be able to talk about all of these situations at once, as opposed to on a case-by-case basis. To do this, we need to introduce a bit of categorical machinery: the Cocone.

The first step is to generalize the β€œcollection of objects and morphisms” involved. Luckily, this step involves no new ideas, just a change in perspective. We already have a way of describing a collection of objects and morphisms: it’s a category! As an example, the starting data of a coproduct is a pair of objects, which can be thought of as a very simple category, with only identity morphisms.

The next step also involves nothing more than a change in perspective. Let’s denote our β€œdiagram” category from earlier as JJ. Then, a means of picking out a JJ shaped figure in CC is… a functor F:Jβ†’CF : J \to C! Going back to the coproduct example, a functor from our 2 object category into CC selects 2 (not necessarily distinct!) objects in CC. We this pair of category and functor a diagram in CC.

module _ {J : Precategory o β„“} {C : Precategory oβ€² β„“β€²} (F : Functor J C) where
  private
    import Cat.Reasoning J as J
    import Cat.Reasoning C as C
    module F = Functor F

  record Cocone : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€²) where
    no-eta-equality
    constructor cocone

Now, for the actual machinery! If we want to capture the essence of all of our concrete examples of colimits, we a notion of an object equipped with maps from every object in our diagram. We call this designated object the β€œcoapex” of the cocone.

    field
      coapex : C.Ob
      ψ      : (x : J.Ob) β†’ C.Hom (F.β‚€ x) coapex

If our diagram consisted of only objects, we would be done! However, some diagrams contan non-identity morphisms, so we need to take those into account as well. This bit is best understood through the lens of the coequaliser: in order to describe the commuting condition there, we want every injection map from the codomain of a morphism to factor through that morphism.

      commutes : βˆ€ {x y} (f : J.Hom x y) β†’ ψ y C.∘ F.₁ f ≑ ψ x

As per usual, we define a helper lemma charaterizing the path space of cones:

  open Cocone

  Cocone-path : {x y : Cocone}
              β†’ (p : coapex x ≑ coapex y)
              β†’ (βˆ€ o β†’ PathP (Ξ» i β†’ C.Hom (F.β‚€ o) (p i)) (ψ x o) (ψ y o))
              β†’ x ≑ y
  Cocone-path p q i .coapex = p i
  Cocone-path p q i .ψ o = q o i
  Cocone-path {x = x} {y = y} p q i .commutes {x = a} {y = b} f =
    is-propβ†’pathp (Ξ» i β†’ C.Hom-set _ _ (q b i C.∘ F.₁ f) (q a i))
      (x .commutes f) (y .commutes f) i

Cocone MapsπŸ”—

Now that we’ve defined cocones, we need a way to figure out how to express universal properties. Like most things categorical, we begin by considering a β€œcocone morphism,” which will give us a category that we can work within. The idea here is that a morphism of cocones is a morphism in CC between the coapicies, such that all of the injection maps commute.

  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

We define yet another helper lemma that describes the path space of cocone morphisms.

  open Cocone-hom

  Cocone-hom-path : βˆ€ {x y} {f g : Cocone-hom x y} β†’ f .hom ≑ g .hom β†’ f ≑ g
  Cocone-hom-path p i .hom = p i
  Cocone-hom-path {x = x} {y = y} {f = f} {g = g} p i .commutes o j =
    is-set→squarep (λ i j → C.Hom-set _ _)
      (Ξ» j β†’ p j C.∘ x .ψ o) (f .commutes o) (g .commutes o) refl i j

Now, we can define the category of cocones over a given diagram:

  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                         ∎

    cat : Precategory _ _
    cat .Ob = Cocone
    cat .Hom = Cocone-hom
    cat .id = cocone-hom C.id (Ξ» _ β†’ C.idl _)
    cat ._∘_ = compose
    cat .idr f = Cocone-hom-path (C.idr (f .hom))
    cat .idl f = Cocone-hom-path (C.idl (f .hom))
    cat .assoc f g h = Cocone-hom-path (C.assoc (f .hom) (g .hom) (h .hom))

ColimitsπŸ”—

We now have all of the machinery in place! What remains is the universal property, which expresses that a particular cocone is universal, in the sense that it has a unique map to any other cocone. However, we already have something that captures this idea, it’s the initial object! This leads to the following terse definition: A colimit over a diagram is an initial object in the category of cocones over that diagram. 
  is-colimit : Cocone β†’ Type _
  is-colimit K = is-initial Cocones K

  Colimit : Type _
  Colimit = Initial Cocones

  Colimit-apex : Colimit β†’ C.Ob
  Colimit-apex x = coapex (Initial.bot x)

Preservation of ColimitsπŸ”—

Because a cocone is a commutative diagram, any given functor F:C→DF : \ca{C} \to \ca{D} takes cocones in C\ca{C} to cocones in D\ca{D}, as functors preserve commutative diagrams.

  F-map-cocone : Cocone Dia β†’ Cocone (F F∘ Dia)
  F-map-cocone x .Cocone.coapex = F.β‚€ (Cocone.coapex x)
  F-map-cocone x .Cocone.ψ f = F.₁ (Cocone.ψ x f)
  F-map-cocone x .Cocone.commutes {y = y} f =
    F.₁ (Cocone.ψ x y) D.∘ F .F₁ _ β‰‘βŸ¨ F.collapse (Cocone.commutes x _) βŸ©β‰‘
    F.₁ (Cocone.ψ x _)             ∎

Though functors must take cocones to cocones, they may not necessarily take colimiting cocones to colimiting cocones! When a functor does, we say that it preserves colimits.

  Preserves-colimit : Cocone Dia β†’ Type _
  Preserves-colimit K = is-colimit Dia K β†’ is-colimit (F F∘ Dia) (F-map-cocone K)

CocompletenessπŸ”—

A category is cocomplete if admits for limits 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 (o,β„“)(o, \ell)-cocomplete if it has colimits for any diagram indexed by a precategory with objects in TypeΒ o\ty\ o and morphisms in TypeΒ β„“\ty\ \ell.

is-cocomplete : βˆ€ {oc β„“c} o β„“ β†’ Precategory oc β„“c β†’ Type _
is-cocomplete o β„“ C = βˆ€ {D : Precategory o β„“} (F : Functor D C) β†’ Colimit F