proposition: Lemma isaset_TRRGraphData (V : hSet) : isaset (TRRGraphData V).
proof: Proof. unfold TRRGraphData. apply (isofhleveltotal2 2). - apply isaset_hrel. - intros x. apply (isofhleveltotal2 2). -- apply setproperty. -- intros. apply hlevelntosn. apply isaprop_isTRR. 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