Lemma is_connected_nat_graph : is_connected nat_graph. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Initial.