Definition is_regular_epi : UU := ∃ (w : C) (g₁ : w --> x) (g₂ : w --> x) (p : g₁ · f = g₂ · f), isCoequalizer g₁ g₂ f p.
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.