proposition: Lemma has_cofiprod_rw : forall a u v, has_cofiprod a u v = (exists y1, exists y2, is_cofiprod a u v y1 y2).
proof: Proof. ir. ap iff_eq; ir. uh H; ee. rwi has_fiprod_rw H0. nin H0. nin H0. sh (flip x). sh (flip x0). uhg; ee. uh H; ee. uh H; ee; am. rw flip_flip. rw flip_flip. am. nin H. nin H. assert (cofiprod_hypothesis a u v x x0). rw cofi_hyp_fi_hyp. uh H; ee. uh H0; ee. am. uh H; ee. am. uhg; ee. uh H0; ee; am. uh H; ee. rw has_fiprod_rw. sh (flip x). sh (flip x0). am. Qed.
imports: Arith colimits little_cat fc_limits cardinal