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