Lemma are_inverses_from_Equalizer_to_Equalizer {a b : C} {f g : C⟦a, b⟧} (E1 E2 : Equalizer f g) : is_inverse_in_precat (from_Equalizer_to_Equalizer E2 E1) (from_Equalizer_to_Equalizer E1 E2). Proof. split; apply pathsinv0. - apply EqualizerEndo_is_identity. rewrite <- assoc. unfold from_Equalizer_to_Equalizer. repeat rewrite EqualizerArrowComm. apply idpath. - apply EqualizerEndo_is_identity. rewrite <- assoc. unfold from_Equalizer_to_Equalizer. repeat rewrite EqualizerArrowComm. 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.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Equalizers.