∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {Y Z : C} (i : Y ≅ Z)
  (j : CategoryTheory.Discrete PEmpty.{1}),
  CategoryTheory.CategoryStruct.comp i.inv ((CategoryTheory.Limits.asEmptyCone Y).π.app j) =
    (CategoryTheory.Limits.asEmptyCone Z).π.app j