proposition: Lemma TRRGraph_univalence_weq2_idpath (G : TRRGraph) : TRRGraph_univalence_weq2 G G (idpath (pr1 G) ,, idpath (((idpath (pr1 G)) # pr2 G)%transport)) = id_TRRGraphiso G.
proof: Proof. apply total2_paths_equiv. exists (idpath (idweq (pr1 G))). apply isaprop_isTRRGhomo. Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions