proposition: Lemma is_constant_fcompose : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g -> is_constant g -> is_constant (fcompose f g).
proof: Proof. ir. uhg. ee. app fcompose_axioms. uh H2. ee. nin H3; ee. sh (fob f x). ee. fw. rww H1. rw source_fcompose. rw target_fcompose. ap constant_functor_criterion. rww source_fcompose. rww target_fcompose. app fcompose_axioms. app ob_fob. rww H1. ir. rww fmor_fcompose. rw H4. rww fmor_constant_functor. fw. Qed.
imports: Arith category