proposition: Lemma has_cofiprods_has_colimits_over_opp : forall a, Category.axioms a -> has_cofiprods a = has_colimits_over (opp vee_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 vee_cat_axioms. wr has_fiprods_has_limits_over. rw has_fiprods_opp. am. app opp_axioms. wr has_fiprods_opp. rw has_fiprods_has_limits_over. assert (vee_cat = opp (opp vee_cat)). rww opp_opp. rw H1. ap has_limits_over_opp. am. ap opp_axioms. ap vee_cat_axioms. am. app opp_axioms. Qed.
imports: Arith colimits little_cat fc_limits cardinal