Lemma are_inverses_from_Coequalizer_to_Coequalizer {a b : C} {f g : C⟦a, b⟧} (E1 E2 : Coequalizer f g) : is_inverse_in_precat (from_Coequalizer_to_Coequalizer E2 E1) (from_Coequalizer_to_Coequalizer E1 E2). Proof. split; apply pathsinv0. - apply CoequalizerEndo_is_identity. rewrite assoc. unfold from_Coequalizer_to_Coequalizer. repeat rewrite CoequalizerArrowComm. apply idpath. - apply CoequalizerEndo_is_identity. rewrite assoc. unfold from_Coequalizer_to_Coequalizer. repeat rewrite CoequalizerArrowComm. apply idpath. 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.