Proposition is_extremal_epi_strong_epi {C : category} {x y : C} {e : x --> y} (He : is_strong_epi e) : is_extremal_epi e. Proof. intros z f g p Hg. assert (e · identity y = f · g) as q. { rewrite id_right. exact p. } pose (fact := He _ _ g f (identity _) q Hg). pose (l := pr11 fact). pose (r := pr121 fact : l · g = identity _). use make_is_z_isomorphism. - exact l. - split. + use Hg. rewrite !assoc'. rewrite r. rewrite id_left, id_right. apply idpath. + exact r. 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.