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