∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (X : (CategoryTheory.Square C)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Square.opFunctor.map
        ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C)ᵒᵖ)).hom.app X))
      ((CategoryTheory.Iso.refl
              (CategoryTheory.Square.unopFunctor.rightOp.comp CategoryTheory.Square.opFunctor)).hom.app
        (CategoryTheory.Square.opFunctor.obj X)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Square.opFunctor.obj X)