proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations