proposition: Lemma is_uni_fiprod_cone : forall a u v y1 y2, fiprod_hypothesis a u v y1 y2 -> is_uni (fiprod_cone a u v y1 y2) = (forall z z', mor a z -> mor a z' -> source y1 = target z -> source y1 = target z' -> comp a y1 z = comp a y1 z' -> comp a y2 z = comp a y2 z'-> z = z').
proof: Proof. ir. ap iff_eq; ir. uh H0. ee. ap H7. app cone_composable_fiprod_cone. app cone_composable_fiprod_cone. rw cone_compose_fiprod_cone. sy; rw cone_compose_fiprod_cone. sy. rw H5. rw H6. tv. am. am. am. am. am. am. uhg. ee. app is_cone_fiprod_cone. ir. cp H1; cp H2. uh H4; uh H5; ee. rwi cone_target_fiprod_cone H8. rwi cone_target_fiprod_cone H6. rwi vertex_fiprod_cone H9. rwi vertex_fiprod_cone H7. app H0. sy; am. sy; am. rwi cone_compose_fiprod_cone H3. tv. transitivity (fimap1 (fiprod_cone a u v (comp a y1 u0) (comp a y2 u0))). rw fimap1_fiprod_cone. tv. rw H3. rw fimap1_cone_compose. rw cone_target_fiprod_cone. rw fimap1_fiprod_cone. tv. am. rww cone_source_fiprod_cone. am. am. am. sy; am. transitivity (fimap2 (cone_compose (fiprod_cone a u v y1 y2) u0)). rw cone_compose_fiprod_cone. rw fimap2_fiprod_cone. tv. am. am. sy; am. rw H3. rw fimap2_cone_compose. rw cone_target_fiprod_cone. rw fimap2_fiprod_cone. tv. am. rww cone_source_fiprod_cone. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal