Theorems · Theorem · category theory

CategoryTheory.Limits.Multicofork.sigma_condition

∀ {C : Type u} [inst : 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.π)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Cited by

2 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category