proposition: Lemma isEqualizerInUnique {x y z : C} (f g : y --> z) (e : x --> y) (H : e · f = e · g) (E : isEqualizer f g e H) (w : C) (h : w --> y) (H' : h · f = h · g) (φ : w --> x) (H'' : φ · e = h) : φ = (pr1 (pr1 (E w h H'))).
proof: Proof. set (T := tpair (fun ψ : w --> x => ψ · e = h) φ H''). set (T' := pr2 (E w h H') T). apply (base_paths _ _ T'). 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