proposition: Lemma structure_identity_principle_helper (xa yb : StrX) (x : xa <~=~> yb) : PreCategoryOfStructures.f (idtoiso (precategory_of_structures P) (sip_isotoid x) : morphism _ _ _) = PreCategoryOfStructures.f (x : morphism _ _ _).
proof: Proof. refine (path_f_idtoiso_precategory_of_structures _ @ _). refine ((ap _ (ap _ _)) @ (ap (@morphism_isomorphic _ _ _) (eisretr (@idtoiso X xa.1 yb.1) (sip_isotoid_helper _)))). exact (pr1_path_sigma_uncurried _). Defined.
imports: Category.Core Category.Univalent Category.Morphisms Structure.Core Types.Sigma Trunc Equivalences Basics.Tactics