Theorems · Theorem · category theory

CategoryTheory.CatEnrichedOrdinary.homEquiv_comp

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CatEnrichedOrdinary.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.homEquiv f)
      (CategoryTheory.CatEnrichedOrdinary.homEquiv g)

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.EnrichedOrdinaryCategory