Lemma Equalizer_eq {C : category} (E : Equalizers C) {x x' y y' : ob C} {f g : C⟦x, y⟧} {f' g' : C⟦x', y'⟧} (i_x : x' = x) (i_y : y = y') (p1 : idtoiso i_x · f · idtoiso i_y = f') (p2 : idtoiso i_x · g · idtoiso i_y = g') : z_iso (E _ _ f g) (E _ _ f' g'). Proof. induction i_x, i_y, p1, p2. cbn. rewrite ! id_left, ! id_right. apply identity_z_iso. 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.