Definition onarc {G H : precgraph} : cgraph_mor G H → arc G → arc H := λ f, pr12 f.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.