proposition: Lemma constant_nt_axioms : forall a b u, Category.axioms a -> Category.axioms b -> mor b u -> axioms (constant_nt a b u).
proof: Proof. ir. uf constant_nt. ap create_axioms. cp H1. rwi mor_facts_rw H2. uh H2; ee. uhg; ee. app constant_functor_axioms. app constant_functor_axioms. rww source_constant_functor. rww source_constant_functor. rww target_constant_functor. rww target_constant_functor. ir. rww target_constant_functor. ir. rww fob_constant_functor. rwi source_constant_functor H8; am. ir. rwi source_constant_functor H8. rww fob_constant_functor. ir. rwi source_constant_functor H8. rww fmor_constant_functor. rww fmor_constant_functor. rw target_constant_functor. rww left_id. Qed.
imports: Arith functor