Lemma is_connected_coequalizer_graph : is_connected Coequalizer_graph. Proof. use (is_connected_pointed Coequalizer_graph (● 0)%stn). intro v. induction v as [v v2]. induction v as [|v Hv]. - exists 0. apply subtypePath; [intro; apply propproperty|]. reflexivity. - induction v as [|v Hv2]; [|induction (nopathsfalsetotrue v2)]. exists 1. exists (● 1)%stn. split. * do 2 apply inl. exact tt. * apply subtypePath; [intro; apply propproperty|]. reflexivity. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Coequalizers.