Lemma Equalizer_z_iso_lr_eq : ι · f₂ = ι · g₂. Proof. unfold ι. pose proof (maponpaths (λ z, inv_from_z_iso l · z · inv_from_z_iso r) p) as p'. pose proof (maponpaths (λ z, inv_from_z_iso l · z · inv_from_z_iso r) q) as q'. cbn in p', q'. rewrite !assoc in p', q'. rewrite z_iso_after_z_iso_inv in p', q'. rewrite id_left in p', q'. rewrite !assoc' in p', q'. rewrite z_iso_inv_after_z_iso in p', q'. rewrite id_right in p', q'. rewrite !assoc'. rewrite <- p', <- q'. rewrite !assoc. apply maponpaths_2. apply EqualizerEqAr. Qed.
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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts.