Definition isaprop_disp_adjunction_univ_cat_with_terminal_obj : isaprop (disp_adjunction a CC₁ CC₂). Proof. use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl. - apply isapropdirprod. + apply isapropunit. + apply isaprop_preserves_terminal. - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)). + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)). * simpl. apply isapropdirprod. ** apply isapropunit. ** apply isaprop_preserves_terminal. * apply isapropdirprod. ** simpl ; apply isapropdirprod ; apply isapropunit. ** simpl ; apply isapropdirprod ; apply isapropunit. + apply isapropdirprod ; apply disp_bicat_terminal_obj. Qed. Section MakeDispAdj. Context (H : preserves_terminal (pr1 a)). Let F : CC₁ -->[ a ] CC₂ := tt ,, H. Local Definition disp_left_adjoint_data_univ_cat_with_terminal_obj : disp_left_adjoint_data a F. Proof. refine ((tt ,, _) ,, ((tt ,, tt) ,, (tt ,, tt))). exact (right_adjoint_preserves_terminal _ (left_adjoint_to_is_left_adjoint a)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. 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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.StructuredCategories. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInBicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.