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