Lemma cancel_z_iso' {M : precategory} {w x y : M} (g : z_iso w x) (f f' : x --> y) : g · f = g · f' -> f = f'. Proof. intro e. destruct g as [g [g' H]]. apply (pre_comp_with_z_iso_is_inj H). assumption. Qed.
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.