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