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. 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.
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.