Definition prod_counit_inv_of_is_biequvalence : disp_pstrans (disp_pseudo_id (disp_dirprod_bicat D₂ D₄)) (disp_pseudo_comp _ _ _ _ _ RRprod LLprod) (invcounit_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 (pr12 H₁ x (pr1 xx)). + exact (pr12 H₂ x (pr2 xx)). - refine (λ x y f xx yy ff, _ ,, _). + exact (disp_psnaturality_of _ _ _ (pr12 H₁) (pr1 ff)). + exact (disp_psnaturality_of _ _ _ (pr12 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.