Definition iso_after_iso_inv {C : precategory} {a b : C} (f : iso a b) : inv_from_iso f · f = identity _ . Proof. set (T := invmaponpathsweq (make_weq (precomp_with f) (pr2 f b))). apply T; clear T; simpl. unfold precomp_with. intermediate_path ((f · inv_from_iso f) · f). - apply assoc. - apply remove_id_left. + apply iso_inv_after_iso. + apply (!(id_right _ )). 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.