Lemma iso_inv_on_right {C : precategory} (a b c : ob C) (f : iso a b) (g : b --> c) (h : a --> c) (H : h = f · g) : inv_from_iso f · h = g. Proof. apply (invmaponpathsweq (make_weq (precomp_with f) (pr2 f c))). unfold precomp_with; simpl. intermediate_path ((f · inv_from_iso f) · h). - apply assoc. - apply remove_id_left. + apply iso_inv_after_iso. + assumption. 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.