Definition prod_unit_inv_of_is_biequvalence : disp_pstrans (disp_pseudo_id (disp_dirprod_bicat D₁ D₃)) (disp_pseudo_comp _ _ _ _ _ LLprod RRprod) (invunit_of_is_biequivalence invs). Proof. use make_disp_pstrans. - use disp_2cells_isaprop_prod. + exact HD₁. + exact HD₃. - use disp_locally_groupoid_prod. + exact HD₁'. + exact HD₃'. - refine (λ x xx, _ ,, _). + exact (pr1 H₁ x (pr1 xx)). + exact (pr1 H₂ x (pr2 xx)). - refine (λ x y f xx yy ff, _ ,, _). + exact (disp_psnaturality_of _ _ _ (pr1 H₁) (pr1 ff)). + exact (disp_psnaturality_of _ _ _ (pr1 H₂) (pr2 ff)). 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.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispModification. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence.