proposition: Lemma fiprod_cone_fiprod : forall a u v, has_fiprod a u v -> fiprod_cone a u v (fipr1 a u v) (fipr2 a u v) = limit (vee_functor a u v).
proof: Proof. ir. uf fipr1; uf fipr2. wr fiprod_cone_eq. tv. uh H; ee; am. ap is_limit_is_cone. ap is_limit_limit. uh H; ee; am. rw socle_limit. tv. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal