Proposition is_strong_epi_extremal_epi_unique : isaprop (∑ l, l · m = g × e · l = f). Proof. use invproofirrelevance. intros l₁ l₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use Hm. exact (pr12 l₁ @ !(pr12 l₂)). 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. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory.