xa : @sip_isotoid xa xa (reflexivity _) = reflexivity _. Proof. refine (_ @ eta_path_sigma_uncurried _). refine (ap (path_sigma_uncurried _ _ _) _). apply equiv_path_sigma_hprop. simpl. refine (_ @ eisretr (isotoid X xa.1 xa.1) 1%path). apply ap. apply sip_isotoid_helper_refl. 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.