Definition isaprop_disp_adjunction_univ_cat_with_bincoprod : isaprop (disp_adjunction a CC₁ CC₂). Proof. use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)) ; simpl. - apply isapropdirprod. + apply isapropunit. + apply isaprop_preserves_bincoproduct. - use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)). + use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)). * simpl. apply isapropdirprod. ** apply isapropunit. ** apply isaprop_preserves_bincoproduct. * apply isapropdirprod. ** simpl ; apply isapropdirprod ; apply isapropunit. ** simpl ; apply isapropdirprod ; apply isapropunit. + apply isapropdirprod ; apply disp_bicat_bincoprod. Qed. Section MakeDispAdj. Context (H : preserves_bincoproduct (pr112 a)). Local Definition disp_left_adjoint_univ_cat_with_bincoprod_1cell : CC₁ -->[ a ] CC₂. Proof. refine (tt ,, _). exact (left_adjoint_preserves_bincoproduct _ (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.