Proposition is_strong_epi_extremal_epi_comm₁ : is_strong_epi_extremal_epi_lift · m = g. Proof. unfold is_strong_epi_extremal_epi_lift. rewrite !assoc'. etrans. { apply maponpaths. exact (!(PullbackSqrCommutes P)). } rewrite !assoc. etrans. { apply maponpaths_2. apply z_iso_after_z_iso_inv. } apply id_left. 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.