proposition: Lemma fc_opp_axioms : forall a b, Category.axioms a -> Category.axioms b -> Functor.axioms (fc_opp a b).
proof: Proof. ir. assert (oax : Category.axioms (opp a)). app opp_axioms. assert (obx : Category.axioms (opp b)). app opp_axioms. uhg; ee. uf fc_opp. uf Functor.create. app Umorphism.create_like. rw source_fc_opp. ap functor_cat_axioms. app opp_axioms. app opp_axioms. rw target_fc_opp. ap opp_axioms. ap functor_cat_axioms. am. am. ir. rwi source_fc_opp H1. cp H1. rwi ob_functor_cat H2. uh H2; ee. rw target_fc_opp. rw ob_opp. rw fob_fc_opp. rw ob_functor_cat. uhg; ee. ap oppf_axioms. am. rww source_oppf. rw H3. rww opp_opp. rw target_oppf. rw H4. rww opp_opp. am. am. am. am. am. rw ob_functor_cat. uhg; ee. am. am. am. app opp_axioms. app opp_axioms. am. am. ir. rwi source_fc_opp H1. cp H1. rwi ob_functor_cat H2. uh H2; ee. assert (ob (functor_cat a b) (oppf x)). rw ob_functor_cat. uhg; ee. app oppf_axioms. rw source_oppf. rw H3. rww opp_opp. am. rw target_oppf. rw H4. rww opp_opp. am. am. am. rw target_fc_opp. rw fob_fc_opp. rw fmor_fc_opp. rw source_fc_opp. rw id_opp. ap uneq. rw id_functor_cat. rw id_functor_cat. rw vident_oppf. tv. am. am. am. rw ob_functor_cat. uhg; ee; try am. am. am. am. am. am. rw ob_opp. am. rw source_fc_opp. app mor_id. am. am. am. am. am. ir. cp H1. rwi source_fc_opp H2. cp H2. rwi mor_functor_cat H3. uh H3. ee. assert (mor (functor_cat a b) (oppnt u)). rw mor_functor_cat. uhg; ee. app oppnt_axioms. rw osource_oppnt. rw H4. rww opp_opp. am. rw otarget_oppnt. rw H5. rww opp_opp. am. am. am. rw target_fc_opp. rw mor_opp. rw mor_functor_cat. uhg; ee. rw fmor_fc_opp. rw flip_flip. app oppnt_axioms. am. rw fmor_fc_opp. rw flip_flip. rw osource_oppnt. rw H4. rww opp_opp. am. am. rw fmor_fc_opp. rw flip_flip. rw otarget_oppnt. rw H5. rww opp_opp. am. am. am. am. am. am. ir. cp H1. rwi source_fc_opp H2. cp H2. rwi mor_functor_cat H3. uh H3. ee. assert (mor (functor_cat a b) (oppnt u)). rw mor_functor_cat. uhg; ee. app oppnt_axioms. rw osource_oppnt. rw H4. rww opp_opp. am. rw otarget_oppnt. rw H5. rww opp_opp. am. am. am. rw fmor_fc_opp. rw source_flip. rw fob_fc_opp. rw target_oppnt. tv. am. am. am. rww ob_source. rw unfold_oppnt. uf oppnt'. uf create. rww Arrow.create_like. am. am. am. am. ir. cp H1. rwi source_fc_opp H2. cp H2. rwi mor_functor_cat H3. uh H3. ee. assert (mor (functor_cat a b) (oppnt u)). rw mor_functor_cat. uhg; ee. app oppnt_axioms. rw osource_oppnt. rw H4. rww opp_opp. am. rw otarget_oppnt. rw H5. rww opp_opp. am. am. am. rw fmor_fc_opp. rw target_flip. rw fob_fc_opp. rw source_oppnt. tv. am. am. am. rw ob_target. tv. am. rw unfold_oppnt. uf oppnt'. uf create. rww Arrow.create_like. am. am. am. am. ir. cp H1. rwi source_fc_opp H4. cp H4. rwi mor_functor_cat H5. uh H5. ee. assert (mor (functor_cat a b) (oppnt u)). rw mor_functor_cat. uhg; ee. app oppnt_axioms. rw osource_oppnt. rw H6. rww opp_opp. am. rw otarget_oppnt. rw H7. rww opp_opp. am. am. am. cp H2. rwi source_fc_opp H9. cp H9. rwi mor_functor_cat H10. uh H10. ee. assert (mor (functor_cat a b) (oppnt v)). rw mor_functor_cat. uhg; ee. app oppnt_axioms. rw osource_oppnt. rw H11. rww opp_opp. am. rw otarget_oppnt. rw H12. rww opp_opp. am. am. am. rw target_fc_opp. rw fmor_fc_opp. rw fmor_fc_opp. rw comp_opp. rw fmor_fc_opp. ap uneq. rw source_fc_opp. rw flip_flip. rw flip_flip. rw comp_functor_cat. rw comp_functor_cat. rw vcompose_oppnt. tv. am. am. am. am. am. am. am. am. am. am. am. am. rw source_oppnt. rw target_oppnt. rw H3. tv. am. am. rw source_fc_opp. rw mor_comp. tv. am. am. am. reflexivity. rw mor_opp. rw flip_flip. am. rw mor_opp. rw flip_flip. am. rw source_flip. rw target_flip. rw target_oppnt. rw source_oppnt. rww H3. am. am. apply mor_arrow_like with (functor_cat a b). am. apply mor_arrow_like with (functor_cat a b). am. am. am. am. am. am. am. Qed.
imports: Arith nat_trans