Definition disp_bicat_of_equalizer_type : disp_bicat bicat_cat_with_terminal_cleaving. Proof. use disp_subbicat. - exact (λ (C : cat_with_terminal_cleaving), fiberwise_equalizers (cleaving_of_types C)). - exact (λ (C₁ C₂ : cat_with_terminal_cleaving) (T₁ : fiberwise_equalizers (cleaving_of_types C₁)) (T₂ : fiberwise_equalizers (cleaving_of_types C₂)) (F : functor_with_terminal_cleaving C₁ C₂), ∏ (x : C₁), preserves_equalizer (fiber_functor (comp_cat_type_functor F) x)). - abstract (intros C EC x y₁ y₂ e f g h p Fp H ; exact H). - intros C₁ C₂ C₃ EC₁ EC₂ EC₃ F G HF HG x y₁ y₂ e f g h p Fp H. use (isEqualizer_eq _ _ _ _ _ (composition_preserves_equalizer (HF x) (HG _) _ _ _ _ _ _ _ _ H)). + abstract (cbn ; rewrite !mor_disp_transportf_prewhisker ; rewrite !mor_disp_transportf_postwhisker ; rewrite !disp_functor_transportf ; rewrite !mor_disp_transportf_prewhisker ; rewrite !mor_disp_transportf_postwhisker ; rewrite <- !disp_functor_comp_var ; rewrite !disp_functor_transportf ; rewrite !transport_f_f ; pose (maponpaths (transportb _ (id_right _)) p) as p' ; cbn in p' ; rewrite !transportbfinv in p' ; rewrite p' ; apply maponpaths_2 ; apply homset_property). + abstract (cbn ; rewrite !disp_functor_transportf ; rewrite !transport_f_f ; apply maponpaths_2 ; apply homset_property). + abstract (cbn ; rewrite !disp_functor_transportf ; rewrite !transport_f_f ; apply maponpaths_2 ; apply homset_property). + abstract (cbn ; rewrite !disp_functor_transportf ; rewrite !transport_f_f ; apply maponpaths_2 ; apply homset_property). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.LiftDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.