`(@IsIsomorphism C x y p) `(@IsIsomorphism C x z q) : (p o q^-1)^-1 = q 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.