Definition is_cgraph_mor {G H : precgraph} (p₀ : node G → node H) (p₁ : arc G → arc H) : UU := (∏ f : arc G, source (p₁ f) = p₀ (source f)) × (∏ f : arc G, target (p₁ f) = p₀ (target f)).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.