Theorems · Theorem · category theory

CategoryTheory.InducedWideCategory.category_id_hom

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative] (X : CategoryTheory.InducedWideCategory D F P),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)

Defined in

Mathlib.CategoryTheory.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative