Lemma is_cgraph_mor_comp {G H K : precgraph} (p : cgraph_mor G H) (q : cgraph_mor H K) : is_cgraph_mor (onnode q ∘ onnode p) (onarc q ∘ onarc p). Proof. apply make_dirprod. - intros. unfold funcomp. etrans. apply (preserves_source q). apply maponpaths. apply (preserves_source p). - intros. unfold funcomp. etrans. apply (preserves_target q). apply maponpaths. apply (preserves_target p). Defined.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.