proposition: Lemma idtoiso_concat (C : category) (a a' a'' : ob C) (p : a = a') (q : a' = a'') : idtoiso (p @ q) = z_iso_comp (idtoiso p) (idtoiso q).
proof: Proof. destruct p. destruct q. apply z_iso_eq. simpl; apply pathsinv0, id_left. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos