Lemma isEqualizer_to_isEqualizer' : isEqualizer f g h H -> isEqualizer'. Proof. intros isEq E'. unfold postcomp_with_equalizer_mor. unfold isweq, hfiber. intros hH'. apply (@iscontrweqf (∑ u : C ⟦ E', E ⟧, u · h = pr1 hH')). - use weqfibtototal; intro; cbn. apply invweq. use subtypeInjectivity. intro; apply C. - exact (isEq E' (pr1 hH') (pr2 hH')). 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.