Theorems · Theorem · category theory

CategoryTheory.CatEnrichedOrdinary.hComp_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C]
  {a b c d : CategoryTheory.CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f')
  (θ : g ⟶ g') (κ : h ⟶ h'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CatEnrichedOrdinary.hComp η θ) κ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CatEnrichedOrdinary.hComp θ κ))
        (CategoryTheory.eqToHom ⋯))

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.EnrichedOrdinaryCategory