proposition: Lemma sip_isotoid_helper_refl (xa : StrX) : @sip_isotoid_helper xa xa (reflexivity _) = reflexivity _.
proof: Proof. unfold sip_isotoid_helper, reflexivity, isomorphic_refl. apply ap. apply path_ishprop. Defined.
imports: Category.Core Category.Univalent Category.Morphisms Structure.Core Types.Sigma Trunc Equivalences Basics.Tactics