proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories