proposition: Lemma comp_nat_z_iso_id_right {C D:category} {F G:functor C D} (α: nat_z_iso F G) :nat_z_iso_comp α (nat_z_iso_id G) = α.
proof: Proof. induction α as (α, α_is_nat_z_iso). use total2_paths_f; cbn. - exact (nat_trans_comp_id_right (pr2 D) F G α). - 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