proposition: Lemma isaprop_isTRRGhomo {G H : TRRGraph} (f : pr1 G → pr1 H) : isaprop (isTRRGhomo f).
proof: Proof. apply isapropdirprod. - repeat (apply impred ; intros). apply isapropdirprod. -- repeat (apply impred; intros; apply propproperty). -- repeat (apply impred; intros; apply propproperty). - apply setproperty. 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