(i j : Isomorphic s d) : @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j. Proof. destruct i, j; simpl. intro; path_induction. f_ap. exact (center _). Defined.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.