Definition isEqualizer'_weq (is : isEqualizer') : ∏ a, (a --> E) ≃ (∑ k : a --> c, (k · f = k · g)) := λ a, make_weq (postcomp_with_equalizer_mor a) (is a).
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.