proposition: Lemma mor_coequalizer : forall a u v, has_coequalizer a u v -> mor a (coequalizer a u v).
proof: Proof. ir. cp (coequalizer_hypothesis_coequalizer H). uh H0; ee. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal