Lemma isaset_graph_mor {G H : pregraph} (h : has_vertexset H) (k : has_edgesets H) : isaset (graph_mor G H). 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.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.