Definition square_verity_double_ver_adjequiv_weq (HB_2_1 : is_univalent_2_1 B) (x y : B) : adjoint_equivalence (B := B) x y ≃ adjoint_equivalence (B := ver_bicat_of_verity_double_bicat square_verity_double_bicat) x y. Proof. use weq_iso. - exact square_verity_double_to_ver_adjequiv. - exact square_verity_double_from_ver_adjequiv. - abstract (intros f ; use subtypePath ; [ intro ; apply (isaprop_left_adjoint_equivalence _ HB_2_1) | ] ; apply idpath). - abstract (intros f ; use subtypePath ; [ intro ; apply (isaprop_left_adjoint_equivalence _ (ver_locally_univalent_square_verity_double_bicat HB_2_1)) | apply idpath ]). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.