proposition: Lemma target_equalizer : forall a u v, has_equalizer a u v -> target (equalizer a u v) = source u.
proof: Proof. ir. cp (is_equalizer_equalizer H). uh H0; ee. uh H0; ee. sy; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal