∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  {X_1 Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X} (g : X_1 ⟶ Y),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).map g).left.left = g.left