proposition: Lemma iso_inv_of_iso_comp (C : precategory) (a b c : ob C) (f : iso a b) (g : iso b c) : iso_inv_from_iso (iso_comp f g) = iso_comp (iso_inv_from_iso g) (iso_inv_from_iso f).
proof: Proof. apply pathsinv0. apply inv_iso_unique. simpl. unfold precomp_with. intermediate_path (f · (g · inv_from_iso g) · inv_from_iso f). - repeat rewrite assoc. apply idpath. - rewrite iso_inv_after_iso. rewrite id_right. apply iso_inv_after_iso. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories