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