proposition: Lemma target_fipr_dotted : forall a u v y1 y2, has_fiprod a u v -> fiprod_hypothesis a u v y1 y2 -> target (fipr_dotted a u v y1 y2) = source (fipr1 a u v).
proof: Proof. ir. cp (cone_composable_fipr_dotted H H0). uh H1; ee. rwi vertex_fiprod_cone H3. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal