Lemma is_cgraph_mor_id (G : precgraph) : is_cgraph_mor (idfun (node G)) (idfun (arc G)). Proof. apply make_dirprod; intros; apply idpath. Defined.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.