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. 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.
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.