Definition square_verity_double_from_ver_adjequiv {x y : B} (f : adjoint_equivalence (B := ver_bicat_of_verity_double_bicat square_verity_double_bicat) x y) : adjoint_equivalence (B := B) x y. Proof. use equiv_to_adjequiv. - exact f. - pose (η := square_verity_double_from_ver_inv2cell (left_equivalence_unit_iso f)). pose (ε := square_verity_double_from_ver_inv2cell (left_equivalence_counit_iso f)). simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)). + exact (left_adjoint_right_adjoint f). + exact η. + exact ε. + apply property_from_invertible_2cell. + apply property_from_invertible_2cell. 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.