proposition: Lemma fob_fc_opp : forall a b f, Category.axioms a -> Category.axioms b -> ob (functor_cat (opp a) (opp b)) f -> fob (fc_opp a b) f = oppf f.
proof: Proof. ir. uf fob. rw fmor_fc_opp. rw source_flip. rw target_oppnt. rw source_id. tv. rw source_fc_opp. am. uf oppnt. uf create. rw source_fc_opp. rw id_functor_cat. rwi ob_functor_cat H1. uh H1; ee. rww vident_axioms. app opp_axioms. app opp_axioms. app opp_axioms. app opp_axioms. am. rw unfold_oppnt. uf oppnt'. uf create. rww Arrow.create_like. rw source_fc_opp. rw id_functor_cat. rwi ob_functor_cat H1. uh H1; ee. rww vident_axioms. app opp_axioms. app opp_axioms. app opp_axioms. app opp_axioms. am. rw source_fc_opp. ap mor_id. am. Qed.
imports: Arith nat_trans