Definition nat_z_iso_inv {C : precategory_data} {D : precategory} {F G : C ⟶ D} (μ : nat_z_iso F G) : nat_z_iso G F. Proof. exists (nat_z_iso_to_trans_inv μ). intro c. red. exists (μ c). red. split. - apply (pr2 (is_z_isomorphism_is_inverse_in_precat (pr2 μ c))). - apply (pr1 (is_z_isomorphism_is_inverse_in_precat (pr2 μ c))). 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.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.