∀ {T : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} T] {X Y : T} (f g : X ⟶ Y),
  f = g → ∀ (A : CategoryTheory.Under Y), (CategoryTheory.Under.map f).obj A = (CategoryTheory.Under.map g).obj A