proposition: Lemma are_inverses_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z} {E E': Coequalizer f g} : is_inverse_in_precat (from_Coequalizer_to_Coequalizer E E') (from_Coequalizer_to_Coequalizer E' E).
proof: Proof. split; apply pathsinv0; use CoequalizerEndo_is_identity; rewrite assoc; unfold from_Coequalizer_to_Coequalizer; repeat rewrite CoequalizerCommutes; apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Retracts