∀ {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e]
  {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp e i = φ → CategoryTheory.Limits.factorThruImage φ = e