proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Retracts