proposition: Lemma isEqualizer_to_isEqualizer' : isEqualizer f g h H -> isEqualizer'.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Retracts