Definition is_nat_z_iso_to_is_invertible_2cell {C D : bicat_of_univ_cats} {F G : C --> D} (η : F ==> G) : is_nat_z_iso (pr1 η) → is_invertible_2cell η. Proof. intros Hη. use tpair. - apply (nat_z_iso_inv (η ,, Hη)). - abstract (split ; [ apply nat_trans_eq ; [ apply homset_property | ] ; intros x ; cbn ; exact (z_iso_inv_after_z_iso (pr1 η x ,, _)) | apply nat_trans_eq ; [ apply homset_property | ] ; intros x ; cbn ; exact (z_iso_after_z_iso_inv (pr1 η x ,, _)) ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. 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.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.