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. set (T := tpair (fun ψ : w --> x => ψ · e = h) φ H''). set (T' := pr2 (E w h H') T). apply (base_paths _ _ T'). 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.