proposition: Lemma fcompose_right_constant_functor : forall a b x f, Functor.axioms f -> source f = b -> Category.axioms a -> ob b x -> fcompose f (constant_functor a b x) = constant_functor a (target f) (fob f x).
proof: Proof. ir. ap constant_functor_criterion. rw source_fcompose. rw source_constant_functor. tv. rw target_fcompose. tv. ir. ap fcompose_axioms. am. ap constant_functor_axioms. am. wr H0; uh H; ee; am. am. rww target_constant_functor. fw. rww H0. ir. rww fmor_fcompose. rww fmor_constant_functor. fw. ap constant_functor_axioms. am. wr H0; uh H; ee; am. am. rww target_constant_functor. rww source_constant_functor. Qed.
imports: Arith category