Theorems · Theorem · category theory

CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt

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

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category