proposition: Lemma constant_functor_is_constant : forall a b x, Category.axioms a -> ob b x -> is_constant (constant_functor a b x).
proof: Proof. ir. uhg. ee. ap constant_functor_axioms. am. lu. am. sh x; ee. fw. rw source_constant_functor. rw target_constant_functor. tv. Qed.
imports: Arith category