Definition preserves_source {G H : precgraph} (p : cgraph_mor G H) : ∏ x : arc G, source (onarc p x) = onnode p (source x) := pr122 p.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.