Definition from_is_invertible_2cell_bicat_of_strict_cat {C₁ C₂ : bicat_of_strict_cats} {F G : C₁ --> C₂} (α : F ==> G) (Hα : is_invertible_2cell α) : is_nat_z_iso (pr1 α). Proof. intros x. use make_is_z_isomorphism. - exact (pr1 (Hα^-1) x). - abstract (split ; [ exact (nat_trans_eq_pointwise (vcomp_rinv Hα) x) | exact (nat_trans_eq_pointwise (vcomp_linv Hα) x) ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Strictness. Require Import UniMath.Bicategories.Core.Univalence.