proposition: Proposition isaprop_Equalizer {C : category} (HC : is_univalent C) {x y : C} (f g : x --> y) : isaprop (Equalizer f g).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use (isaprop_total2 (_ ,, _) (λ _, (_ ,, _))). - apply homset_property. - simpl. repeat (use impred ; intro). apply isapropiscontr. } use total2_paths_f. - use (isotoid _ HC). use z_iso_from_Equalizer_to_Equalizer. - rewrite transportf_isotoid ; cbn. apply EqualizerCommutes. Qed.
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