`(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m; left_inverse := right_inverse; right_inverse := left_inverse |}. Local Ltac iso_comp_t inv_lemma := etransitivity; [ | apply inv_lemma ]; first [ rewrite -> ?associativity; apply ap | rewrite <- ?associativity; apply ap ]; first [ rewrite -> ?associativity; rewrite inv_lemma | rewrite <- ?associativity; rewrite inv_lemma ]; auto with morphism. Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1) : IsIsomorphism (m0 o m1). Proof. exists (m1^-1 o m0^-1); [ abstract iso_comp_t @left_inverse | abstract iso_comp_t @right_inverse ]. Defined.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.