proposition: Lemma cofipr_dotted_comp : forall a u v z, has_cofiprod a u v -> mor a z -> source z = target (cofipr1 a u v) -> cofipr_dotted a u v (comp a z (cofipr1 a u v)) (comp a z (cofipr2 a u v)) = z.
proof: Proof. ir. cp H. rwi has_cofipr_has_fipr H. assert (cofiprod_hypothesis a u v (comp a z (cofipr1 a u v)) (comp a z (cofipr2 a u v))). app cofiprod_hypothesis_comp. app cofiprod_hypothesis_cofiprod. rwi cofi_hyp_fi_hyp H3. uf cofipr_dotted. assert (flip (comp a z (cofipr1 a u v)) = comp (opp a) (fipr1 (opp a) (flip u) (flip v)) (flip z)). rw comp_opp. sy; rw flip_flip. uf cofipr1. tv. app mor_fipr1. rww mor_opp. rww flip_flip. ufi cofipr1 H1. rwi target_flip H1. wr H1. rww target_flip. alike. apply mor_arrow_like with (opp a). app mor_fipr1. assert (flip (comp a z (cofipr2 a u v)) = comp (opp a) (fipr2 (opp a) (flip u) (flip v)) (flip z)). rw comp_opp. sy; rw flip_flip. uf cofipr2. tv. app mor_fipr2. rww mor_opp. rww flip_flip. assert (lem1 : source z = target (cofipr2 a u v)). rw target_cofipr2. am. am. ufi cofipr2 lem1. rwi target_flip lem1. wr lem1. rww target_flip. alike. apply mor_arrow_like with (opp a). app mor_fipr2. rw H4. rw H5. rw fipr_dotted_comp. rww flip_flip. am. rw mor_opp. rww flip_flip. ufi cofipr1 H1. rwi target_flip H1. wr H1. rww target_flip. alike. apply mor_arrow_like with (opp a). app mor_fipr1. uh H0; ee; am. uh H0; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal