proposition: Lemma constant_functor_criterion : forall a b x f, source f = a -> target f = b -> Functor.axioms f -> ob b x -> (forall u, mor a u -> fmor f u = id b x) -> f = constant_functor a b x.
proof: Proof. ir. ap axioms_extensionality. am. app constant_functor_axioms. wr H. uh H1; ee; am. wr H0; uh H1; ee; am. rww source_constant_functor. rww target_constant_functor. ir. rww fmor_constant_functor. ap H3. wrr H. wrr H. Qed.
imports: Arith category