Definition cgraph_mor_comp {G H K : precgraph} (p : cgraph_mor G H) (q : cgraph_mor H K) : cgraph_mor G K := make_cgraph_mor (onnode q ∘ onnode p) (onarc q ∘ onarc p) (is_cgraph_mor_comp p q).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.