Lemma isaprop_isTRRGhomo {G H : TRRGraph} (f : pr1 G → pr1 H) : isaprop (isTRRGhomo f). Proof. apply isapropdirprod. - repeat (apply impred ; intros). apply isapropdirprod. -- repeat (apply impred; intros; apply propproperty). -- repeat (apply impred; intros; apply propproperty). - apply setproperty. Qed.