proposition: Lemma sip_isotoid_refl xa : @sip_isotoid xa xa (reflexivity _) = reflexivity _.
proof: 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.
imports: Category.Core Category.Univalent Category.Morphisms Structure.Core Types.Sigma Trunc Equivalences Basics.Tactics