Theorems · Theorem · category theory

CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y

∀ {C : Type u} [inst : 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_1 : (E.sigmaOfIsColimit hc).I₀) (x_2 : PUnit.{w + 1}),
  (E.sigmaOfIsColimit hc hd).Y x_2 = d.pt

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category