proposition: Proposition disp_left_adjoint_equivalence_subbicat {C₁ C₂ : bicat_of_univ_cats} {F : C₁ --> C₂} (HF : left_adjoint_equivalence F) (T₁ : disp_bicat_terminal_obj C₁) (T₂ : disp_bicat_terminal_obj C₂) (FT : T₁ -->[ F ] T₂) : disp_left_adjoint_equivalence HF FT.
proof: Proof. use disp_left_adjoint_equivalence_subbicat. - clear C₁ C₂ F HF T₁ T₂ FT ; cbn. intros C₁ C₂ T₁ T₂ F HF. exact (right_adjoint_preserves_terminal _ (adj_equivalence_of_cats_inv _ (adj_equiv_to_equiv_cat _ HF))). - exact univalent_cat_is_univalent_2. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell UniMath.Bicategories.DisplayedBicats.Examples.Prod