Lemma EqualizerOfIso_diagram_proof_pd_f : f · pr12 (z_iso_inv j) = pr12 i · (i · f · j). Proof. apply pathsinv0. do 2 rewrite assoc. etrans. { do 2 apply maponpaths_2. apply (pr2 i). } refine (assoc' _ _ _ @ _). apply id_left. 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.Core.Univalence. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Retracts.