Loogle!

Result

Found 180 declarations mentioning CategoryTheory.Limits.Cofan.

• CategoryTheory.Limits.Cofan 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) : Type (max (max w u) v)
• CategoryTheory.Limits.Cofan.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : CategoryTheory.Limits.Cofan f
• CategoryTheory.Limits.hasCoproducts_of_colimit_cofans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (cf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Cofan f) (cf_isColimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsColimit (cf f)) : CategoryTheory.Limits.HasCoproducts C
• CategoryTheory.Limits.Cofan.inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Cofan f) (j : β) : f j ⟶ p.pt
• CategoryTheory.Limits.Cofan.IsColimit.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) : c.pt ⟶ A
• CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)] : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)
• CategoryTheory.Limits.Cofan.IsColimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i
• CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Cofan f) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun i => c.inj (ε i))
• CategoryTheory.Limits.Cofan.IsColimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Cofan X) : CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (F.obj c.pt) fun i => F.map (c.inj i))
• CategoryTheory.Limits.Cofan.IsColimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f g : c.pt ⟶ A) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) : f = g
• CategoryTheory.Limits.Cofan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) = CategoryTheory.CategoryStruct.comp (d.inj i) h
• CategoryTheory.Limits.Cofan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (CategoryTheory.Limits.Cofan.ext e w).hom.hom = e.hom
• CategoryTheory.Limits.Cofan.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (CategoryTheory.Limits.Cofan.ext e w).inv.hom = e.inv
• CategoryTheory.Limits.Cofan.isColimitTrans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) {β : α → Type u_1} {Y : (a : α) → β a → C} (π : (a : α) → (b : β a) → Y a b ⟶ X a) (hs : (a : α) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (X a) (π a))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun x => match x with | ⟨a, b⟩ => CategoryTheory.CategoryStruct.comp (π a b) (c.inj a))
• CategoryTheory.Limits.Cofan.IsColimit.prod 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → CategoryTheory.Limits.Cofan fun j => X i j) (hc : (i : ι) → CategoryTheory.Limits.IsColimit (c i)) (c' : CategoryTheory.Limits.Cofan fun i => (c i).pt) (hc' : CategoryTheory.Limits.IsColimit c') : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c'.pt fun p => CategoryTheory.CategoryStruct.comp ((c p.1).inj p.2) (c'.inj p.1))
• CategoryTheory.Limits.mkCofanColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) : CategoryTheory.Limits.IsColimit s
• CategoryTheory.Limits.Cofan.IsColimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) : CategoryTheory.Limits.IsColimit s
• CategoryTheory.Limits.Cofan.IsColimit.mk_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) (t : CategoryTheory.Limits.Cofan f) : (CategoryTheory.Limits.Cofan.IsColimit.mk s desc fac uniq).desc t = desc t
• ModuleCat.finsuppCocone 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
  (R : Type w) [CommRing R] (M ι : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Limits.Cofan fun x => ModuleCat.of R M
• CategoryTheory.extendCofan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : CategoryTheory.Limits.Cofan f
• CategoryTheory.extendCofan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendCofanIsColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.extendCofan_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as
• ModuleCat.coproductCocone 📋 Mathlib.Algebra.Category.ModuleCat.Products
  {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] : CategoryTheory.Limits.Cofan Z
• CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) : (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).pt = i.pt
• CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) {i : CategoryTheory.Limits.Cofork s t} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) (hi : CategoryTheory.Limits.IsColimit i) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i)
• CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) (x✝ : J) : (CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit s t hs ht i).ι.app x✝ = CategoryTheory.CategoryStruct.comp (c₂.ι.app { as := x✝ }) i.π
• CategoryTheory.Limits.Cofan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (c : CategoryTheory.Limits.Cofan Z) : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)
• CategoryTheory.Limits.Fan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (f : CategoryTheory.Limits.Fan Z) : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)
• CategoryTheory.Limits.Cofan.IsColimit.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit c.op
• CategoryTheory.Limits.opCoproductIsoProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) : Opposite.op c.pt ≅ f.pt
• CategoryTheory.Limits.opProductIsoCoproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) : Opposite.op f.pt ≅ c.pt
• CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (f.proj i) = (c.inj i).op
• CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b
• CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (b : α) : CategoryTheory.CategoryStruct.comp (f.proj b).op (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = c.inj b
• CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (c' : CategoryTheory.Limits.Cofan Z) : CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
• CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (f' : CategoryTheory.Limits.Fan Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
• CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (i : α) {Z✝ : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (CategoryTheory.CategoryStruct.comp (f.proj i) h) = CategoryTheory.CategoryStruct.comp (c.inj i).op h
• CategoryTheory.Limits.opCoproductIsoProduct'_comp_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c c' : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hc' : CategoryTheory.Limits.IsColimit c') (hf : CategoryTheory.Limits.IsLimit f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom (CategoryTheory.Limits.opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
• CategoryTheory.Limits.opProductIsoCoproduct'_comp_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f f' : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hf' : CategoryTheory.Limits.IsLimit f') (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom (CategoryTheory.Limits.opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
• CategoryTheory.isSeparator_of_isColimit_cofan 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} (hf : (CategoryTheory.ObjectProperty.ofObj f).IsSeparating) {c : CategoryTheory.Limits.Cofan f} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.IsSeparator c.pt
• CategoryTheory.isSeparator_iff_of_isColimit_cofan 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} {f : β → C} {c : CategoryTheory.Limits.Cofan f} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.IsSeparator c.pt ↔ (CategoryTheory.ObjectProperty.ofObj f).IsSeparating
• CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} (hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.Epi p) : P.IsSeparating
• CategoryTheory.Limits.Cofan.cofanTypes 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) : CategoryTheory.Limits.CofanTypes F
• CategoryTheory.Limits.Cofan.cofanTypes_pt 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) : c.cofanTypes.pt = c.pt
• CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) : CategoryTheory.Functor.CoconeTypes.IsColimit c.cofanTypes ↔ Nonempty (CategoryTheory.Limits.IsColimit c)
• CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_bijective_fromSigma 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Bijective (CategoryTheory.Limits.CofanTypes.fromSigma F c.cofanTypes)
• CategoryTheory.Limits.Cofan.inj_injective_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) (i : C) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (c.inj i))
• CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) (x : c.pt) : ∃ i y, (CategoryTheory.ConcreteCategory.hom (c.inj i)) y = x
• CategoryTheory.Limits.Cofan.cofanTypes_ι 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.Cofan F) (x✝ : CategoryTheory.Discrete C) (a✝ : (CategoryTheory.Discrete.functor F).obj x✝) : c.cofanTypes.ι x✝ a✝ = (match (motive := (x : CategoryTheory.Discrete C) → (CategoryTheory.Discrete.functor F).obj x → c.pt) x✝ with | { as := j } => ⇑(CategoryTheory.ConcreteCategory.hom (c.inj j))) a✝
• CategoryTheory.Limits.Cofan.eq_of_inj_apply_eq_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) (h : (CategoryTheory.ConcreteCategory.hom (c.inj i₁)) y₁ = (CategoryTheory.ConcreteCategory.hom (c.inj i₂)) y₂) : i₁ = i₂
• CategoryTheory.Limits.Cofan.inj_apply_eq_iff_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {i j : C} (x : F i) (y : F j) : (CategoryTheory.ConcreteCategory.hom (c.inj i)) x = (CategoryTheory.ConcreteCategory.hom (c.inj j)) y ↔ ∃ (hij : i = j), y = cast ⋯ x
• CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
• CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) : c.pt ⟶ d.pt
• CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) : c.pt ⟶ d.pt
• CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (x : CategoryTheory.Limits.WalkingParallelPair) : (I.parallelPairDiagramOfIsColimit d hc).obj x = CategoryTheory.Limits.parallelPair.parallelPairObj c.pt d.pt x
• CategoryTheory.Limits.Multicofork.ofSigmaCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} {hc : CategoryTheory.Limits.IsColimit c} {d : CategoryTheory.Limits.Cofan I.right} (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : CategoryTheory.Limits.Multicofork I
• CategoryTheory.Limits.Multicofork.toSigmaCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) (K : CategoryTheory.Limits.Multicofork I) : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
• CategoryTheory.Limits.Multicofork.toSigmaCofork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) (K : CategoryTheory.Limits.Multicofork I) : (CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K).pt = K.pt
• CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} : CategoryTheory.Functor (CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (CategoryTheory.Limits.Multicofork I)
• CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} {hc : CategoryTheory.Limits.IsColimit c} {d : CategoryTheory.Limits.Cofan I.right} (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).pt = a.pt
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : CategoryTheory.Limits.Multicofork I ≌ CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)
• CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Multicofork I) (CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))
• CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) : CategoryTheory.CategoryStruct.comp (c.inj i) (I.fstSigmaMapOfIsColimit d hc) = CategoryTheory.CategoryStruct.comp (I.fst i) (d.inj (J.fst i))
• CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) : CategoryTheory.CategoryStruct.comp (c.inj i) (I.sndSigmaMapOfIsColimit d hc) = CategoryTheory.CategoryStruct.comp (I.snd i) (d.inj (J.snd i))
• CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : (I.parallelPairDiagramOfIsColimit d hc).map h = CategoryTheory.Limits.parallelPair.parallelPairHom (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc) h
• CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) h) = CategoryTheory.CategoryStruct.comp (I.fst i) (CategoryTheory.CategoryStruct.comp (d.inj (J.fst i)) h)
• CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) h) = CategoryTheory.CategoryStruct.comp (I.snd i) (CategoryTheory.CategoryStruct.comp (d.inj (J.snd i)) h)
• CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : (I.ofSigmaCoforkFunctor hc).obj a = CategoryTheory.Limits.Multicofork.ofSigmaCofork a
• CategoryTheory.Limits.Multicofork.toSigmaCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : (CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K).π = CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π
• CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) (K : CategoryTheory.Limits.Multicofork I) : (I.toSigmaCoforkFunctor hc hd).obj K = CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K
• CategoryTheory.Limits.Multicofork.sigma_condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) = CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π)
• CategoryTheory.Limits.Multicofork.ofSigmaCofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.R) : (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).π i = CategoryTheory.CategoryStruct.comp (d.inj i) a.π
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).inverse = I.ofSigmaCoforkFunctor hc
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).functor = I.toSigmaCoforkFunctor hc hd
• CategoryTheory.Limits.Multicofork.sigma_condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) {Z : C} (h : K.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) h) = CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) h)
• CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) {K₁ K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂) : ((I.toSigmaCoforkFunctor hc hd).map f).hom = f.hom
• CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.L) : (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).ι.app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) a.π)
• CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} {K₁ K₂ : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)} (f : K₁ ⟶ K₂) : ((I.ofSigmaCoforkFunctor hc).map f).hom = f.hom
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multicofork I)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl (((I.ofSigmaCoforkFunctor hc).comp (I.toSigmaCoforkFunctor hc hd)).obj K).pt) ⋯) ⋯
• CategoryTheory.GradedObject.cofanMapObjComp 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = k → X.CofanMapObjFun p j) (c' : CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt) : X.CofanMapObjFun r k
• CategoryTheory.GradedObject.isColimitCofanMapObjComp 📋 Mathlib.CategoryTheory.GradedObject
  {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [CategoryTheory.Category.{v_1, u_4} C] (X : CategoryTheory.GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = k → X.CofanMapObjFun p j) (hc : (j : J) → (hj : q j = k) → CategoryTheory.Limits.IsColimit (c j hj)) (c' : CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt) (hc' : CategoryTheory.Limits.IsColimit c') : CategoryTheory.Limits.IsColimit (X.cofanMapObjComp p q r hpqr k c c')
• CategoryTheory.ObjectProperty.prop_of_isColimit_cofan 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C} {F : CategoryTheory.Limits.Cofan f} (hF : CategoryTheory.Limits.IsColimit F) (h : ∀ (j : J), P (f j)) : P F.pt
• TopCat.sigmaCofan 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {ι : Type v} (α : ι → TopCat) : CategoryTheory.Limits.Cofan α
• CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ B) (q₂ : (i : ι) → P i ⟶ X i) (hP : ∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) v (f i)) {d : CategoryTheory.Limits.Cofan P} (hd : CategoryTheory.Limits.IsColimit d) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) [CategoryTheory.Limits.HasPullback v u] : CategoryTheory.IsPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hd q₁) (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (q₂ x) (a.inj x)) v u
• CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ X i) (q₂ : (i : ι) → P i ⟶ B) (hP : ∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) (f i) v) {d : CategoryTheory.Limits.Cofan P} (hd : CategoryTheory.Limits.IsColimit d) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) [CategoryTheory.Limits.HasPullback u v] : CategoryTheory.IsPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (q₁ x) (a.inj x)) (CategoryTheory.Limits.Cofan.IsColimit.desc hd q₂) u v
• CategoryTheory.isPullback_of_cofan_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {ι : Type u_3} {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.IsVanKampenColimit c) (i j : ι) [DecidableEq ι] : CategoryTheory.IsPullback (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X i))) (if h : j = i then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X j))) (c.inj i) (c.inj j)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ B) (q₂ : (i : ι) → P i ⟶ X i) (hP : ∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) v (f i)) {Z : C} {p₁ : Z ⟶ B} {p₂ : Z ⟶ a.pt} (h : CategoryTheory.IsPullback p₁ p₂ v u) (d : CategoryTheory.Limits.Cofan P) (e : d.pt ≅ Z) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (he₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₁) = q₁ i := by cat_disch) (he₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₂) = CategoryTheory.CategoryStruct.comp (q₂ i) (a.inj i) := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ X i) (q₂ : (i : ι) → P i ⟶ B) (hP : ∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) (f i) v) {Z : C} {p₁ : Z ⟶ a.pt} {p₂ : Z ⟶ B} (h : CategoryTheory.IsPullback p₁ p₂ u v) (d : CategoryTheory.Limits.Cofan P) (e : d.pt ≅ Z) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (he₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₁) = CategoryTheory.CategoryStruct.comp (q₁ i) (a.inj i) := by cat_disch) (he₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₂) = q₂ i := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y} (hbu : CategoryTheory.IsUniversalColimit b) (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S) [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] [CategoryTheory.Limits.HasPullback u v] {P : ι × ι' → C} {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j} (hP : ∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) (d : CategoryTheory.Limits.Cofan P) (hd : CategoryTheory.Limits.IsColimit d) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (hv : ∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i := by cat_disch) : CategoryTheory.IsPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p => CategoryTheory.CategoryStruct.comp (q₁ p.1 p.2) (a.inj p.1)) (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p => CategoryTheory.CategoryStruct.comp (q₂ p.1 p.2) (b.inj p.2)) u v
• CategoryTheory.isUniversalColimit_extendCofan 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.IsUniversalColimit c₁) (t₂ : CategoryTheory.IsUniversalColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i] : CategoryTheory.IsUniversalColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.isVanKampenColimit_extendCofan 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.IsVanKampenColimit c₁) (t₂ : CategoryTheory.IsVanKampenColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.IsVanKampenColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y} (hbu : CategoryTheory.IsUniversalColimit b) (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S) [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] {P : ι × ι' → C} {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j} (hP : ∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) {Z : C} {p₁ : Z ⟶ a.pt} {p₂ : Z ⟶ b.pt} (h : CategoryTheory.IsPullback p₁ p₂ u v) {d : CategoryTheory.Limits.Cofan P} (e : d.pt ≅ Z) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (hv : ∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i := by cat_disch) (he₁ : ∀ (i : ι) (j : ι'), CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom p₁) = CategoryTheory.CategoryStruct.comp (q₁ i j) (a.inj i) := by cat_disch) (he₂ : ∀ (i : ι) (j : ι'), CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom p₂) = CategoryTheory.CategoryStruct.comp (q₂ i j) (b.inj j) := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) (s : (i : ι) → CategoryTheory.Limits.PullbackCone v (f i)) (hs : (i : ι) → CategoryTheory.Limits.IsLimit (s i)) (t : CategoryTheory.Limits.PullbackCone v u) (ht : CategoryTheory.Limits.IsLimit t) (d : CategoryTheory.Limits.Cofan fun i => (s i).pt) (e : d.pt ≅ t.pt) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (he₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.fst) = (s i).fst := by cat_disch) (he₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.snd) = CategoryTheory.CategoryStruct.comp (s i).snd (a.inj i) := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) (s : (i : ι) → CategoryTheory.Limits.PullbackCone (f i) v) (hs : (i : ι) → CategoryTheory.Limits.IsLimit (s i)) (t : CategoryTheory.Limits.PullbackCone u v) (ht : CategoryTheory.Limits.IsLimit t) (d : CategoryTheory.Limits.Cofan fun i => (s i).pt) (e : d.pt ≅ t.pt) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (he₁ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.fst) = CategoryTheory.CategoryStruct.comp (s i).fst (a.inj i) := by cat_disch) (he₂ : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.snd) = (s i).snd := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C} {a : CategoryTheory.Limits.Cofan X} (hau : CategoryTheory.IsUniversalColimit a) {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y} (hbu : CategoryTheory.IsUniversalColimit b) (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S) [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] (s : (i : ι) → (j : ι') → CategoryTheory.Limits.PullbackCone (f i) (g j)) (hs : (i : ι) → (j : ι') → CategoryTheory.Limits.IsLimit (s i j)) (t : CategoryTheory.Limits.PullbackCone u v) (ht : CategoryTheory.Limits.IsLimit t) {d : CategoryTheory.Limits.Cofan fun p => (s p.1 p.2).pt} (e : d.pt ≅ t.pt) (hu : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i := by cat_disch) (hv : ∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i := by cat_disch) (he₁ : ∀ (i : ι) (j : ι'), CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom t.fst) = CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).fst (a.inj (i, j).1) := by cat_disch) (he₂ : ∀ (i : ι) (j : ι'), CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom t.snd) = CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).snd (b.inj (i, j).2) := by cat_disch) : Nonempty (CategoryTheory.Limits.IsColimit d)
• CategoryTheory.Limits.MonoCoprod.mono_inj 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} (X : I → C) (c : CategoryTheory.Limits.Cofan X) (h : CategoryTheory.Limits.IsColimit c) (i : I) [CategoryTheory.Limits.HasCoproduct fun k => X ↑k] : CategoryTheory.Mono (c.inj i)
• CategoryTheory.Limits.MonoCoprod.binaryCofanSum 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt
• CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂)
• CategoryTheory.Limits.MonoCoprod.mono_of_injective 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) [CategoryTheory.Limits.HasCoproduct fun k => X ↑k] : CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
• CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cofan fun k => X ↑k) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
• CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] : CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
• CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] : CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
• CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl' 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] (inl : c₁.pt ⟶ c.pt) (hinl : ∀ (i₁ : I₁), CategoryTheory.CategoryStruct.comp (c₁.inj i₁) inl = c.inj (Sum.inl i₁)) : CategoryTheory.Mono inl
• CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr' 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] (inr : c₂.pt ⟶ c.pt) (hinr : ∀ (i₂ : I₂), CategoryTheory.CategoryStruct.comp (c₂.inj i₂) inr = c.inj (Sum.inr i₂)) : CategoryTheory.Mono inr
• CategoryTheory.Mono.of_coproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι) : CategoryTheory.Mono (c.inj i)
• CategoryTheory.Limits.CoproductDisjoint.mono_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {ι : Type u_1} {X : ι → C} [self : CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι) : CategoryTheory.Mono (c.inj i)
• CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {Y : C} (hY : CategoryTheory.Limits.IsInitial Y) {i j : ι} [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] (hij : i ≠ j) : CategoryTheory.IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimitOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {ι : Type u_1} {X : ι → C} [self : CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {i j : ι} : i ≠ j → ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s), Nonempty (CategoryTheory.Limits.IsInitial s.pt)
• CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfCommSq 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [CategoryTheory.Limits.HasStrictInitialObjects C] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {Z : C} (fst : Z ⟶ X i) (snd : Z ⟶ X j) (h : CategoryTheory.CategoryStruct.comp fst (c.inj i) = CategoryTheory.CategoryStruct.comp snd (c.inj j)) [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] : CategoryTheory.Limits.IsInitial Z
• CategoryTheory.Limits.CoproductDisjoint.of_cofan 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) [∀ (i : ι), CategoryTheory.Mono (c.inj i)] (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij)) (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt) : CategoryTheory.Limits.CoproductDisjoint X
• CategoryTheory.Limits.CoproductDisjoint.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} (nonempty_isInitial_of_ne : ∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {i j : ι}, i ≠ j → ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s), Nonempty (CategoryTheory.Limits.IsInitial s.pt)) (mono_inj : ∀ {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι), CategoryTheory.Mono (c.inj i)) : CategoryTheory.Limits.CoproductDisjoint X
• CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C} {ι : Type u_2} [Small.{max w v, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S) {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.uliftYoneda.{w, v, u}.obj (X i)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Sieve.ofArrows X f ∈ J S ↔ CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.uliftYoneda.{w, v, u}.map (f i))
• CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.LocallySmall.{w, v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S) {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Sieve.ofArrows X f ∈ J S ↔ CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))
• CategoryTheory.Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S) [CategoryTheory.LocallySmall.{w, v, u} C] {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)} (hc : CategoryTheory.Limits.IsColimit c) {U : C} (g : U ⟶ S) : CategoryTheory.Presheaf.imageSieve (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i)) (CategoryTheory.shrinkYonedaObjObjEquiv.symm g) = CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.ofArrows X f)
• SheafOfModules.freeCofan 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : CategoryTheory.Limits.Cofan fun x => SheafOfModules.unit R
• CategoryTheory.PreZeroHypercover.sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.PreZeroHypercover S
• CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : (E.sigmaOfIsColimit hc).I₀ = PUnit.{w + 1}
• CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x✝ : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc).X x✝ = c.pt
• CategoryTheory.PreZeroHypercover.presieve₀_sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) : (E.sigmaOfIsColimit hc).presieve₀ = CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f)
• CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x✝ : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc).f x✝ = CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f
• CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) : CategoryTheory.CategoryStruct.comp (c.inj i) ((E.sigmaOfIsColimit hc).f r) = E.f i
• CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) {Z : C} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc).f r) h) = CategoryTheory.CategoryStruct.comp (E.f i) h
• CategoryTheory.PreOneHypercover.sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : CategoryTheory.PreOneHypercover S
• CategoryTheory.PreOneHypercover.instUniqueLMulticospanShapeSigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.L
• CategoryTheory.PreOneHypercover.instUniqueRMulticospanShapeSigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.R
• CategoryTheory.PreOneHypercover.sigmaOfIsColimit_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) : (E.sigmaOfIsColimit hc hd).toPreZeroHypercover = E.sigmaOfIsColimit hc
• CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (x✝ x✝¹ : (E.sigmaOfIsColimit hc).I₀) (x✝² : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc hd).Y x✝² = d.pt
• CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] : CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ CategoryTheory.Limits.IsLimit (E.multifork F)
• CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) {Z : C} (h : (E.sigmaOfIsColimit hc hd).X a ⟶ Z) : CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₁ r) h) = CategoryTheory.CategoryStruct.comp (E.p₁ i.snd) (CategoryTheory.CategoryStruct.comp (c.inj i.fst.1) h)
• CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) {Z : C} (h : (E.sigmaOfIsColimit hc hd).X b ⟶ Z) : CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₂ r) h) = CategoryTheory.CategoryStruct.comp (E.p₂ i.snd) (CategoryTheory.CategoryStruct.comp (c.inj i.fst.2) h)
• CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) : CategoryTheory.CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₁ r) = CategoryTheory.CategoryStruct.comp (E.p₁ i.snd) (c.inj i.fst.1)
• CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) : CategoryTheory.CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₂ r) = CategoryTheory.CategoryStruct.comp (E.p₂ i.snd) (c.inj i.fst.2)
• CategoryTheory.PreOneHypercover.forkOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Limits.Fork (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (E.p₁ x.snd) (c.inj x.fst.1)).op) (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (E.p₂ x.snd) (c.inj x.fst.2)).op)
• CategoryTheory.PreOneHypercover.forkOfIsColimit_pt 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) : (E.forkOfIsColimit hc hd F).pt = F.obj (Opposite.op S)
• CategoryTheory.PreOneHypercover.isLimitMultiforkEquivIsLimitFork 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F] : CategoryTheory.Limits.IsLimit (E.multifork F) ≃ CategoryTheory.Limits.IsLimit (E.forkOfIsColimit hc hd F)
• CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι (F.map (c.inj i).op) = F.map (E.f i).op
• CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀) {Z : A} (h : F.obj (Opposite.op (E.X i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι (CategoryTheory.CategoryStruct.comp (F.map (c.inj i).op) h) = CategoryTheory.CategoryStruct.comp (F.map (E.f i).op) h
• CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff 📋 Mathlib.CategoryTheory.Sites.CoproductSheafCondition
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} {ι : Type u_3} {X : ι → C} (f : (i : ι) → X i ⟶ S) [(CategoryTheory.Presieve.ofArrows X f).HasPairwisePullbacks] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (hc' : CategoryTheory.IsUniversalColimit c) [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)] [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)] (F : CategoryTheory.Functor Cᵒᵖ (Type u_4)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun ij => Opposite.op (CategoryTheory.Limits.pullback (f ij.1) (f ij.2))) F] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X f)
• CategoryTheory.PreZeroHypercover.isLimitSigmaOfIsColimitEquiv 📋 Mathlib.CategoryTheory.Sites.CoproductSheafCondition
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (huniv : CategoryTheory.IsUniversalColimit c) [(E.sigmaOfIsColimit hc).HasPullbacks] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)] (F : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.toPreOneHypercover.X i)) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.toPreOneHypercover.Y' i)) F] : CategoryTheory.Limits.IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)
• CategoryTheory.Presieve.isSheafFor_of_preservesProduct 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)
• CategoryTheory.Presieve.preservesProduct_of_isSheafFor 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) (hF' : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.isSheafFor_iff_preservesProduct 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔ CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
• CategoryTheory.Presieve.firstMap_eq_secondMap 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [CategoryTheory.Limits.HasInitial C] [∀ (i : α), CategoryTheory.Mono (c.inj i)] (hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) : CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj = CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
• CategoryTheory.Presieve.piComparison_fac 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type u_1} [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) : have this := ⋯; (CategoryTheory.Limits.piComparison F fun x => Opposite.op (X x)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.opCoproductIsoProduct' hc (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (X x))).inv) (CategoryTheory.Equalizer.Presieve.Arrows.forkMap F X c.inj)
• CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} [CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasStrictInitialObjects C] (hcov : ∀ {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) (htriv : ∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) J.yoneda
• CategoryTheory.GrothendieckTopology.isColimitCofanMkYoneda 📋 Mathlib.CategoryTheory.Sites.Subcanonical
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {ι : Type u_1} (X : ι → C) {c : CategoryTheory.Limits.Cofan X} (H : CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) [∀ (i : ι), CategoryTheory.Mono (c.inj i)] (hempty : ∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) (hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), CategoryTheory.CategoryStruct.comp a (c.inj i) = CategoryTheory.CategoryStruct.comp b (c.inj j) → Nonempty (CategoryTheory.Limits.IsInitial Y)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i))
• HomotopicalAlgebra.AttachCells.cofan₁ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : HomotopicalAlgebra.AttachCells g f) : CategoryTheory.Limits.Cofan fun i => A (self.π i)
• HomotopicalAlgebra.AttachCells.cofan₂ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : HomotopicalAlgebra.AttachCells g f) : CategoryTheory.Limits.Cofan fun i => B (self.π i)
• HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₁ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).cofan₁ = c.cofan₁
• HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₂ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).cofan₂ = c.cofan₂
• HomotopicalAlgebra.AttachCells.mk 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (ι : Type w) (π : ι → α) (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)) (isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁) (isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂) (m : cofan₁.pt ⟶ cofan₂.pt) (hm : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m = CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i) := by cat_disch) (g₁ : cofan₁.pt ⟶ X₁) (g₂ : cofan₂.pt ⟶ X₂) (isPushout : CategoryTheory.IsPushout g₁ m f g₂) : HomotopicalAlgebra.AttachCells g f
• HomotopicalAlgebra.AttachCells.reindex_cofan₁ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).cofan₁ = CategoryTheory.Limits.Cofan.mk c.cofan₁.pt fun i' => c.cofan₁.inj (e i')
• HomotopicalAlgebra.AttachCells.reindex_cofan₂ 📋 Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).cofan₂ = CategoryTheory.Limits.Cofan.mk c.cofan₂.pt fun i' => c.cofan₂.inj (e i')
• CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₁ = CategoryTheory.Limits.Cofan.mk (∐ fun i => A i.i) (CategoryTheory.Limits.Sigma.ι fun i => A i.i)
• CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂ 📋 Mathlib.CategoryTheory.SmallObject.Construction
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₂ = CategoryTheory.Limits.Cofan.mk (∐ fun i => B i.i) (CategoryTheory.Limits.Sigma.ι fun i => B i.i)
• CategoryTheory.SimplicialObject.Splitting.cofan 📋 Mathlib.AlgebraicTopology.SimplicialObject.Split
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting) (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.Cofan (CategoryTheory.SimplicialObject.Splitting.summand s.N Δ)
• CategoryTheory.SimplicialObject.Splitting.cofan' 📋 Mathlib.AlgebraicTopology.SimplicialObject.Split
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (N : ℕ → C) (X : CategoryTheory.SimplicialObject C) (φ : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n })) (Δ : SimplexCategoryᵒᵖ) : CategoryTheory.Limits.Cofan (CategoryTheory.SimplicialObject.Splitting.summand N Δ)
• SSet.relativeCellComplexOfMono_attachCells_cofan₂ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
  {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((SSet.relativeCellComplexOfMono i).attachCells d x✝).cofan₂ = CategoryTheory.Limits.Cofan.mk (∐ fun i => SSet.stdSimplex.obj { len := d }) (CategoryTheory.Limits.Sigma.ι fun i => SSet.stdSimplex.obj { len := d })
• SSet.relativeCellComplexOfMono_attachCells_cofan₁ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
  {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] (d : ℕ) (x✝ : ¬IsMax d) : ((SSet.relativeCellComplexOfMono i).attachCells d x✝).cofan₁ = CategoryTheory.Limits.Cofan.mk (∐ fun i => (SSet.boundary d).toSSet) (CategoryTheory.Limits.Sigma.ι fun i => (SSet.boundary d).toSSet)
• CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_extremalEpi 📋 Mathlib.CategoryTheory.Generator.StrongGenerator
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.ExtremalEpi p) : P.IsStrongGenerator
• CategoryTheory.ObjectProperty.isStrongGenerator_iff_exists_extremalEpi 📋 Mathlib.CategoryTheory.Generator.StrongGenerator
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.ObjectProperty.Small.{w, v, u} P] : P.IsStrongGenerator ↔ ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.ExtremalEpi p
• SSet.chainComplexXCofan 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.Limits.Cofan fun x => R
• SSet.cofanNormalizedChainComplex 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) : CategoryTheory.Limits.Cofan fun x => R
• CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily 📋 Mathlib.CategoryTheory.EffectiveEpi.Coproduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} (X : α → C) (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiStruct (hc.desc (CategoryTheory.Limits.Cofan.mk B π))
• CategoryTheory.Limits.Cofan.combPairHoms 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} (c₁ : CategoryTheory.Limits.Cofan f₁) (c₂ : CategoryTheory.Limits.Cofan f₂) (bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt) (i : ι₁ ⊕ ι₂) : Sum.elim f₁ f₂ i ⟶ bc.pt
• CategoryTheory.Limits.Cofan.combPairIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Cofan f₁} {c₂ : CategoryTheory.Limits.Cofan f₂} {bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (h : CategoryTheory.Limits.IsColimit bc) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc))
• CategoryTheory.Limits.FormalCoproduct.cofan 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) : CategoryTheory.Limits.Cofan f
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).f p = (t.inj p.fst).f p.snd
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).φ p = (t.inj p.fst).φ p.snd
• CompHausLike.finiteCoproduct.cofan 📋 Mathlib.Topology.Category.CompHausLike.Limits
  {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.Cofan X
• Condensed.fintypeCatAsCofan 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Profinite) : CategoryTheory.Limits.Cofan fun x => Profinite.of PUnit.{u + 1}
• LightCondensed.fintypeCatAsCofan 📋 Mathlib.Condensed.Discrete.Colimit
  (X : LightProfinite) : CategoryTheory.Limits.Cofan fun x => LightProfinite.of PUnit.{u + 1}

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c