∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] (X : T) {Z Y : CategoryTheory.Over (Opposite.op X)}
  (f : Z ⟶ Y),
  CategoryTheory.CategoryStruct.comp (Opposite.unop (Opposite.op (CategoryTheory.Under.mk Y.hom.unop))).hom
      f.left.unop =
    (Opposite.unop (Opposite.op (CategoryTheory.Under.mk Z.hom.unop))).hom