proposition: Lemma is_connected_nat_graph : is_connected nat_graph.
proof: Proof. use (is_connected_pointed nat_graph 0). intro v. induction v as [|v Hv]. - now exists 0. - use (append_graph_zig_zag Hv). exists 1. exists (S v). split. * now apply inl. * reflexivity. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Initial