proposition: Lemma point_functor_axioms : forall a b x, ob a x -> Category.axioms b -> Functor.axioms (point_functor a b x).
proof: Proof. ir. assert (Category.axioms a). uh H; ee; am. uf point_functor. ap Functor.create_axioms. sh (fun y => fob y x). uhg; dj. ap functor_cat_axioms. lu. am. am. rwi ob_functor_cat H4. uh H4; ee. wr H6. ap ob_fob. am. rww H5. am. am. rw id_functor_cat. rw ntrans_vident. rwi ob_functor_cat H5. uh H5; ee. rww H7. am. am. rwi ob_functor_cat H5. uh H5; ee. rww H6. am. am. am. am. am. rwi mor_functor_cat H6; ee. uh H6; ee. app mor_ntrans. rww H7. sy; am. am. am. rww source_ntrans. rwi mor_functor_cat H7; uh H7; ee. am. am. am. rwi mor_functor_cat H7; uh H7; ee. rww H8. am. am. rww target_ntrans. rwi mor_functor_cat H8; uh H8; ee. am. am. am. rwi mor_functor_cat H8; uh H8; ee. rww H9. am. am. rw comp_functor_cat. rw ntrans_vcompose. rwi mor_functor_cat H9; uh H9; ee. rww H13. am. am. rwi mor_functor_cat H10; uh H10; ee. rww H12. am. am. am. am. am. am. am. Qed.
imports: Arith nat_trans