Definition make_precgraph {N : UU} {E : UU} (s t : E → N) : precgraph := N,, E,, make_dirprod s t.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.