proposition: Lemma has_fipr_has_cofipr : forall a u v, Category.axioms a -> has_fiprod a u v = has_cofiprod (opp a) (flip u) (flip v).
proof: Proof. ir. rw has_cofipr_has_fipr. rw flip_flip. rw flip_flip. rw opp_opp. tv. app opp_axioms. Qed.
imports: Arith colimits little_cat fc_limits cardinal