proposition: Lemma source_fipr_dotted : forall a u v y1 y2, has_cofiprod a u v -> cofiprod_hypothesis a u v y1 y2 -> source (cofipr_dotted a u v y1 y2) = target (cofipr1 a u v).
proof: Proof. ir. rwi has_cofipr_has_fipr H. rwi cofi_hyp_fi_hyp H0. uf cofipr_dotted. rw source_flip. rw target_fipr_dotted. uf cofipr1. rw target_flip. tv. apply mor_arrow_like with (opp a). app mor_fipr1. am. am. apply mor_arrow_like with (opp a). app mor_fipr_dotted. uh H0; ee. uh H1; ee; am. uh H0; ee. uh H1; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal