proposition: Lemma oppf'_oppf' : forall f, Functor.axioms f -> oppf' (oppf' f) = f.
proof: Proof. ir. ap axioms_extensionality. app oppf'_axioms. app oppf'_axioms. am. rw source_oppf'. rw source_oppf'. rw opp_opp. tv. rw target_oppf'. rw target_oppf'. rw opp_opp. tv. ir. rwi source_oppf' H0. rwi source_oppf' H0. rwi opp_opp H0. rw fmor_oppf'. rw fmor_oppf'. rw flip_flip. rww flip_flip. rw source_oppf'. rw mor_opp. rw flip_flip. am. rw source_oppf'. rw source_oppf'. rw opp_opp. am. Qed.
imports: Arith category