open import Cat.Functor.Naturality.Reflection
open import Cat.Diagram.Pullback.Properties
open import Cat.Functor.Adjoint.Continuous
open import Cat.Instances.Shape.Terminal
open import Cat.CartesianClosed.Locally
open import Cat.Instances.Slice.Colimit
open import Cat.Functor.Kan.Reflection
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Finite
open import Cat.Instances.Shape.Join
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Naturality
open import Cat.Diagram.Pullback
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Functor.Pullback
open import Cat.Functor.Compose
open import Cat.Instances.Slice
open import Cat.Prelude

open import Data.Sum

import Cat.Reasoning

open Functor
open _=>_

module Cat.Diagram.Colimit.Universal where

Universal colimits🔗

A colimit in a category $\mathcal{C}$ with pullbacks is said to be universal, or stable under pullback, if it is preserved under base change.

There are multiple ways to make this precise. First, we might consider pulling back a colimiting cocone — say, for the sake of concreteness, a coproduct diagram $A\to A+B\leftarrow B$ — along some morphism $f:X\to A+B\text{:}$

We say that the bottom colimit is universal if the top cocone $f^{\ast }A\to X\leftarrow f^{\ast }B$ is also colimiting for all $f\text{.}$

Alternatively, we might consider pulling back a colimiting cocone in $\mathcal{C}/Y$ along some morphism $f:X\to Y$ like so:

In this case, we say that the colimit is stable under pullback if the top diagram is colimiting in $\mathcal{C}/X\text{,}$ which amounts to saying that every pullback functor $f^{\ast }:\mathcal{C}/Y\to \mathcal{C}/X$ preserves this colimit.

module _ {oj ℓj oc ℓc}
  (J : Precategory oj ℓj)
  (C : Precategory oc ℓc)
  (pb : has-pullbacks C)
  where
  open Precategory C

  has-stable-colimits : Type _
  has-stable-colimits =
    ∀ {X Y} (f : Hom X Y) (F : Functor J (Slice C Y))
    → preserves-colimit (Base-change pb f) F

Universality vs. pullback-stability🔗

If $\mathcal{C}$ has all colimits of shape $\mathcal{J}\text{,}$ we can show that the two notions are equivalent.

We start by noticing that a cocone under $F$ with coapex $X$ in $\mathcal{C}$ can equivalently be described as a functor ${\mathcal{J}}^{▹}\to \mathcal{C}$ that sends the adjoined terminal object of ${\mathcal{J}}^{▹}$ to $X$ and otherwise restricts to $F\text{.}$

module _ {oj ℓj oc ℓc} {J : Precategory oj ℓj} {C : Precategory oc ℓc} where
  open Cat.Reasoning C
  open /-Obj
  open /-Hom

  cocone→cocone▹
    : ∀ {X} {F : Functor J C} → F => X F∘ !F → Functor (J ▹) C
  cocone▹→cocone
    : (F : Functor (J ▹) C) → F F∘ ▹-in => Const (F .F₀ (inr _))

  is-colimit▹ : Functor (J ▹) C → Type _
  is-colimit▹ F = is-colimit (F F∘ ▹-in) (F .F₀ (inr _)) (cocone▹→cocone F)

Yet another way of describing a cocone with coapex $X$ is as a functor $\mathcal{J}\to \mathcal{C}/X$ into the slice category over $X\text{:}$

  cocone/→cocone▹
    : ∀ {X} → Functor J (Slice C X) → Functor (J ▹) C
  cocone▹→cocone/
    : (F : Functor (J ▹) C) → Functor J (Slice C (F .F₀ (inr _)))

  cocone→cocone▹ {X} {F} α .F₀ (inl j) = F .F₀ j
  cocone→cocone▹ {X} {F} α .F₀ (inr tt) = X .F₀ _
  cocone→cocone▹ {X} {F} α .F₁ {inl x} {inl y} (lift f) = F .F₁ f
  cocone→cocone▹ {X} {F} α .F₁ {inl x} {inr tt} (lift f) = α .η x
  cocone→cocone▹ {X} {F} α .F₁ {inr tt} {inr tt} (lift tt) = id
  cocone→cocone▹ {X} {F} α .F-id {inl x} = F .F-id
  cocone→cocone▹ {X} {F} α .F-id {inr x} = refl
  cocone→cocone▹ {X} {F} α .F-∘ {inl x} {inl y} {inl z} f g = F .F-∘ _ _
  cocone→cocone▹ {X} {F} α .F-∘ {inl x} {inl y} {inr z} f g =
    sym (α .is-natural _ _ _ ∙ eliml (X .F-id))
  cocone→cocone▹ {X} {F} α .F-∘ {inl x} {inr y} {inr z} f g = sym (idl _)
  cocone→cocone▹ {X} {F} α .F-∘ {inr x} {inr y} {inr z} f g = sym (idl _)

  cocone▹→cocone F .η j = F .F₁ _
  cocone▹→cocone F .is-natural x y f = sym (F .F-∘ _ _) ∙ sym (idl _)

  cocone/→cocone▹ F .F₀ (inl x) = F .F₀ x .domain
  cocone/→cocone▹ {X} F .F₀ (inr _) = X
  cocone/→cocone▹ F .F₁ {inl x} {inl y} (lift f) = F .F₁ f .map
  cocone/→cocone▹ F .F₁ {inl x} {inr _} f = F .F₀ x .map
  cocone/→cocone▹ F .F₁ {inr _} {inr _} f = id
  cocone/→cocone▹ F .F-id {inl x} = ap map (F .F-id)
  cocone/→cocone▹ F .F-id {inr _} = refl
  cocone/→cocone▹ F .F-∘ {inl x} {inl y} {inl z} f g = ap map (F .F-∘ _ _)
  cocone/→cocone▹ F .F-∘ {inl x} {inl y} {inr z} f (lift g) = sym (F .F₁ g .commutes)
  cocone/→cocone▹ F .F-∘ {inl x} {inr y} {inr z} f g = sym (idl _)
  cocone/→cocone▹ F .F-∘ {inr x} {inr y} {inr z} f g = sym (idl _)

  cocone▹→cocone/ F .F₀ j = cut {domain = F .F₀ (inl j)} (F .F₁ _)
  cocone▹→cocone/ F .F₁ f .map = F .F₁ (lift f)
  cocone▹→cocone/ F .F₁ f .commutes = sym (F .F-∘ _ _)
  cocone▹→cocone/ F .F-id = ext (F .F-id)
  cocone▹→cocone/ F .F-∘ f g = ext (F .F-∘ _ _)

Using this language, we can define what it means for $\mathcal{C}$ to have universal colimits in the sense of the first diagram above: for every equifibred natural transformation $\alpha :F\Rightarrow G$ between diagrams ${\mathcal{J}}^{▹}\to \mathcal{C}\text{,}$ if $G$ is colimiting then $F$ is colimiting.

module _ {oj ℓj oc ℓc}
  (J : Precategory oj ℓj)
  (C : Precategory oc ℓc)
  where

  has-universal-colimits : Type _
  has-universal-colimits =
    ∀ (F G : Functor (J ▹) C) (α : F => G) → is-equifibred α
    → is-colimit▹ G → is-colimit▹ F

We will establish the equivalence between pullback-stable and universal colimits in several steps. First, we show that pullback-stability is equivalent to the following condition: for every diagram as below, that is, for every equifibred natural transformation $\alpha :F\Rightarrow G$ between diagrams $F,G:{\mathcal{J}}^{▹▹}\to \mathcal{C}\text{,}$ if the bottom diagram $G$ (seen as a diagram ${\mathcal{J}}^{▹}\to \mathcal{C}/Y\text{)}$ is colimiting, then the top diagram $F$ (seen as a diagram ${\mathcal{J}}^{▹}\to \mathcal{C}/X\text{)}$ is colimiting.

module _ {oj ℓj oc ℓc}
  (J : Precategory oj ℓj)
  (C : Precategory oc ℓc)
  (pb : has-pullbacks C)
  where
  open Cat.Reasoning C
  open /-Obj
  open /-Hom
  open is-pullback
  private
    module C/ {X} = Cat.Reasoning (Slice C X)

    step2 =
      ∀ (F G : Functor (J ▹ ▹) C) (α : F => G) → is-equifibred α
      → is-colimit▹ (cocone▹→cocone/ G) → is-colimit▹ (cocone▹→cocone/ F)

In the forwards direction, we use the uniqueness of pullbacks to construct a natural isomorphism $f^{\ast }\circ G\cong F:{\mathcal{J}}^{▹}\to \mathcal{C}/X\text{;}$ since the pullback functor $f^{\ast }$ is assumed to preserve colimits, we get that $F$ is colimiting.

    step1→2 : has-stable-colimits J C pb → step2
    step1→2 u F G α eq G-colim = F-colim where
      f = α .η (inr _)

      f*G≅F : Base-change pb f F∘ cocone▹→cocone/ G F∘ ▹-in
            ≅ⁿ cocone▹→cocone/ F F∘ ▹-in
      f*G≅F = iso→isoⁿ
        (λ j → C/.invertible→iso
          (record { map = eq _ .universal (sym (pb _ _ .Pullback.square))
                  ; commutes = eq _ .p₁∘universal })
          (Forget/-is-conservative (Equiv.from (pullback-unique (rotate-pullback (eq _)) _)
            (pb _ _ .Pullback.has-is-pb))))
        λ f → ext (unique₂ (eq _)
          {p = sym (pb _ _ .Pullback.square) ∙ pushl (G .F-∘ _ _)}
          (pulll (sym (F .F-∘ _ _)) ∙ eq _ .p₁∘universal)
          (pulll (α .is-natural _ _ _) ∙ pullr (eq _ .p₂∘universal))
          (pulll (eq _ .p₁∘universal) ∙ pb _ _ .Pullback.p₂∘universal)
          (pulll (eq _ .p₂∘universal) ∙ pb _ _ .Pullback.p₁∘universal))

      f*G-colim : preserves-lan (Base-change pb f) G-colim
      f*G-colim = u f _ G-colim

      F-colim : is-colimit▹ (cocone▹→cocone/ F)
      F-colim = natural-isos→is-lan idni
        f*G≅F
        (!const-isoⁿ (C/.invertible→iso
          (record { map = eq _ .universal (sym (pb _ _ .Pullback.square))
                  ; commutes = eq _ .p₁∘universal })
          (Forget/-is-conservative (Equiv.from (pullback-unique (rotate-pullback (eq _)) _)
            (pb _ _ .Pullback.has-is-pb)))))
        (ext λ j → (idl _ ⟩∘⟨refl) ∙ unique₂ (eq _)
          {p = eq _ .square ∙ pushl (G .F-∘ _ _)}
          (pulll (eq _ .p₁∘universal) ·· pulll (pb _ _ .Pullback.p₂∘universal) ·· pb _ _ .Pullback.p₂∘universal)
          (pulll (eq _ .p₂∘universal) ·· pulll (pb _ _ .Pullback.p₁∘universal) ·· pullr (pb _ _ .Pullback.p₁∘universal))
          (sym (F .F-∘ _ _))
          (α .is-natural _ _ _))
        f*G-colim

For the converse direction, we build a natural transformation from the pullback of $G$ to $G$ and show that it is equifibred using the pasting law for pullbacks. The rest of the proof consists in repackaging data between “obviously isomorphic” functors.

    step2→1 : step2 → has-stable-colimits J C pb
    step2→1 u f F {K} {eta} = trivial-is-colimit! ⊙ u _ _ α eq ⊙ trivial-is-colimit!
      where
        α : cocone/→cocone▹ (Base-change pb f F∘ cocone→cocone▹ eta)
         => cocone/→cocone▹ (cocone→cocone▹ eta)
        α .η (inl j) = pb _ _ .Pullback.p₁
        α .η (inr _) = f
        α .is-natural (inl x) (inl y) g = pb _ _ .Pullback.p₁∘universal
        α .is-natural (inl x) (inr _) g = sym (pb _ _ .Pullback.square)
        α .is-natural (inr _) (inr _) g = id-comm

        eq : is-equifibred α
        eq {inl x} {inl y} (lift g) = pasting-outer→left-is-pullback
          (rotate-pullback (pb _ _ .Pullback.has-is-pb))
          (subst₂ (λ x y → is-pullback C x f (pb _ _ .Pullback.p₁) y)
            (sym ((Base-change pb f F∘ cocone→cocone▹ eta) .F₁ g .commutes))
            (sym (cocone→cocone▹ eta .F₁ g .commutes))
            (rotate-pullback (pb _ _ .Pullback.has-is-pb)))
          (α .is-natural (inl x) (inl y) (lift g))
        eq {inl x} {inr _} g = rotate-pullback (pb _ _ .Pullback.has-is-pb)
        eq {inr _} {inr _} g = id-is-pullback

Next, we prove that this is equivalent to requiring that the top diagram ${\mathcal{J}}^{▹}\to \mathcal{C}$ be colimiting if the bottom diagram ${\mathcal{J}}^{▹}\to \mathcal{C}$ is colimiting, disregarding the $X\to Y$ part entirely.

    step3 =
      ∀ (F G : Functor (J ▹ ▹) C) (α : F => G) → is-equifibred α
      → is-colimit▹ (G F∘ ▹-in) → is-colimit▹ (F F∘ ▹-in)

This follows from the characterisation of colimits in slice categories: assuming that all $\mathcal{J}\text{-colimits}$ exist in $\mathcal{C}\text{,}$ the forgetful functor $\mathcal{C}/X\to \mathcal{C}$ both preserves and reflects colimits.

    module _ (J-colims : ∀ (F : Functor J C) → Colimit F) where
      colim/≃colim
        : (F : Functor (J ▹ ▹) C)
        → is-colimit▹ (cocone▹→cocone/ F) ≃ is-colimit▹ (F F∘ ▹-in)
      colim/≃colim F =
        prop-ext!
          (Forget/-preserves-colimits _ (J-colims _))
          (Forget/-reflects-colimits _)
        ∙e trivial-colimit-equiv!

      step2≃3 : step2 ≃ step3
      step2≃3 = Π-cod≃ λ F → Π-cod≃ λ G → Π-cod≃ λ α → Π-cod≃ λ eq →
        function≃ (colim/≃colim G) (colim/≃colim F)

Finally, we show that this is equivalent to $\mathcal{C}$ having universal colimits. This follows easily by noticing that ${\mathcal{J}}^{▹▹}$ retracts onto ${\mathcal{J}}^{▹}\text{.}$

    step3→4 : step3 → has-universal-colimits J C
    step3→4 u F G α eq = Equiv.to (function≃ (▹-retract G) (▹-retract F))
      (u _ _ (α ◂ ▹-join) (◂-equifibred ▹-join α eq))
      where
        ▹-retract
          : (F : Functor (J ▹) C)
          → is-colimit▹ ((F F∘ ▹-join) F∘ ▹-in) ≃ is-colimit▹ F
        ▹-retract F = trivial-colimit-equiv!

    step4→3 : has-universal-colimits J C → step3
    step4→3 u F G α eq = u _ _ (α ◂ ▹-in) (◂-equifibred ▹-in α eq)

This concludes our equivalence.

  stable≃universal
    : (∀ (F : Functor J C) → Colimit F)
    → has-stable-colimits J C pb ≃ has-universal-colimits J C
  stable≃universal J-colims =
       prop-ext! step1→2 step2→1
    ∙e step2≃3 J-colims
    ∙e prop-ext! step3→4 step4→3

Examples🔗

As a general class of examples, any locally cartesian closed category has pullback-stable colimits, because the pullback functor has a right adjoint and therefore preserves colimits.

module _ {o ℓ} {C : Precategory o ℓ} (lcc : Locally-cartesian-closed C) where
  open Locally-cartesian-closed lcc
  open Finitely-complete has-is-lex

  lcc→stable-colimits
    : ∀ {oj ℓj} {J : Precategory oj ℓj}
    → has-stable-colimits J C pullbacks
  lcc→stable-colimits f F = left-adjoint-is-cocontinuous
    (lcc→pullback⊣dependent-product C lcc f)