open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Coherence
open import Cat.Instances.Functor
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

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”.

We define colimits in a similar way to limits; the only difference being that we define a colimits of a diagram $F$ as left Kan extensions instead of right Kan extensions. 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

  cocone→unit : ∀ {x : C.Ob} → (Diagram => Const x) → Diagram => const! x F∘ !F
  unquoteDef cocone→unit = define-coherence cocone→unit

  is-colimit : (x : C.Ob) → Diagram => Const x → Type _
  is-colimit x cocone =
    is-lan !F Diagram (const! x) (cocone→unit 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 $\phi$. Moreover, if $f : x \to y$ is a morphism in the “shape” category $\mathcal{J}$, we require $\psi y \circ Ff = \psi x$, 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 $\psi$ is the universal family of maps with this property; if $\varepsilon_j : Fj \to x$ is another natural family, then each $\varepsilon_j$ factors through the coapex by a unique universal morphism:

      universal
        : ∀ {x : C.Ob}
        → (eps : ∀ j → C.Hom (F₀ j) x)
        → (∀ {x y} (f : J.Hom x y) → eps y C.∘ F₁ f ≡ eps x)
        → C.Hom coapex x
      factors
        : ∀ {j : J.Ob} {x : C.Ob}
        → (eps : ∀ j → C.Hom (F₀ j) x)
        → (p : ∀ {x y} (f : J.Hom x y) → eps y C.∘ F₁ f ≡ eps x)
        → universal eps p C.∘ ψ j ≡ eps j
      unique
        : ∀ {x : C.Ob}
        → (eps : ∀ j → C.Hom (F₀ j) x)
        → (p : ∀ {x y} (f : J.Hom x y) → eps y C.∘ F₁ f ≡ eps x)
        → (other : C.Hom coapex x)
        → (∀ j → other C.∘ ψ j ≡ eps j)
        → other ≡ universal eps p

    unique₂
      : ∀ {x : C.Ob}
      → (eps : ∀ j → C.Hom (F₀ j) x)
      → (p : ∀ {x y} (f : J.Hom x y) → eps y C.∘ F₁ f ≡ eps x)
      → ∀ {o1} → (∀ j → o1 C.∘ ψ j ≡ eps j)
      → ∀ {o2} → (∀ j → o2 C.∘ ψ j ≡ eps j)
      → o1 ≡ o2
    unique₂ eps p q r = unique eps p _ q ∙ sym (unique eps 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 {α = α} = Nat-path λ j →
      factors (α .η) _
    colim .σ-uniq {α = α} {σ′ = σ′} p = Nat-path λ _ →
      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)) F∘ !F} {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' .σ α = hom→⊤-natural-trans (lan.σ α .η tt)
    lan' .σ-comm {M} {α} = Nat-path λ j →
      ap (_ C.∘_) (sym q)
      ∙ lan.σ-comm {α = α} ηₚ _
    lan' .σ-uniq {M} {α} {σ′} r = Nat-path λ j →
      lan.σ-uniq {σ′ = hom→⊤-natural-trans (σ′ .η tt)}
        (Nat-path (λ 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 (Functor.F₀ 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} (eps : ∀ j → C.Hom (F₀ j) x)
                 (p : ∀ {x y} (f : J.Hom x y) →  eps y C.∘ F₁ f ≡ eps x)
      where

      eps-nt : D => const! x F∘ !F
      eps-nt .η = eps
      eps-nt .is-natural _ _ f = p f ∙ sym (C.idl _)

      hom : C.Hom coapex x
      hom = σ {M = const! x} eps-nt .η tt

    mc : make-is-colimit D coapex
    mc .ψ = eta.η
    mc .commutes f = eta.is-natural _ _ f ∙ C.eliml (Functor.F-id F)
    mc .universal = hom
    mc .factors e p = σ-comm {α = eps-nt e p} ηₚ _
    mc .unique {x = x} eta p other q =
      sym $ σ-uniq {σ′ = other-nt} (Nat-path λ j → sym (q j)) ηₚ tt
      where
        other-nt : F => const! x
        other-nt .η _ = other
        other-nt .is-natural _ _ _ = C.elimr (Functor.F-id F) ∙ 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 Lan L
    open Functor
    open _=>_

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 $\{*\} \to \mathcal{C}$ with value coapex to be a Kan extension, but Colimit, being an instance of Lan, packages an arbitrary functor $\{*\} \to \mathcal{C}$.

Since Agda does not compare functors for $\eta$-equality, 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 =
    Nat-path (λ _ → σ-comm ηₚ _)
  has-colimit .is-lan.σ-uniq {M = M} {σ′ = σ′} p =
    Nat-path (λ _ → σ-uniq {σ′ = nt} (Nat-path (λ j → p ηₚ j)) ηₚ _)
    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 $\top \to \mathcal{C}$ correspond with isomorphisms in $\mathcal{C}$.

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 =
    natural-inverses→inverses
      {α = hom→⊤-natural-trans f}
      {β = hom→⊤-natural-trans g}
      (Lan-unique.σ-inversesp Cx Cy
        (Nat-path λ j → f-factor {j})
        (Nat-path λ j → g-factor {j}))
      tt

  colimits→invertiblep {f = f} f-factor =
    is-natural-invertible→invertible
      {α = hom→⊤-natural-trans f}
      (Lan-unique.σ-is-invertiblep
        Cx
        Cy
        (Nat-path λ 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 =
    Nat-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 golfin 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}
    → (eps : ∀ j → C.Hom (D.₀ j) x)
    → (∀ {x y} (f : J.Hom x y) → eps y C.∘ D.₁ f ≡ eps 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}
    → (eps : ∀ j → C.Hom (D.₀ j) (K' .F₀ tt))
    → (p : ∀ {x y} (f : J.Hom x y) → eps y C.∘ D.₁ f ≡ eps x)
    → (∀ {j} → eps j ≡ eta .η j)
    → C.is-invertible (Cy.universal eps p)
    → is-lan !F D K' eta
  is-invertible→is-colimitp {K' = K'} {eta = eta} eps p q invert =
    generalize-colimitp
      (is-invertible→is-lan Cy $ componentwise-invertible→invertible _ λ _ → invert)
      q

Another useful fact is that if $C$ is a colimit of some diagram $Dia$, and $Dia$ is naturally isomorphic to some other diagram $Dia'$, then the coapex of $C$ is also a colimit of $Dia'$.

  natural-iso-diagram→is-colimitp
    : ∀ {D′ : Functor J C} {eta : D′ => K F∘ !F}
    → (isos : natural-iso D D′)
    → (∀ {j} →  Cy.ψ j C.∘ natural-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
    : natural-iso 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 natural-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 of Colimits🔗

The definitions here are the same idea as preservation of limits, just dualized.

module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategory o₃ h₃}
         (F : Functor C D) (Diagram : Functor J C) where
  private
    module D = Precategory D
    module C = Precategory C
    module J = Precategory J
    module F = Func F

  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} {eps : Diagram => K F∘ !F}
    → (lan : is-lan !F (F F∘ Diagram) (F F∘ K) (nat-assoc-to (F ▸ eps)))
    → 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}
    → {eps : (j : J.Ob) → C.Hom (Dia.F₀ j) x}
    → {p : ∀ {i j} (f : J.Hom i j) → eps j C.∘ Dia.F₁ f ≡ eps i}
    → (colim : is-lan !F Dia K eta)
    → F.F₁ (is-colimit.universal colim eps p) ≡ is-colimit.universal (preserves colim) (λ j → F.F₁ (eps 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
    : natural-iso F F'
    → preserves-colimit F Dia
    → preserves-colimit F' Dia
  natural-iso→preserves-colimits α F-preserves {K = K} {eps} colim =
    natural-isos→is-lan
      idni (α ◂ni Dia) (α ◂ni K)
      (Nat-path λ j →
        ⌜ F' .F₁ (K .F₁ tt) D.∘ α.to .η _ ⌝ D.∘ (F .F₁ (eps .η j) D.∘ α.from .η _) ≡⟨ ap! (eliml F' (K .F-id)) ⟩≡
        α.to .η _ D.∘ (F .F₁ (eps .η j) D.∘ α.from .η _)                           ≡⟨ D.pushr (sym (α.from .is-natural _ _ _)) ⟩≡
        ((α.to .η _ D.∘ α.from .η _) D.∘ F' .F₁ (eps .η j))                        ≡⟨ D.eliml (α.invl ηₚ _) ⟩≡
        F' .F₁ (eps .η j) ∎)
      (F-preserves colim)
    where
      module α = natural-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 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, \ell)$-cocomplete if it has colimits for any diagram indexed by a precategory with objects in $\mathrm{Type}\ o$ and morphisms in $\mathrm{Type}\ \ell$.

is-cocomplete : ∀ {oc ℓc} o ℓ → Precategory oc ℓc → Type _
is-cocomplete o ℓ C = ∀ {D : Precategory o ℓ} (F : Functor D C) → Colimit F