Lemma are_inverses_from_Equalizer_to_Equalizer {y z : C} {f g : y --> z} {E E': Equalizer f g} : is_inverse_in_precat (from_Equalizer_to_Equalizer E E') (from_Equalizer_to_Equalizer E' E). Proof. split; apply pathsinv0; use EqualizerEndo_is_identity; rewrite <- assoc; unfold from_Equalizer_to_Equalizer; repeat rewrite EqualizerCommutes; apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Retracts.