Definition invertible_2cell_to_nat_z_iso {C D : bicat_of_cats} (F G : C --> D) : invertible_2cell F G → nat_z_iso F G. Proof. intros η. use make_nat_z_iso. - exact (cell_from_invertible_2cell η). - apply is_invertible_2cell_to_is_nat_z_iso. apply η. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.