proposition: Lemma has_coequalizers_has_colimits_over_opp : forall a, Category.axioms a -> has_coequalizers a = has_colimits_over (opp twoarrow_cat) a.
proof: Proof. ir. ap iff_eq; ir. assert (a = opp (opp a)). rww opp_opp. rw H1. ap has_colimits_over_opp. app opp_axioms. ap twoarrow_cat_axioms. wr has_equalizers_has_limits_over. rw has_equalizers_opp. am. app opp_axioms. wr has_equalizers_opp. rw has_equalizers_has_limits_over. assert (twoarrow_cat = opp (opp twoarrow_cat)). rww opp_opp. rw H1. ap has_limits_over_opp. am. ap opp_axioms. ap twoarrow_cat_axioms. am. app opp_axioms. Qed.
imports: Arith colimits little_cat fc_limits cardinal