proposition: Lemma TRRGraph_univalence_compute (G H : TRRGraph) : pr1 (TRRGraph_univalence G H) = TRRGraph_univalence_map G H.
proof: Proof. reflexivity. 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