+Lemma functor_comp_assoc `{C':Category}`{D:Category}`{E:Category}`{F:Category}
+ {F1obj}(F1:Functor C' D F1obj)
+ {F2obj}(F2:Functor D E F2obj)
+ {F3obj}(F3:Functor E F F3obj)
+ `(f:a~>b) :
+ ((F1 >>>> F2) >>>> F3) \ f ~~ (F1 >>>> (F2 >>>> F3)) \ f.
+ intros; simpl.
+ reflexivity.
+ Qed.