proposition: Lemma finite_colimits_finite_limits_opp : forall b, has_finite_colimits b = has_finite_limits (opp b).
proof: Proof. ir. ap iff_eq; ir. uh H; uhg; ee. app opp_axioms. ir. assert (c = opp (opp c)). rww opp_opp. rw H2. ap has_limits_over_opp. am. ap opp_axioms. uh H1; ee; am. ap H0. ap is_finite_cat_opp. am. uh H; uhg; ee. wrr axioms_opp. ir. assert (c = opp (opp c)). rww opp_opp. assert (b = opp (opp b)). rww opp_opp. rw H2; rw H3. ap has_colimits_over_opp. am. ap opp_axioms. uh H1; ee; am. ap H0. app is_finite_cat_opp. Qed.
imports: Arith cat_examples cardinal fc_limits