Lemma iso_inv_on_left {C : precategory} (a b c : ob C) (f : a --> b) (g : iso b c) (h : a --> c) (H : h = f · g) : f = h · inv_from_iso g. Proof. assert (H2 : h · inv_from_iso g = (f · g) · inv_from_iso g). rewrite H. apply idpath. rewrite <- assoc in H2. rewrite iso_inv_after_iso in H2. rewrite id_right in H2. apply pathsinv0. 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.