(xa : StrX) : @sip_isotoid_helper xa xa (reflexivity _) = reflexivity _. Proof. unfold sip_isotoid_helper, reflexivity, isomorphic_refl. apply ap. apply path_ishprop. 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.