proposition: Lemma oppf'_axioms : forall f, Functor.axioms f -> Functor.axioms (oppf' f).
proof: Proof. ir. uhg; ee. uf oppf'. uf create. ap Umorphism.create_like. rw source_oppf'. ap opp_axioms. lu. rw target_oppf'. ap opp_axioms. lu. ir. rw target_oppf'. rw fob_oppf'. rw ob_opp. ap ob_fob. am. rwi source_oppf' H0. rwi ob_opp H0. am. am. am. ir. cp H0. rwi source_oppf' H1. rwi ob_opp H1. rw target_oppf'. rw fmor_oppf'. rw source_oppf'. rw id_opp. rw id_opp. rw flip_flip. rw fmor_id. rw fob_oppf'. tv. am. am. am. tv. am. rww ob_opp. rw ob_opp. rw fob_oppf'. app ob_fob. am. am. rw source_oppf'. rw id_opp. rw mor_opp. rw flip_flip. app mor_id. rww ob_opp. ir. rw target_oppf'. rw fmor_oppf'. rw mor_opp. rw flip_flip. ap mor_fmor. am. rwi source_oppf' H0. rwi mor_opp H0. am. uh H; ee; am. ir. rw fmor_oppf'. rw source_flip. rw target_fmor. rw target_flip. rw fob_oppf'. tv. am. rw source_oppf'. rw ob_opp. assert (source u = target (flip u)). rww target_flip. apply mor_arrow_like with (source (oppf' f)). am. rw H1. rw ob_target. tv. rwi source_oppf' H0. rwi mor_opp H0. am. alike. am. rwi source_oppf' H0. rwi mor_opp H0. am. apply mor_arrow_like with (target f). ap mor_fmor. am. rwi source_oppf' H0. rwi mor_opp H0. am. uh H; ee; am. ir. rw fmor_oppf'. rw fob_oppf'. rw target_flip. rw source_fmor. rw source_flip. tv. apply mor_arrow_like with (source (oppf' f)). am. am. rwi source_oppf' H0. rwi mor_opp H0. am. apply mor_arrow_like with (target f). ap mor_fmor. am. rwi source_oppf' H0. rwi mor_opp H0. am. am. rw source_oppf'. rw ob_opp. assert (target u = source (flip u)). rww source_flip. apply mor_arrow_like with (source (oppf' f)). am. rw H1. rw ob_source. tv. rwi source_oppf' H0. rwi mor_opp H0. am. uh H; ee; am. ir. assert (Arrow.like u). apply mor_arrow_like with (source (oppf' f)). am. assert (Arrow.like v). apply mor_arrow_like with (source (oppf' f)). am. assert (mor (source f) (flip u)). rwi source_oppf' H0. rwi mor_opp H0. am. assert (mor (source f) (flip v)). rwi source_oppf' H1. rwi mor_opp H1. am. rw target_oppf'. rww fmor_oppf'. rww fmor_oppf'. rw comp_opp. rw flip_flip. rw flip_flip. rw fmor_oppf'. rw source_oppf'. rw comp_opp. rw flip_flip. rw comp_fmor. tv. am. am. am. rww source_flip. rww target_flip. sy; am. rww mor_opp. rww mor_opp. am. rww mor_comp. rw mor_opp. rw flip_flip. app mor_fmor. rw mor_opp. rw flip_flip. app mor_fmor. rw source_flip. rw target_flip. rw target_fmor. rw source_fmor. ap uneq. rww target_flip. rww source_flip. am. am. am. am. apply mor_arrow_like with (target f). app mor_fmor. apply mor_arrow_like with (target f). app mor_fmor. Qed.
imports: Arith category