Theorems · Theorem · category theory

CategoryTheory.Limits.ColimitPresentation.bind.congr_simp

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] {X : C}
  (P : CategoryTheory.Limits.ColimitPresentation J X)
  (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j))
  [inst_3 : ∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [inst_4 : ∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)], P.bind Q = P.bind Q

Defined in

Mathlib.CategoryTheory.ObjectProperty.Ind

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.IsFinitelyPresentable