Definition invertible_2cell_is_nat_z_iso {C D : bicat_of_univ_cats} (F G : C --> D) : nat_z_iso F G ≃ invertible_2cell F G. Proof. use make_weq. - exact (nat_z_iso_to_invertible_2cell F G). - use isweq_iso. + exact (invertible_2cell_to_nat_z_iso F G). + intros x. use subtypePath. * intro. apply isaprop_is_nat_z_iso. * apply idpath. + intros x. use subtypePath. * intro. apply isaprop_is_invertible_2cell. * apply idpath. 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.