(xa yb : StrX) (f : xa <~=~> yb) : xa = yb. Proof. refine (path_sigma_uncurried _ _ _ (isotoid X xa.1 yb.1 (sip_isotoid_helper f); _)). apply sip_helper; simpl. split; lazymatch goal with | [ |- context[idtoiso ?X ((isotoid ?X ?x ?y) ?m)] ] => pose proof (eisretr (@idtoiso X x y) m) as H'; pattern (idtoiso X ((isotoid X x y) m)) end; refine (transport _ H'^ _); clear H'; simpl; apply PreCategoryOfStructures.h. Defined.
Require Import Category.Core Category.Univalent Category.Morphisms. Require Import Structure.Core. Require Import Types.Sigma Trunc Equivalences. Require Import Basics.Iff Basics.Tactics.