Lemma isEqualizerInsEq {x y z: C} {f g : y --> z} {e : x --> y} {H : e · f = e · g} (E : isEqualizer f g e H) {w : C} (φ1 φ2: w --> x) (H' : φ1 · e = φ2 · e) : φ1 = φ2. Proof. assert (H'1 : φ1 · e · f = φ1 · e · g). rewrite <- assoc. rewrite H. rewrite assoc. apply idpath. set (E' := make_Equalizer _ _ _ _ E). set (E'ar := EqualizerIn E' w (φ1 · e) H'1). intermediate_path E'ar. apply isEqualizerInUnique. apply idpath. apply pathsinv0. apply isEqualizerInUnique. apply pathsinv0. apply H'. 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.