proposition: Lemma isaset_graph_mor {G H : pregraph} (h : has_vertexset H) (k : has_edgesets H) : isaset (graph_mor G H).
proof: Proof. apply isaset_total2. - exact (funspace_isaset h). - intro p₀. apply impred_isaset. intro x. apply impred_isaset. intro y. apply funspace_isaset. apply k. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions