proposition: Lemma nat_z_iso_inv_id {C D : category} {F : C ⟶ D} : nat_z_iso_inv (nat_z_iso_id F) = nat_z_iso_id F.
proof: Proof. use total2_paths_f. - use total2_paths_f. * reflexivity. * apply proofirrelevance. apply isaprop_is_nat_trans. apply homset_property. - apply proofirrelevance. apply isaprop_is_nat_z_iso. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence