Theorems · Theorem · category theory

CategoryTheory.GradedObject.mapMap_id

∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p],
  CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.id X) p =
    CategoryTheory.CategoryStruct.id (X.mapObj p)

Defined in

Mathlib.CategoryTheory.GradedObject

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GradedObject.HasMap