proposition: Lemma cone_source_fiprod_cone : forall a u v y1 y2, cone_source (fiprod_cone a u v y1 y2) = vee_cat.
proof: Proof. ir. uf cone_source. rw socle_fiprod_cone. rww source_vee_functor. Qed.
imports: Arith colimits little_cat fc_limits cardinal