(i j : Isomorphic s d) p q : ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q. Proof. apply path_ishprop. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.