Lemma TRRGraph_univalence_weq1_idpath (G : TRRGraph) : ((TRRGraph_univalence_weq1 G G) (idpath G)) = (idpath (pr1 G) ,, idpath (((idpath (pr1 G)) # pr2 G)%transport)). Proof. apply total2_paths_equiv. exists (idpath (idpath (pr1 G))). reflexivity. Qed.