proposition: Lemma cone_composable_fipr_dotted : forall a u v y1 y2, has_fiprod a u v -> fiprod_hypothesis a u v y1 y2 -> cone_composable (fiprod_cone a u v (fipr1 a u v) (fipr2 a u v)) (fipr_dotted a u v y1 y2).
proof: Proof. ir. uf fipr_dotted. rw fiprod_cone_fiprod. assert (vee_functor a u v = socle (fiprod_cone a u v y1 y2)). rww socle_fiprod_cone. rw H1. ap cone_composable_dotted. app is_cone_fiprod_cone. rw socle_fiprod_cone. uh H; ee; am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal