proposition: Lemma fcompose_oppf' : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g -> fcompose (oppf' f) (oppf' g) = oppf' (fcompose f g).
proof: Proof. ir. assert (axioms (oppf' f)). app oppf'_axioms. assert (axioms (oppf' g)). app oppf'_axioms. assert (axioms (fcompose f g)). app fcompose_axioms. ap axioms_extensionality. ap fcompose_axioms. am. am. rw source_oppf'. rw target_oppf'. rww H1. ap oppf'_axioms. am. rw source_fcompose. rw source_oppf'. rw source_oppf'. rw source_fcompose. tv. rw target_fcompose. rw target_oppf'. rw target_oppf'. rw target_fcompose. tv. ir. rwi source_fcompose H5. cp H5. rwi source_oppf' H6. rwi mor_opp H6. rw fmor_fcompose. rw fmor_oppf'. rw fmor_oppf'. rw flip_flip. rw fmor_oppf'. rw fmor_fcompose. tv. am. am. am. am. rw source_oppf'. rw source_fcompose. rw mor_opp. am. am. assert (source (oppf' f) = target (oppf' g)). rw source_oppf'. rw target_oppf'. rw H1. tv. rw H7. ap mor_fmor. am. am. am. am. rw source_oppf'. rw target_oppf'. rw H1. tv. am. Qed.
imports: Arith category