Definition preserves_target {G H : precgraph} (p : cgraph_mor G H) : ∏ f : arc G, target (onarc p f) = onnode p (target f) := pr222 p.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.