Definition prod_disp_is_biequivalence_data : disp_is_biequivalence_data (disp_dirprod_bicat D₁ D₃) (disp_dirprod_bicat D₂ D₄) invs prod_is_disp_biequivalence_unit_counit. Proof. simple refine (_ ,, _ ,, (_ ,, _) ,, (_ ,, _)). - exact prod_unit_inv_of_is_biequvalence. - exact prod_counit_inv_of_is_biequvalence. - use make_disp_invmodification. + use disp_2cells_isaprop_prod. * exact HD₁. * exact HD₃. + use disp_locally_groupoid_prod. * exact HD₁'. * exact HD₃'. + refine (λ x xx, _ ,, _). * exact (pr11 (pr122 H₁) x (pr1 xx)). * exact (pr11 (pr122 H₂) x (pr2 xx)). - use make_disp_invmodification. + use disp_2cells_isaprop_prod. * exact HD₁. * exact HD₃. + use disp_locally_groupoid_prod. * exact HD₁'. * exact HD₃'. + refine (λ x xx, _ ,, _). * exact (pr12 (pr122 H₁) x (pr1 xx)). * exact (pr12 (pr122 H₂) x (pr2 xx)). - use make_disp_invmodification. + use disp_2cells_isaprop_prod. * exact HD₂. * exact HD₄. + use disp_locally_groupoid_prod. * exact HD₂'. * exact HD₄'. + refine (λ x xx, _ ,, _). * exact (pr11 (pr222 H₁) x (pr1 xx)). * exact (pr11 (pr222 H₂) x (pr2 xx)). - use make_disp_invmodification. + use disp_2cells_isaprop_prod. * exact HD₂. * exact HD₄. + use disp_locally_groupoid_prod. * exact HD₂'. * exact HD₄'. + refine (λ x xx, _ ,, _). * exact (pr12 (pr222 H₁) x (pr1 xx)). * exact (pr12 (pr222 H₂) x (pr2 xx)). 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.