Proposition preserves_equalizer_fiber_disp_codomain_functor {C₁ C₂ : category} (F : C₁ ⟶ C₂) (HF : preserves_equalizer F) (x : C₁) : preserves_equalizer (fiber_functor (disp_codomain_functor F) x). Proof. intros y₁ y₂ z f g e p Fp H. assert (# F (dom_mor e) · # F (dom_mor f) = # F (dom_mor e) · # F (dom_mor g)) as q. { refine (!(functor_comp F _ _) @ _ @ functor_comp F _ _). apply maponpaths. unfold dom_mor. exact (!(comp_in_cod_fib _ _) @ maponpaths dom_mor p @ comp_in_cod_fib _ _). } use to_isEqualizer_cod_fib. - abstract (rewrite !disp_codomain_fiber_functor_mor ; exact q). - use (isEqualizer_eq _ _ _ _ _ (HF _ _ _ _ _ _ _ _ (from_isEqualizer_cod_fib _ _ _ _ _ H))). + exact q. + rewrite disp_codomain_fiber_functor_mor. apply idpath. + rewrite disp_codomain_fiber_functor_mor. apply idpath. + rewrite disp_codomain_fiber_functor_mor. apply idpath. + unfold dom_mor. exact (!(comp_in_cod_fib _ _) @ maponpaths dom_mor p @ comp_in_cod_fib _ _). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.