Definition is_strong_epi {C : category} {w x : C} (e : w --> x) : UU := ∏ (y z : C) (m : y --> z) (f : w --> y) (g : x --> z) (p : e · g = f · m) (Hm : isMonic m), ∃! (l : x --> y), (l · m = g) × (e · l = f).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory.