(xa yb : StrX) (x : xa <~=~> yb) : PreCategoryOfStructures.f (idtoiso (precategory_of_structures P) (sip_isotoid x) : morphism _ _ _) = PreCategoryOfStructures.f (x : morphism _ _ _). 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.
Require Import Category.Core Category.Univalent Category.Morphisms. Require Import Structure.Core. Require Import Types.Sigma Trunc Equivalences. Require Import Basics.Iff Basics.Tactics.