Theorems · Theorem · category theory

CategoryTheory.GlueData.glue_condition

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J),
  CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) =
    CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)

Defined in

Mathlib.CategoryTheory.GlueData

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasMulticoequalizer