proposition: Lemma Equalizer_z_iso_lr_eq : ι · f₂ = ι · g₂.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.BinCoproducts