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