proposition: Lemma fob_point_functor : forall a b x y, Category.axioms a -> Category.axioms b -> ob (functor_cat a b) y -> ob a x -> fob (point_functor a b x) y = fob y x.
proof: Proof. ir. uf point_functor. rw Functor.fob_create. rw source_ntrans. rw source_id. tv. am. rw id_functor_cat. rww vident_axioms. rwi ob_functor_cat H1. lu. am. am. am. am. am. rw id_functor_cat. rw osource_vident. rwi ob_functor_cat H1. uh H1; ee. rww H3. am. am. am. am. am. am. Qed.
imports: Arith nat_trans