proposition: Lemma fob_oppf' : forall f x, Functor.axioms f -> ob (source (oppf' f)) x -> fob (oppf' f) x = fob f x.
proof: Proof. ir. rwi source_oppf' H0. rwi ob_opp H0. uf fob. rw fmor_oppf'. rw source_flip. rw source_oppf'. rw id_opp. rw flip_flip. rw target_fmor. rw source_fmor. rw target_id. rww source_id. am. am. app mor_id. am. app mor_id. rw ob_opp. am. apply mor_arrow_like with (target f). ap mor_fmor. am. rw source_oppf'. rw id_opp. rw flip_flip. app mor_id. rww ob_opp. rw source_oppf'. rw mor_opp. rw id_opp. rw flip_flip. app mor_id. rww ob_opp. Qed.
imports: Arith category