proposition: Lemma has_cofiprods_opp : forall a, has_cofiprods (opp a) = has_fiprods a.
proof: Proof. ir. ap iff_eq; ir. uh H; ee. uhg; ee. wrr axioms_opp. ir. rw has_fipr_has_cofipr. ap H0. rw covee_hypothesis_opp. rw flip_flip. rw flip_flip. am. wrr axioms_opp. wrr axioms_opp. uh H; ee. uhg; ee. app opp_axioms. ir. rw has_cofipr_has_fipr. rw opp_opp. ap H0. wr covee_hypothesis_opp. am. am. app opp_axioms. Qed.
imports: Arith colimits little_cat fc_limits cardinal