Lemma post_comp_with_iso_is_inj {C : precategory} (b c : ob C) (h : b --> c) (H : is_iso h) (a : ob C) (f g : a --> b) : f · h = g · h -> f = g. Proof. intro HH. set (T := iso_inv_after_iso (h,,H)). simpl in T. intermediate_path (f · (h · inv_from_iso (h,,H))). - rewrite T. clear T. apply pathsinv0, id_right. - rewrite assoc. rewrite HH. rewrite <- assoc. rewrite T. apply id_right. 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.