proposition: Lemma is_equalizer_equalizer : forall a u v, has_equalizer a u v -> is_equalizer a u v (equalizer a u v).
proof: Proof. ir. uhg; ee. app equalizer_hypothesis_equalizer. uf equalizer. wr equalizer_cone_eq. ap is_limit_limit. uh H; ee; am. uh H; ee. am. ap is_limit_is_cone. ap is_limit_limit. uh H; ee; am. rw socle_limit. tv. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal