proposition: Lemma has_equalizer_rw : forall a u v, has_equalizer a u v = (exists y, is_equalizer a u v y).
proof: Proof. ir. ap iff_eq; ir. uh H; ee. uh H0. nin H0. uh H0; ee. sh (eqzmap x). uhg; ee. ap equalizer_hypothesis_eqzmap. am. app is_limit_is_cone. am. assert (is_cone x). app is_limit_is_cone. util (equalizer_cone_eq (a:=a) (u:=u) (v:=v) (c:=x)). am. am. am. wr H3. am. nin H. uhg; ee. uh H; ee. uh H; ee; am. uh H; ee. uhg. sh (equalizer_cone a u v x). uhg; ee. am. rww socle_equalizer_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal