Definition precgraph : UU := ∑ (N : UU) (E : UU), (E → N) × (E → N).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.