Definition isEqualizer_eq {C : category} {e x y : C} {f g f' g' : x --> y} {i i' : e --> x} (p : i · f = i · g) (q : i' · f' = i' · g') (s₁ : f = f') (s₂ : g = g') (s₃ : i = i') (He : isEqualizer f g i p) : isEqualizer f' g' i' q. Proof. intros w h r. use iscontraprop1. - abstract (induction s₁, s₂, s₃ ; apply (isapropifcontr (He w h r))). - simple refine (_ ,, _). + refine (EqualizerIn (make_Equalizer _ _ _ _ He) _ h _). abstract (induction s₁, s₂ ; exact r). + abstract (cbn ; induction s₁, s₂, s₃ ; apply (EqualizerCommutes (make_Equalizer _ _ _ _ He))). 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.