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