proposition: Lemma point_trans_axioms : forall a b u, mor a u -> Category.axioms b -> Nat_Trans.axioms (point_trans a b u).
proof: Proof. ir. assert (lem1 : Category.axioms a). uh H; ee; am. uf point_trans. ap Nat_Trans.create_axioms. uhg; dj. ap point_functor_axioms. rwi mor_facts_rw H; lu. am. ap point_functor_axioms. rwi mor_facts_rw H; lu. am. rw source_point_functor. rw source_point_functor. tv. rw target_point_functor. rw target_point_functor. tv. rw target_point_functor. rwi source_point_functor H5. rwi ob_functor_cat H5. uh H5; ee. wr H7. ap mor_fmor. am. rww H6. am. am. rwi source_point_functor H6. cp H6. rwi ob_functor_cat H7. uh H7; ee. rww fob_point_functor. rww source_fmor. rww H8. rww ob_source. am. am. rwi source_point_functor H7. cp H7. rwi ob_functor_cat H7. uh H7; ee. rww fob_point_functor. rww target_fmor. rww H9. rww ob_target. am. am. rwi source_point_functor H8. cp H8. rwi mor_functor_cat H8. uh H8; ee. rww target_point_functor. rww fmor_point_functor. rww fmor_point_functor. wr H11. rw carre. tv. am. rww H10. am. am. Qed.
imports: Arith nat_trans