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