proposition: Lemma is_versal_fiprod_cone : forall a u v y1 y2, fiprod_hypothesis a u v y1 y2 -> is_versal (fiprod_cone a u v y1 y2) = (forall z1 z2, fiprod_hypothesis a u v z1 z2 -> (exists w, (mor a w & source y1 = target w & comp a y1 w = z1 & comp a y2 w = z2))).
proof: Proof. ir. ap iff_eq; ir. uh H0; ee. util (H2 (fiprod_cone a u v z1 z2)). app is_cone_fiprod_cone. rww socle_fiprod_cone; sy; rww socle_fiprod_cone. nin H3. ee. cp H3. uh H5; ee. rwi cone_target_fiprod_cone H6. rwi vertex_fiprod_cone H7. rwi cone_compose_fiprod_cone H4. sh x; ee. am. sy; am. transitivity (fimap1 (fiprod_cone a u v (comp a y1 x) (comp a y2 x))). rw fimap1_fiprod_cone. tv. rw H4. rw fimap1_fiprod_cone. tv. transitivity (fimap2 (fiprod_cone a u v (comp a y1 x) (comp a y2 x))). rw fimap2_fiprod_cone. tv. rw H4. rw fimap2_fiprod_cone. tv. am. am. sy; am. assert (lem1: fiprod_hypothesis a u v y1 y2). am. uh H; uhg; ee; try am. app is_cone_fiprod_cone. ir. rwi socle_fiprod_cone H8. cp (fiprod_cone_eq H H7 H8). cp (fiprod_hypothesis_fimaps H H7 H8). util (H0 (fimap1 b) (fimap2 b)). am. nin H11. ee. sh x; ee. app cone_composable_fiprod_cone. rww cone_compose_fiprod_cone. rw H13. rw H14. sy; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal