Proposition isaprop_Equalizer {C : category} (HC : is_univalent C) {x y : C} (f g : x --> y) : isaprop (Equalizer f g). 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.
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.