proposition: Lemma fipr_dotted_comp : forall a u v z, has_fiprod a u v -> mor a z -> source (fipr1 a u v) = target z -> fipr_dotted a u v (comp a (fipr1 a u v) z) (comp a (fipr2 a u v) z) = z.
proof: Proof. ir. assert (fiprod_hypothesis a u v (fipr1 a u v) (fipr2 a u v)). app fiprod_hypothesis_fiprod. ap fipr_dotted_uni. am. app fiprod_hypothesis_comp. uhg; ee. app is_cone_fiprod_cone. rww cone_target_fiprod_cone. rww vertex_fiprod_cone. sy; am. rw cone_compose_fiprod_cone. tv. am. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal