Definition cell_E₁_to_E₂_is_invertible {x y : E₁} {f g : x --> y} (α : f ==> g) : is_invertible_2cell α → is_invertible_2cell (cell_E₁_to_E₂ α). Proof. intros Hα. use tpair. - exact (cell_E₁_to_E₂ (Hα^-1)). - split. + exact ((cell_E₁_to_E₂_vcomp α (Hα^-1)) @ maponpaths cell_E₁_to_E₂ (pr12 Hα) @ cell_E₁_to_E₂_id₂ _). + exact ((cell_E₁_to_E₂_vcomp (Hα^-1) α) @ maponpaths cell_E₁_to_E₂ (pr22 Hα) @ cell_E₁_to_E₂_id₂ _). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.