Lemma isEqualizer'_to_isEqualizer : isEqualizer' -> isEqualizer f g h H. Proof. intros isEq' E' h' H'. apply (@iscontrweqf (hfiber (isEqualizer'_weq isEq' _) (h',, H'))). - cbn; unfold hfiber. use weqfibtototal; intros j; cbn. unfold postcomp_with_equalizer_mor. apply subtypeInjectivity. intro; apply C. - apply weqproperty. 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.