Definition nat_z_iso_to_trans_inv {C : precategory_data} {D : precategory} {F G : C ⟶ D} (μ : nat_z_iso F G) : G ⟹ F. Proof. apply (make_nat_trans G F (fun c => is_z_isomorphism_mor (pr2 μ c))). red. intros c c' f. set (h := μ c,,pr2 μ c : z_iso (F c) (G c)). set (h' := μ c',,pr2 μ c' : z_iso (F c') (G c')). change (# G f · inv_from_z_iso h' = inv_from_z_iso h · # F f). apply pathsinv0. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. apply pathsinv0. apply (nat_trans_ax μ). 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.