Definition mate_verity_double_to_ver_inv2cell {x y : LB} {f g : B ⟦ pr1 x , pr1 y ⟧} (τ : invertible_2cell (C := B) f g) : invertible_2cell (C := ver_bicat_of_verity_double_bicat mate_verity_double_bicat) f g. Proof. use make_invertible_2cell. - exact (τ^-1). - use make_is_invertible_2cell. + exact τ. + abstract (exact (vcomp_rinv τ)). + abstract (exact (vcomp_linv τ)). 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.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.