Proposition from_internal_relation_slice_monic {C : category} {x : C} {zf : C/x} (R : internal_relation zf) (w : C) (f g : w --> cod_dom R) (p : f · dom_mor (internal_relation_src R) = g · dom_mor (internal_relation_src R)) (q : f · dom_mor (internal_relation_tar R) = g · dom_mor (internal_relation_tar R)) : f = g. Proof. use (maponpaths dom_mor (@internal_relation_monic _ _ R (make_cod_fib_ob (f · cod_mor R)) (make_cod_fib_mor _ _) (make_cod_fib_mor _ _) _ _)). - apply idpath. - cbn. rewrite <- !(mor_eq (internal_relation_src R)). rewrite !assoc. apply maponpaths_2. exact (!p). - use eq_mor_cod_fib. rewrite !comp_in_cod_fib. cbn. exact p. - use eq_mor_cod_fib. rewrite !comp_in_cod_fib. cbn. exact q. 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.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.ExactCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodMorphisms. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. Section PreservesFromStable. End PreservesFromStable.