Definition cgraph_mor (G H : precgraph) : UU := ∑ (p₀ : node G → node H) (p₁ : arc G → arc H), is_cgraph_mor p₀ p₁.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.