(i j : Isomorphic s d) p : ap (@morphism_isomorphic _ _ _) (path_isomorphic i j p) = p. Proof. unfold path_isomorphic. destruct i, j. path_induction_hammer. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.