proposition: Lemma coequalizer_hypothesis_coequalizer : forall a u v, has_coequalizer a u v -> coequalizer_hypothesis a u v (coequalizer a u v).
proof: Proof. ir. uf coequalizer. rw coeq_hyp_eq_hyp. rw flip_flip. ap equalizer_hypothesis_equalizer. uh H. ee; am. uh H; ee. uh H; ee. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal