feat: Remove Extensive in favour of FinitaryExtensive. (#7731)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/CategoryTheory/Extensive.lean

@@ -8,6 +8,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
 import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
 import Mathlib.CategoryTheory.Limits.FunctorCategory
+import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
 import Mathlib.CategoryTheory.Limits.VanKampen
 
 #align_import category_theory.extensive from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
@@ -31,7 +32,9 @@ import Mathlib.CategoryTheory.Limits.VanKampen
 - `CategoryTheory.FinitaryExtensive_TopCat`:
   The category `Top` is extensive.
 - `CategoryTheory.FinitaryExtensive_functor`: The category `C ⥤ D` is extensive if `D`
-  has all pullbacks and is extensive
+  has all pullbacks and is extensive.
+- `CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts`: Finite coproducts in a
+  finitary extensive category are van Kampen.
 ## TODO
 
 Show that the following are finitary extensive:
@@ -58,17 +61,26 @@ section Extensive
 
 variable {X Y : C}
 
-/-- A category is (finitary) extensive if it has finite coproducts,
-and binary coproducts are van Kampen.
+/-- A category is (finitary) pre-extensive if it has finite coproducts,
+and binary coproducts are van Kampen. -/
+class FinitaryPreExtensive (C : Type u) [Category.{v} C] : Prop where
+  [hasFiniteCoproducts : HasFiniteCoproducts C]
+  [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f]
+  /-- In a finitary extensive category, all coproducts are van Kampen-/
+  universal' : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsUniversalColimit c
 
-TODO: Show that this is iff all finite coproducts are van Kampen. -/
+attribute [instance] FinitaryPreExtensive.hasFiniteCoproducts FinitaryPreExtensive.hasPullbackInl
+
+/-- A category is (finitary) extensive if it has finite coproducts,
+and binary coproducts are van Kampen. -/
 class FinitaryExtensive (C : Type u) [Category.{v} C] : Prop where
   [hasFiniteCoproducts : HasFiniteCoproducts C]
+  [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f]
   /-- In a finitary extensive category, all coproducts are van Kampen-/
   van_kampen' : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsVanKampenColimit c
 #align category_theory.finitary_extensive CategoryTheory.FinitaryExtensive
 
-attribute [instance] FinitaryExtensive.hasFiniteCoproducts
+attribute [instance] FinitaryExtensive.hasFiniteCoproducts FinitaryExtensive.hasPullbackInl
 
 theorem FinitaryExtensive.vanKampen [FinitaryExtensive C] {F : Discrete WalkingPair ⥤ C}
     (c : Cocone F) (hc : IsColimit c) : IsVanKampenColimit c := by
@@ -83,6 +95,33 @@ theorem FinitaryExtensive.vanKampen [FinitaryExtensive C] {F : Discrete WalkingP
   exact FinitaryExtensive.van_kampen' c hc
 #align category_theory.finitary_extensive.van_kampen CategoryTheory.FinitaryExtensive.vanKampen
 
+namespace FinitaryPreExtensive
+
+variable [FinitaryPreExtensive C] {X Y Z : C} (f : Z ⟶ X ⨿ Y)
+
+instance hasPullbackInl' :
+    HasPullback f coprod.inl :=
+  hasPullback_symmetry _ _
+
+instance hasPullbackInr' :
+    HasPullback f coprod.inr := by
+  have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom :=
+    IsPullback.of_horiz_isIso ⟨by simp⟩
+  have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this
+  simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc, BinaryCofan.mk_pt,
+    BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this
+  exact ⟨⟨⟨_, this.isLimit⟩⟩⟩
+
+instance hasPullbackInr :
+    HasPullback coprod.inr f :=
+  hasPullback_symmetry _ _
+
+end FinitaryPreExtensive
+
+instance (priority := 100) FinitaryExtensive.toFinitaryPreExtensive [FinitaryExtensive C] :
+    FinitaryPreExtensive C :=
+  ⟨fun c hc ↦ (FinitaryExtensive.van_kampen' c hc).isUniversal⟩
+
 theorem FinitaryExtensive.mono_inr_of_isColimit [FinitaryExtensive C] {c : BinaryCofan X Y}
     (hc : IsColimit c) : Mono c.inr :=
   BinaryCofan.mono_inr_of_isVanKampen (FinitaryExtensive.vanKampen c hc)
@@ -105,18 +144,19 @@ theorem FinitaryExtensive.isPullback_initial_to_binaryCofan [FinitaryExtensive C
   BinaryCofan.isPullback_initial_to_of_isVanKampen (FinitaryExtensive.vanKampen c hc)
 #align category_theory.finitary_extensive.is_pullback_initial_to_binary_cofan CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan
 
-instance (priority := 100) hasStrictInitialObjects_of_finitaryExtensive [FinitaryExtensive C] :
-    HasStrictInitialObjects C :=
-  hasStrictInitial_of_isUniversal (FinitaryExtensive.vanKampen _
+instance (priority := 100) hasStrictInitialObjects_of_finitaryPreExtensive
+    [FinitaryPreExtensive C] : HasStrictInitialObjects C :=
+  hasStrictInitial_of_isUniversal (FinitaryPreExtensive.universal' _
     ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
       dsimp
-      infer_instance)).some).isUniversal
-#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive
+      infer_instance)).some)
+#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive
 
 theorem finitaryExtensive_iff_of_isTerminal (C : Type u) [Category.{v} C] [HasFiniteCoproducts C]
+    [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f]
     (T : C) (HT : IsTerminal T) (c₀ : BinaryCofan T T) (hc₀ : IsColimit c₀) :
     FinitaryExtensive C ↔ IsVanKampenColimit c₀ := by
-  refine' ⟨fun H => H.2 c₀ hc₀, fun H => _⟩
+  refine' ⟨fun H => H.van_kampen' c₀ hc₀, fun H => _⟩
   constructor
   simp_rw [BinaryCofan.isVanKampen_iff] at H ⊢
   intro X Y c hc X' Y' c' αX αY f hX hY
@@ -348,7 +388,8 @@ instance finitaryExtensive_functor [HasPullbacks C] [FinitaryExtensive C] :
     FinitaryExtensive.vanKampen _ <| PreservesColimit.preserves hc⟩
 
 theorem finitaryExtensive_of_preserves_and_reflects (F : C ⥤ D) [FinitaryExtensive D]
-    [HasFiniteCoproducts C] [PreservesLimitsOfShape WalkingCospan F]
+    [HasFiniteCoproducts C] [∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f]
+    [PreservesLimitsOfShape WalkingCospan F]
     [ReflectsLimitsOfShape WalkingCospan F] [PreservesColimitsOfShape (Discrete WalkingPair) F]
     [ReflectsColimitsOfShape (Discrete WalkingPair) F] : FinitaryExtensive C :=
   ⟨fun _ hc => (FinitaryExtensive.vanKampen _ (isColimitOfPreserves F hc)).of_mapCocone F⟩
@@ -366,6 +407,141 @@ theorem finitaryExtensive_of_preserves_and_reflects_isomorphism (F : C ⥤ D) [F
 
 end Functor
 
+section FiniteCoproducts
+
+theorem FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin [FinitaryPreExtensive C] {n : ℕ}
+    {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c := by
+  let f : Fin n → C := F.obj ∘ Discrete.mk
+  have : F = Discrete.functor f :=
+    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp)
+  clear_value f
+  subst this
+  induction' n with n IH
+  · exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal
+  · apply IsUniversalColimit.of_iso _
+      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
+    apply @isUniversalColimit_extendCofan _ _ _ _ _ _ _ _ ?_
+    · apply IH
+      exact coproductIsCoproduct _
+    · apply FinitaryPreExtensive.universal'
+      exact coprodIsCoprod _ _
+    · dsimp
+      infer_instance
+
+theorem FinitaryPreExtensive.isUniversal_finiteCoproducts [FinitaryPreExtensive C] {ι : Type*}
+    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c := by
+  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
+  apply (IsUniversalColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp
+  apply FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin
+  exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc
+
+theorem FinitaryExtensive.isVanKampen_finiteCoproducts_Fin [FinitaryExtensive C] {n : ℕ}
+    {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c := by
+  let f : Fin n → C := F.obj ∘ Discrete.mk
+  have : F = Discrete.functor f :=
+    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp)
+  clear_value f
+  subst this
+  induction' n with n IH
+  · exact isVanKampenColimit_of_isEmpty _ hc
+  · apply IsVanKampenColimit.of_iso _
+      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
+    apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_
+    · apply IH
+      exact coproductIsCoproduct _
+    · apply FinitaryExtensive.van_kampen'
+      exact coprodIsCoprod _ _
+    · dsimp
+      infer_instance
+
+theorem FinitaryExtensive.isVanKampen_finiteCoproducts [FinitaryExtensive C] {ι : Type*}
+    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c := by
+  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
+  apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp
+  apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
+  exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc
+
+lemma FinitaryPreExtensive.hasPullbacks_of_is_coproduct [FinitaryPreExtensive C] {ι : Type*}
+    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) (i : Discrete ι) {X : C}
+    (g : X ⟶ _) : HasPullback g (c.ι.app i) := by
+  classical
+  let f : ι → C := F.obj ∘ Discrete.mk
+  have : F = Discrete.functor f :=
+    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp)
+  clear_value f
+  subst this
+  change Cofan f at c
+  obtain ⟨i⟩ := i
+  let e : ∐ f ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) :=
+  { hom := Sigma.desc (fun j ↦ if h : j = i then eqToHom (congr_arg f h) ≫ coprod.inl else
+      Sigma.ι (fun j : ({i}ᶜ : Set ι) ↦ f j) ⟨j, h⟩ ≫ coprod.inr)
+    inv := coprod.desc (Sigma.ι f i) (Sigma.desc <| fun j ↦ Sigma.ι f j)
+    hom_inv_id := by aesop_cat
+    inv_hom_id := by
+      ext j
+      · simp
+      · simp only [coprod.desc_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
+          eqToHom_refl, Category.id_comp, dite_true, BinaryCofan.mk_pt, BinaryCofan.ι_app_right,
+          BinaryCofan.mk_inr, colimit.ι_desc_assoc, Discrete.functor_obj, Category.comp_id]
+        exact dif_neg j.prop }
+  let e' : c.pt ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) :=
+    hc.coconePointUniqueUpToIso (getColimitCocone _).2 ≪≫ e
+  have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩
+  · simp only [Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt,
+      BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
+    exact colimit.comp_coconePointUniqueUpToIso_inv _ _
+  clear_value e'
+  rw [← this]
+  have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩
+  exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩
+
+lemma FinitaryExtensive.mono_ι [FinitaryExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C}
+    {c : Cocone F} (hc : IsColimit c) (i : Discrete ι) :
+    Mono (c.ι.app i) :=
+  mono_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) _
+
+instance [FinitaryExtensive C] {ι : Type*} [Finite ι] (X : ι → C) (i : ι) :
+    Mono (Sigma.ι X i) :=
+  FinitaryExtensive.mono_ι (coproductIsCoproduct _) ⟨i⟩
+
+lemma FinitaryExtensive.isPullback_initial_to [FinitaryExtensive C]
+    {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C}
+    {c : Cocone F} (hc : IsColimit c) (i j : Discrete ι) (e : i ≠ j) :
+    IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) :=
+  isPullback_initial_to_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) i j e
+
+lemma FinitaryExtensive.isPullback_initial_to_sigma_ι [FinitaryExtensive C] {ι : Type*} [Finite ι]
+    (X : ι → C) (i j : ι) (e : i ≠ j) :
+    IsPullback (initial.to _) (initial.to _) (Sigma.ι X i) (Sigma.ι X j) :=
+  FinitaryExtensive.isPullback_initial_to (coproductIsCoproduct _) ⟨i⟩ ⟨j⟩
+    (ne_of_apply_ne Discrete.as e)
+
+instance FinitaryPreExtensive.hasPullbacks_of_inclusions [FinitaryPreExtensive C] {X Z : C}
+    {α : Type*} (f : X ⟶ Z) {Y : (a : α) → C} (i : (a : α) → Y a ⟶ Z) [Finite α]
+    [hi : IsIso (Sigma.desc i)] (a : α) : HasPullback f (i a) := by
+  apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i)
+  exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) hi
+
+lemma FinitaryPreExtensive.sigma_desc_iso [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C}
+    {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Sigma.desc π)) :
+    IsIso (Sigma.desc ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) := by
+  suffices IsColimit (Cofan.mk _ ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) by
+    change IsIso (this.coconePointUniqueUpToIso (getColimitCocone _).2).inv
+    infer_instance
+  let : IsColimit (Cofan.mk X π)
+  · refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) ?_
+    convert hπ
+    simp [coproductIsCoproduct]
+  refine (FinitaryPreExtensive.isUniversal_finiteCoproducts this
+    (Cofan.mk _ ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _))
+    (Discrete.natTrans <| fun i ↦ pullback.snd) f ?_
+    (NatTrans.equifibered_of_discrete _) ?_).some
+  · ext
+    simp [pullback.condition]
+  · exact fun j ↦ IsPullback.of_hasPullback f (π j.as)
+
+end FiniteCoproducts
+
 end Extensive
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/VanKampen.lean

@@ -133,6 +133,18 @@ theorem IsInitial.isVanKampenColimit [HasStrictInitialObjects C] {X : C} (h : Is
 
 section Functor
 
+theorem IsUniversalColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (hc : IsUniversalColimit c)
+    (e : c ≅ c') : IsUniversalColimit c' := by
+  intro F' c'' α f h hα H
+  have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
+    ext j
+    exact e.inv.2 j
+  apply hc c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα
+  intro j
+  rw [← Category.comp_id (α.app j)]
+  have : IsIso e.inv.hom := Functor.map_isIso (Cocones.forget _) e.inv
+  exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨by simp⟩)
+
 theorem IsVanKampenColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (H : IsVanKampenColimit c)
     (e : c ≅ c') : IsVanKampenColimit c' := by
   intro F' c'' α f h hα
@@ -162,6 +174,18 @@ theorem IsVanKampenColimit.precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIs
   rw [← IsPullback.paste_vert_iff this _, Category.comp_id]
   exact (congr_app e j).symm
 
+theorem IsUniversalColimit.precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α]
+    {c : Cocone G} (hc : IsUniversalColimit c) :
+    IsUniversalColimit ((Cocones.precompose α).obj c) := by
+  intros F' c' α' f e hα H
+  apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e)
+    (hα.comp (NatTrans.equifibered_of_isIso _)))
+  intro j
+  simp only [Functor.const_obj_obj, NatTrans.comp_app,
+    Cocones.precompose_obj_pt, Cocones.precompose_obj_ι]
+  rw [← Category.comp_id f]
+  exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨Category.comp_id _⟩)
+
 theorem IsVanKampenColimit.precompose_isIso_iff {F G : J ⥤ C} (α : F ⟶ G) [IsIso α]
     {c : Cocone G} : IsVanKampenColimit ((Cocones.precompose α).obj c) ↔ IsVanKampenColimit c :=
   ⟨fun hc ↦ IsVanKampenColimit.of_iso (IsVanKampenColimit.precompose_isIso (inv α) hc)
@@ -189,6 +213,28 @@ theorem IsVanKampenColimit.mapCocone_iff (G : C ⥤ D) {F : J ⥤ C} {c : Cocone
     refine hc.of_iso (Cocones.ext (G.asEquivalence.unitIso.app c.pt) ?_)
     simp [Functor.asEquivalence]⟩
 
+theorem IsUniversalColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K)
+    {F : K ⥤ C} {c : Cocone F} (hc : IsUniversalColimit c) :
+    IsUniversalColimit (c.whisker e.functor) := by
+  intro F' c' α f e' hα H
+  convert hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
+    ((hα.whiskerLeft _).comp (NatTrans.equifibered_of_isIso _)) ?_ using 1
+  · exact (IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr
+  · convert congr_arg (whiskerLeft e.inverse) e'
+    ext
+    simp
+  · intro k
+    rw [← Category.comp_id f]
+    refine (H (e.inverse.obj k)).paste_vert ?_
+    have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance
+    exact IsPullback.of_vert_isIso ⟨by simp⟩
+
+theorem IsUniversalColimit.whiskerEquivalence_iff {K : Type*} [Category K] (e : J ≌ K)
+    {F : K ⥤ C} {c : Cocone F} :
+    IsUniversalColimit (c.whisker e.functor) ↔ IsUniversalColimit c :=
+  ⟨fun hc ↦ ((hc.whiskerEquivalence e.symm).precompose_isIso (e.invFunIdAssoc F).inv).of_iso
+      (Cocones.ext (Iso.refl _) (by simp)), IsUniversalColimit.whiskerEquivalence e⟩
+
 theorem IsVanKampenColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K)
     {F : K ⥤ C} {c : Cocone F} (hc : IsVanKampenColimit c) :
     IsVanKampenColimit (c.whisker e.functor) := by
@@ -659,6 +705,62 @@ theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
       BinaryCofan.ι_app_right, BinaryCofan.mk_inr, colimit.ι_desc,
       Discrete.natTrans_app] using t₁'.paste_horiz (t₂' ⟨WalkingPair.right⟩)
 
+theorem isPullback_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {X : ι → C}
+    {c : Cofan X} (hc : IsVanKampenColimit c) (i j : ι) [DecidableEq ι] :
+    IsPullback (P := (if j = i then X i else ⊥_ C))
+      (if h : j = i then eqToHom (if_pos h) else eqToHom (if_neg h) ≫ initial.to (X i))
+      (if h : j = i then eqToHom ((if_pos h).trans (congr_arg X h.symm))
+        else eqToHom (if_neg h) ≫ initial.to (X j))
+      (Cofan.inj c i) (Cofan.inj c j) := by
+  refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
+    (fun k ↦ if h : k = i then (eqToHom $ if_pos h) else (eqToHom $ if_neg h) ≫ initial.to _))
+    (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom $ (if_pos h).trans
+      (congr_arg X h.symm)) else (eqToHom $ if_neg h) ≫ initial.to _))
+    (c.inj i) ?_ (NatTrans.equifibered_of_discrete _)).mp ⟨?_⟩ ⟨j⟩
+  · ext ⟨k⟩
+    simp only [Discrete.functor_obj, Functor.const_obj_obj, NatTrans.comp_app,
+      Discrete.natTrans_app, Cofan.mk_pt, Cofan.mk_ι_app, Functor.const_map_app]
+    split
+    · subst ‹k = i›; rfl
+    · simp
+  · refine mkCofanColimit _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_
+    · intro t j
+      simp only [Cofan.mk_pt, cofan_mk_inj]
+      split
+      · subst ‹j = i›; simp
+      · rw [Category.assoc, ← IsIso.eq_inv_comp]
+        exact initialIsInitial.hom_ext _ _
+    · intro t m hm
+      simp [← hm i]
+
+theorem isPullback_initial_to_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C}
+    {c : Cocone F} (hc : IsVanKampenColimit c) (i j : Discrete ι) (hi : i ≠ j) :
+    IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) := by
+  classical
+  let f : ι → C := F.obj ∘ Discrete.mk
+  have : F = Discrete.functor f :=
+    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp)
+  clear_value f
+  subst this
+  convert isPullback_of_cofan_isVanKampen hc i.as j.as
+  exact (if_neg (mt (Discrete.ext _ _) hi.symm)).symm
+
+theorem mono_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C}
+    {c : Cocone F} (hc : IsVanKampenColimit c) (i : Discrete ι) : Mono (c.ι.app i) := by
+  classical
+  let f : ι → C := F.obj ∘ Discrete.mk
+  have : F = Discrete.functor f :=
+    Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp)
+  clear_value f
+  subst this
+  refine' PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit _)
+  nth_rw 1 [← Category.id_comp (c.ι.app i)]
+  convert IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as)
+  swap
+  · exact (eqToHom (if_pos rfl).symm)
+  · simp
+  · exact IsPullback.of_vert_isIso ⟨by simp⟩
+
 end FiniteCoproducts
 
 end CategoryTheory