Theorems · Theorem · category theory

CategoryTheory.CatEnriched.id_hComp_id

∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C}
  (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id f) (CategoryTheory.CategoryStruct.id g) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.EnrichedCategory