Lemma z_iso_inv_of_z_iso_comp {C : category} (a b c : ob C) (f : z_iso a b) (g : z_iso b c) : z_iso_inv_from_z_iso (z_iso_comp f g) = z_iso_comp (z_iso_inv_from_z_iso g) (z_iso_inv_from_z_iso f). Proof. apply z_iso_eq. apply idpath. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.