Definition TRRGraph_univalence_weq2 (G H : TRRGraph) : G ╝ H ≃ G ≅ H. Proof. use weqbandf. - exact (hSet_univalence (pr1 G) (pr1 H)). - intro p. simpl. use weqimplimpl. * intros q. exact (TRRGhomo_frompath (pr1 G) (pr1 H) (pr2 G) (pr2 H) p q). * intros q. exact (TRRGhomo_topath (pr1 G) (pr1 H) (pr2 G) (pr2 H) p q). * exact (isaset_TRRGraphData (pr1 H) ((p # pr2 G)%transport) (pr2 H)). * exact (isaprop_isTRRGhomo (hSet_univalence_map (pr1 G) (pr1 H) p)). Defined.