Lemma TRRGhomo_topath (X Y : hSet) (G : TRRGraphData X) (H : TRRGraphData Y) (p : X = Y) : @isTRRGhomo (X ,, G) (Y ,, H) (pr1weq (hSet_univalence _ _ p)) → transportf (λ x : hSet, TRRGraphData x) p G = H. Proof. induction p. rewrite -> idpath_transportf. intros P. unfold isTRRGhomo in P. simpl in P. destruct P as [π σ]. assert (q : pr1 G = pr1 H). { use funextfun. unfold homot. intros x. use funextfun. unfold homot. intros y. apply (hPropUnivalence (pr1 G x y) (pr1 H x y) (pr1 (π x y)) (pr2 (π x y))). } apply total2_paths_equiv. exists q. apply (helper X (pr1 G) (pr1 H) (pr12 G) (pr12 H) _ _ q σ). Qed.