proposition: Lemma has_coequalizer_rw : forall a u v, has_coequalizer a u v = (exists y, is_coequalizer a u v y).
proof: Proof. ir. ap iff_eq; ir. uh H; ee. rwi has_equalizer_rw H0. nin H0. sh (flip x). uhg; ee. uh H; ee. uh H; ee; am. rww flip_flip. nin H. uh H; ee. uhg; ee. uh H0; ee. wri coeq_hyp_eq_hyp H0. uh H0. ee; am. am. rw has_equalizer_rw. sh (flip x). am. Qed.
imports: Arith colimits little_cat fc_limits cardinal