Lemma TRRGhomo_frompath (X Y : hSet) (G : TRRGraphData X) (H : TRRGraphData Y) (p : X = Y) : transportf (λ x : hSet, TRRGraphData x) p G = H → @isTRRGhomo (X ,, G) (Y ,, H) (pr1weq (hSet_univalence _ _ p)). Proof. simpl. induction p. simpl. unfold isTRRGhomo. intros q. split. - intros x y. rewrite -> idpath_transportf in q. split. rewrite -> q. intros P ; apply P. rewrite -> q. intros P ; apply P. - rewrite -> idpath_transportf in q. induction q. reflexivity. Qed.