module Cat.Diagram.Colimit.Universal where

Universal colimits🔗

A colimit in a category 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 — along some morphism

We say that the bottom colimit is universal if the top cocone is also colimiting for all

Alternatively, we might consider pulling back a colimiting cocone in along some morphism like so:

In this case, we say that the colimit is stable under pullback if the top diagram is colimiting in which amounts to saying that every pullback functor preserves this colimit.

  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

This definition makes sense even if not all pullback functors exist; however, for the sake of simplicity, we assume that has all pullbacks.

Universality vs. pullback-stability🔗

If has all colimits of shape we can show that the two notions are equivalent.


This is essentially a 1-categorical version of the proof of lemma in Higher Topos Theory (Lurie 2008).

We start by noticing that a cocone under with coapex in can equivalently be described as a functor that sends the adjoined terminal object of to and otherwise restricts to

    : ∀ {X} {F : Functor J C} → F => X F∘ !F → Functor (J ▹) C
    : (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 is as a functor into the slice category over

    : ∀ {X} → Functor J (Slice C X) → Functor (J ▹) C
    : (F : Functor (J ▹) C) → Functor J (Slice C (F .F₀ (inr _)))
The proofs are by simple data repackaging.
  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 to have universal colimits in the sense of the first diagram above: for every equifibred natural transformation between diagrams if is colimiting then is colimiting.

  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 between diagrams if the bottom diagram (seen as a diagram is colimiting, then the top diagram (seen as a diagram is colimiting.

    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 since the pullback functor is assumed to preserve colimits, we get that 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
        (!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 _ _ _))

For the converse direction, we build a natural transformation from the pullback of to 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!
        α : 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 be colimiting if the bottom diagram is colimiting, disregarding the 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 exist in the forgetful functor both preserves and reflects colimits.

    module _ (J-colims : ∀ (F : Functor J C) → Colimit F) where
        : (F : Functor (J ▹ ▹) C)
        → is-colimit▹ (cocone▹→cocone/ F) ≃ is-colimit▹ (F F∘ ▹-in)
      colim/≃colim F =
          (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 having universal colimits. This follows easily by noticing that retracts onto

    step3→4 : step3 → has-universal-colimits J C
    step3→4 u F G α eq = (function≃ (▹-retract G) (▹-retract F))
      (u _ _ (α ◂ ▹-join) (◂-equifibred ▹-join α eq))
          : (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.

    : (∀ (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


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.

    : ∀ {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)