Theorems · Theorem · category theory

CategoryTheory.InducedWideCategory.category_comp_hom

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative]
  {x x_1 x_2 : CategoryTheory.InducedWideCategory D F P} (f : x.Hom x_1) (g : x_1.Hom x_2),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative