open import Cat.Functor.Naturality.Reflection
open import Cat.Diagram.Pullback.Properties
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 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.

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

Note

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.

Source

This is essentially a 1-categorical version of the proof of lemma 6.1.3.3 in Higher Topos Theory .

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

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 is as a functor into the slice category over

  cocone/→cocone▹
: ∀ {X} → Functor J (Slice C X) → Functor (J ▹) C
cocone▹→cocone/
: (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.

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