Proposition is_regular_epi_f_epi_unique : isaprop (∑ (hk : w --> cod_dom (cod_pb PB f sum)), hk · top_map = h × hk · dom_mor (cod_fiber_functor_pb PB f sum_im_map) = k). Proof. use invproofirrelevance. intros ζ₁ ζ₂. use subtypePath. { intro ; apply isapropdirprod ; apply homset_property. } use (MorphismsIntoPullbackEqual (isPullback_Pullback P)). - exact (pr12 ζ₁ @ !(pr12 ζ₂)). - pose proof (maponpaths (λ z, z · PullbackPr2 _) (pr22 ζ₁ @ !(pr22 ζ₂))) as r. cbn in r. rewrite !assoc' in r. rewrite !PullbackArrow_PullbackPr2 in r. exact r. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.DisjointBinCoproducts. Require Import UniMath.CategoryTheory.Limits.StrictInitial. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.Inclusion. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts.