∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I)
  (j : J) (X : C (g j)), (CategoryTheory.Sigma.inclCompMap C g j).hom.app X = CategoryTheory.CategoryStruct.id ⟨g j, X⟩