Theorems · Theorem · category theory

CategoryTheory.InducedCategory.comp_hom

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y Z : CategoryTheory.InducedCategory D F} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.Category