Definition is_iso_inv_from_iso {C : precategory} {a b : C} (f : iso a b) : is_iso (inv_from_iso f). Proof. intro c. apply (isweq_iso _ (precomp_with f)). - intro g. unfold precomp_with. intermediate_path ((f · inv_from_iso f) · g). + apply assoc. + apply remove_id_left. apply iso_inv_after_iso. apply idpath. - intro g. unfold precomp_with. intermediate_path ((inv_from_iso f · f) · g). + apply assoc. + apply remove_id_left. apply iso_after_iso_inv. apply idpath. 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.