proposition: Lemma show_is_cofiprod : forall a u v y1 y2, Category.axioms a -> cofiprod_hypothesis a u v y1 y2 -> (forall z z', mor a z -> mor a z' -> source z = target y1 -> source z' = target y1 -> comp a z y1 = comp a z' y1 -> comp a z y2 = comp a z' y2 -> z = z') -> (forall z1 z2, cofiprod_hypothesis a u v z1 z2 -> (exists w, (mor a w & source w = target y1 & comp a w y1 = z1 & comp a w y2 = z2))) -> is_cofiprod a u v y1 y2.
proof: Proof. ir. assert (lem1 : target y1 = target y2). uh H0. ee. transitivity (target (comp a y1 u)). rww target_comp. uh H0; ee; am. rw H7. rww target_comp. uh H0; ee; am. uhg; ee. am. ap show_is_fiprod. wr cofi_hyp_fi_hyp. am. am. ir. set (z1:=flip z). set (z2 := flip z'). assert (z1 = z2). ap H1. uf z1. rwi mor_opp H3. am. rwi mor_opp H4. am. uf z1. rw source_flip; try alike. wr H5. rww source_flip; try alike. uh H0; ee. alike. uf z2. rw source_flip; try alike. wr H6. rww source_flip; try alike. uh H0; ee. alike. uf z1; uf z2. rwi comp_opp H7. rwi flip_flip H7. rwi comp_opp H7. rwi flip_flip H7. rwi comp_opp H8. rwi flip_flip H8. rwi comp_opp H8. rwi flip_flip H8. ap flip_eq. am. rww mor_opp. rw flip_flip. uh H0; ee; am. am. uh H0; ee. rw source_flip. wr lem1. rwi source_flip H6. am. alike. alike. rww mor_opp. rw flip_flip. uh H0; ee; am. am. rw source_flip; try alike. wr lem1. rwi source_flip H5. am. uh H0; ee; alike. uh H0; ee; alike. rw mor_opp; rww flip_flip. uh H0; ee; am. am. am. rw mor_opp; rw flip_flip; uh H0; ee; am. am. am. uf z1; uf z2. rwi comp_opp H7. rwi flip_flip H7. rwi comp_opp H7. rwi flip_flip H7. rwi comp_opp H8. rwi flip_flip H8. rwi comp_opp H8. rwi flip_flip H8. ap flip_eq. am. rww mor_opp. rw flip_flip. uh H0; ee; am. am. uh H0; ee. rw source_flip. wr lem1. rwi source_flip H6. am. alike. alike. rww mor_opp. rw flip_flip. uh H0; ee; am. am. rw source_flip; try alike. wr lem1. rwi source_flip H5. am. uh H0; ee; alike. uh H0; ee; alike. rw mor_opp; rww flip_flip. uh H0; ee; am. am. am. rw mor_opp; rw flip_flip; uh H0; ee; am. am. am. ap flip_eq. am. ir. cp H3. set (z1' := flip z1). assert (z1= flip z1'). uf z1'; rww flip_flip. rwi H5 H4. set (z2' := flip z2). assert (z2= flip z2'). uf z2'; rww flip_flip. rwi H6 H4. wri cofi_hyp_fi_hyp H4. nin (H2 z1' z2' H4). ee. sh (flip x). ee. rww mor_opp. rww flip_flip. rw source_flip. rw target_flip. sy; am. alike. uh H0; ee; alike. rw comp_opp. rw flip_flip. rw flip_flip. ap flip_eq. rw flip_flip. exact H9. rww mor_opp. rw flip_flip. uh H0; ee; am. rww mor_opp. rww flip_flip. rw source_flip. rw target_flip. sy; am. alike. uh H0; ee; alike. rw comp_opp. rw flip_flip. rw flip_flip. ap flip_eq. rw flip_flip. exact H10. rw mor_opp; rw flip_flip. uh H0; ee; am. rw mor_opp; rww flip_flip. rw source_flip. rw target_flip. rww H8. sy; am. alike. uh H0; ee; alike. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal