Theorem isweq_TRRGraph_univalence_map (G H : TRRGraph) : isweq (TRRGraph_univalence_map G H). Proof. use isweqhomot. - exact (weqcomp (TRRGraph_univalence_weq1 G H) (TRRGraph_univalence_weq2 G H)). - intros e. induction e. use (pathscomp0 weqcomp_to_funcomp_app). rewrite TRRGraph_univalence_weq1_idpath. rewrite TRRGraph_univalence_weq2_idpath. reflexivity. - use weqproperty. Qed.