`(@IsIsomorphism C x z p) `(q : morphism C y z) : p o (p^-1 o q) = q. Proof. iso_concat_t. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.