proposition: Theorem isweq_TRRGraph_univalence_map (G H : TRRGraph) : isweq (TRRGraph_univalence_map G H).
proof: 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.
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