Proposition isrefl_from_internal_is_eqrel_slice {C : category} {x : C} {zf : C/x} (R : internal_eqrel zf) : internal_isrefl (from_internal_relation_slice R). Proof. intros w g. pose (w' := make_cod_fib_ob (g · cod_mor zf)). assert (g · cod_mor zf = cod_mor w') as p. { apply idpath. } pose (g' := @make_cod_fib_mor _ _ w' zf g p). pose (r := isrefl_internal_eqrel R w' g' : internal_relation_to_arr_relation _ _ _). use make_internal_relation_to_arr_relation. - exact (dom_mor r). - refine (!(comp_in_cod_fib r _) @ _). rewrite (internal_relation_to_arr_relation_src r). apply idpath. - refine (!(comp_in_cod_fib r _) @ _). rewrite (internal_relation_to_arr_relation_tar r). apply idpath. 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.