Proposition istrans_from_internal_is_eqrel_slice {C : category} {x : C} {zf : C/x} (R : internal_eqrel zf) : internal_istrans (from_internal_relation_slice R). Proof. intros w g₁ g₂ g₃ p q. pose (w' := make_cod_fib_ob (g₁ · cod_mor zf)). induction p as [ h [ p₁ p₂ ]]. induction q as [ k [ q₁ q₂ ]]. cbn in h, p₁, p₂, k, q₁, q₂. assert (g₁ · cod_mor zf = cod_mor w') as r₁. { apply idpath. } pose (g₁' := @make_cod_fib_mor _ _ w' zf g₁ r₁). assert (g₂ · cod_mor zf = cod_mor w') as r₂. { cbn. rewrite <- p₁, <- p₂. rewrite !assoc'. rewrite (mor_eq (internal_relation_src R)). rewrite (mor_eq (internal_relation_tar R)). apply idpath. } pose (g₂' := @make_cod_fib_mor _ _ w' zf g₂ r₂). assert (k · cod_mor R = h · cod_mor R) as lem. { etrans. { rewrite <- (mor_eq (internal_relation_src R)). rewrite !assoc. rewrite q₁. apply idpath. } rewrite <- (mor_eq (internal_relation_tar R)). rewrite !assoc. rewrite p₂. apply idpath. } assert (g₃ · cod_mor zf = cod_mor w') as r₃. { cbn. rewrite <- p₁, <- q₂. rewrite !assoc'. rewrite (mor_eq (internal_relation_src R)). rewrite (mor_eq (internal_relation_tar R)). exact lem. } pose (g₃' := @make_cod_fib_mor _ _ w' zf g₃ r₃). assert (internal_relation_to_arr_hrel R w' g₁' g₂') as H₁. { use make_internal_relation_to_arr_relation. - use make_cod_fib_mor. + exact h. + cbn. rewrite <- p₁. rewrite !assoc'. rewrite (mor_eq (internal_relation_src R)). apply idpath. - 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 p₂. } assert (internal_relation_to_arr_hrel R w' g₂' g₃') as H₂. { use make_internal_relation_to_arr_relation. - use make_cod_fib_mor. + exact k. + cbn. rewrite <- p₁. rewrite !assoc'. rewrite (mor_eq (internal_relation_src R)). exact lem. - use eq_mor_cod_fib. rewrite comp_in_cod_fib ; cbn. exact q₁. - use eq_mor_cod_fib. rewrite comp_in_cod_fib ; cbn. exact q₂. } pose (r := istrans_internal_eqrel R w' g₁' g₂' g₃' H₁ H₂). cbn in r. 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.