proposition: Lemma constant_functor_axioms : forall a b x, Category.axioms a -> Category.axioms b -> ob b x -> Functor.axioms (constant_functor a b x).
proof: Proof. ir. uf constant_functor. ap Functor.create_axioms. sh (fun y:E => x). uhg; ee. am. am. ir. am. ir. tv. ir. cw. ir. cw. ir. cw. ir. cw. app mor_id. rww source_id. Qed.
imports: Arith category