proposition: Lemma opp_fc_axioms : forall a b, Category.axioms a -> Category.axioms b -> Functor.axioms (opp_fc a b).
proof: Proof. ir. assert (oax : Category.axioms (opp a)). app opp_axioms. assert (obx :Category.axioms (opp b)). app opp_axioms. assert (fcox : Category.axioms (functor_cat (opp a) (opp b))). ap functor_cat_axioms. am. am. assert (ofcx : Category.axioms (opp (functor_cat a b))). ap opp_axioms. ap functor_cat_axioms. am. am. assert (sfcx : Category.axioms (source (opp_fc a b))). rw source_opp_fc. am. assert (tfcx : Category.axioms (target (opp_fc a b))). rw target_opp_fc. am. assert (fcx : Category.axioms (functor_cat a b)). ap functor_cat_axioms. am. am. uhg; ee. uf opp_fc. uf Functor.create. ap Umorphism.create_like. am. am. ir. cp H1. rwi source_opp_fc H2. cp H2. rwi ob_opp H3. cp H3. rwi ob_functor_cat H4. uh H4; ee. assert (ob (functor_cat (opp a) (opp b)) (oppf x)). rw ob_functor_cat. uhg; ee. ap oppf_axioms. am. rw source_oppf. rww H5. am. rw target_oppf. rww H6. am. am. am. rw target_opp_fc. rw fob_opp_fc. am. am. am. am. am. am. ir. cp H1. rwi source_opp_fc H2. cp H2. rwi ob_opp H3. cp H3. rwi ob_functor_cat H4. uh H4; ee. assert (ob (functor_cat (opp a) (opp b)) (oppf x)). rw ob_functor_cat. uhg; ee. ap oppf_axioms. am. rw source_oppf. rww H5. am. rw target_oppf. rw H6. tv. am. am. am. rw target_opp_fc. rw fob_opp_fc. rw fmor_opp_fc. rw source_opp_fc. rw id_functor_cat. rw id_opp. rw flip_flip. rw id_functor_cat. rw vident_oppf. tv. am. am. am. am. rw ob_opp. am. am. am. am. rw source_opp_fc. ap mor_id. am. am. am. am. am. am. ir. cp H1. rwi source_opp_fc H2. cp H2. rwi mor_opp H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. assert (axioms (oppnt (flip u))). ap oppnt_axioms. am. rw target_opp_fc. rw fmor_opp_fc. rw mor_functor_cat. uhg; ee. am. rw osource_oppnt. rww H5. am. rw otarget_oppnt. rww H6. am. am. am. am. am. am. ir. cp H1. rwi source_opp_fc H2. cp H2. rwi mor_opp H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. assert (axioms (oppnt (flip u))). ap oppnt_axioms. am. assert (Arrow.like u). apply mor_arrow_like with (source (opp_fc a b)). am. rw fmor_opp_fc. rw fob_opp_fc. rw source_oppnt. rww target_flip. rwi axioms_oppnt H7. am. am. am. rww ob_source. am. am. am. ir. cp H1. rwi source_opp_fc H2. cp H2. rwi mor_opp H3. cp H3. rwi mor_functor_cat H4. uh H4; ee. assert (axioms (oppnt (flip u))). ap oppnt_axioms. am. assert (Arrow.like u). apply mor_arrow_like with (source (opp_fc a b)). am. rw fmor_opp_fc. rw fob_opp_fc. rw target_oppnt. rww source_flip. am. am. am. rww ob_target. am. am. am. ir. cp H1. rwi source_opp_fc H4. cp H4. rwi mor_opp H5. cp H5. rwi mor_functor_cat H6. uh H6; ee. assert (axioms (oppnt (flip u))). ap oppnt_axioms. am. assert (Arrow.like u). apply mor_arrow_like with (source (opp_fc a b)). am. cp H2. rwi source_opp_fc H11. cp H11. rwi mor_opp H12. cp H12. rwi mor_functor_cat H13. uh H13; ee. assert (axioms (oppnt (flip v))). ap oppnt_axioms. am. assert (Arrow.like v). apply mor_arrow_like with (source (opp_fc a b)). am. assert (source (flip v) = target (flip u)). rw source_flip. rw target_flip. sy; am. am. am. assert (mor (functor_cat (opp a) (opp b)) (oppnt (flip u))). rw mor_functor_cat. uhg; ee. am. rw osource_oppnt. rww H7. am. rw otarget_oppnt. ap uneq; am. am. am. am. assert (mor (functor_cat (opp a) (opp b)) (oppnt (flip v))). rw mor_functor_cat. uhg; ee. am. rw osource_oppnt. ap uneq; am. am. rw otarget_oppnt. ap uneq; am. am. am. am. rw target_opp_fc. rw fmor_opp_fc. rw fmor_opp_fc. rw fmor_opp_fc. rw source_opp_fc. rw comp_functor_cat. rw comp_opp. rw flip_flip. rw comp_functor_cat. rw vcompose_oppnt. reflexivity. am. am. am. am. am. am. am. am. am. am. am. am. am. am. am. rw source_oppnt. rw target_oppnt. ap uneq. sy; am. am. am. rw source_opp_fc. rw mor_comp. tv. am. am. am. tv. am. am. am. am. am. am. Qed.
imports: Arith nat_trans