∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X}
  {f : U.right ⟶ V.right} [CategoryTheory.Epi f] (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom),
  CategoryTheory.Epi (CategoryTheory.Under.homMk f w)