Theorems · Theorem · category theory

CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_id_hom

∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (a b : CategoryTheory.Bicategory.InducedBicategory C F) (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id f).hom = CategoryTheory.CategoryStruct.id f.hom

Defined in

Mathlib.CategoryTheory.Bicategory.InducedBicategory

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

CategoryTheory.Bicategory