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. destruct p. destruct q. apply z_iso_eq. simpl; apply pathsinv0, id_left. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos.