proposition: Lemma cofi_hyp_fi_hyp : forall a u v y1 y2, Category.axioms a -> cofiprod_hypothesis a u v y1 y2 = fiprod_hypothesis (opp a) (flip u) (flip v) (flip y1) (flip y2).
proof: Proof. ir. ap iff_eq; ir. uh H0; uhg; ee. uh H0; uhg; ee. rww mor_opp. rww flip_flip. rww mor_opp. rww flip_flip. rw target_flip. rw target_flip. am. alike. alike. rww mor_opp. rww flip_flip. rw mor_opp; rww flip_flip. rw target_flip; try alike. rw source_flip; try alike. sy; am. uh H0; ee; alike. rw target_flip; try alike. rw source_flip; try alike. sy; am. uh H0; ee; alike. rw source_flip; try alike. rw source_flip; try alike. transitivity (target (comp a y1 u)). rw target_comp. tv. am. uh H0; ee; am. am. rw H5. rww target_comp. uh H0; ee; am. rw comp_opp. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. rw flip_flip. ap uneq. am. rww mor_opp; rww flip_flip. uh H0; ee; am. rww mor_opp; rww flip_flip. rww target_flip; try alike. rww source_flip; try alike. uh H0; ee. sy; am. uh H0; ee; alike. rww mor_opp; rww flip_flip. uh H0; ee; am. rww mor_opp; rww flip_flip. rww target_flip; try alike. rww source_flip; try alike. sy; am. uh H0; ee; alike. uh H0; ee. uh H0; ee. uhg; dj. uhg; dj. rwi mor_opp H0. rwi flip_flip H0. am. rwi mor_opp H7. rwi flip_flip H7. am. wr target_flip; try alike. rw H8. rw target_flip; try alike. tv. rwi mor_opp H1. rwi flip_flip H1; am. rwi mor_opp H2. rwi flip_flip H2; am. wr source_flip; try alike. rw H3. rww target_flip; try alike. rwi mor_opp H0. rwi flip_flip H0. alike. wr target_flip; try alike. wr H4. uh H9; ee. rww source_flip; try alike. rwi comp_opp H6. rwi flip_flip H6. rwi flip_flip H6. ap flip_eq. rw H6. rw comp_opp. rw flip_flip. rw flip_flip. tv. am. am. am. am. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal