Proposition comp_preserves_regular_epi {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} (HF : preserves_regular_epi F) (HG : preserves_regular_epi G) : preserves_regular_epi (F ∙ G). Proof. intros x y f Hf. apply HG. apply HF. exact Hf. Qed.
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.