proposition: Lemma cofiprod_hypothesis_comp : forall a u v y1 y2 z, cofiprod_hypothesis a u v y1 y2 -> mor a z -> source z = target y1 -> cofiprod_hypothesis a u v (comp a z y1) (comp a z y2).
proof: Proof. ir. rw cofi_hyp_fi_hyp. rwi cofi_hyp_fi_hyp H. assert (flip (comp a z y1) = comp (opp a) (flip y1) (flip z)). rw comp_opp. rw flip_flip. rww flip_flip. uh H; ee; am. rww mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip. sy; am. alike. uh H; ee. rwi mor_opp H2. rwi flip_flip H2; alike. assert (flip (comp a z y2) = comp (opp a) (flip y2) (flip z)). rw comp_opp. rw flip_flip. rww flip_flip. uh H; ee; am. rww mor_opp. rww flip_flip. uh H; ee. wr H7. rw source_flip; try alike. rw target_flip. sy; am. alike. rwi mor_opp H3. rwi flip_flip H3; alike. rw H2; rw H3. ap fiprod_hypothesis_comp. am. rww mor_opp. rww flip_flip. rw source_flip; try alike. rw target_flip. sy; am. alike. uh H; ee. rwi mor_opp H4. rwi flip_flip H4; alike. uh H0; ee; am. uh H0; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal