Definition is_invertible_2cell_bicat_of_strict_cat {C₁ C₂ : bicat_of_strict_cats} {F G : C₁ --> C₂} (α : F ==> G) (Hα : is_nat_z_iso (pr1 α)) : is_invertible_2cell α. Proof. use make_is_invertible_2cell. - exact (pr1 (nat_z_iso_inv (make_nat_z_iso _ _ α Hα))). - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; exact (z_iso_inv_after_z_iso (make_z_iso _ _ (Hα x)))). - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; exact (z_iso_after_z_iso_inv (make_z_iso _ _ (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.