Proposition is_strong_epi_extremal_epi {C : category} (PB : Pullbacks C) {w x : C} {e : w --> x} (He : is_extremal_epi e) : is_strong_epi e. Proof. intros y z m f g p Hm. use iscontraprop1. - apply is_strong_epi_extremal_epi_unique. exact Hm. - simple refine (_ ,, _ ,, _). + exact (is_strong_epi_extremal_epi_lift PB e m f g p He Hm). + apply is_strong_epi_extremal_epi_comm₁. + apply is_strong_epi_extremal_epi_comm₂. Defined.
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.