fact: 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)).
imports: UniMath.MoreFoundations.Propositions