-Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
- GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
- intro g01.
- intro g12.
- refine
- {| ga_functor := g01 >>>> RepresentableFunctor s1 (mon_i s1) >>>> g12 |}.
- apply MonoidalFunctorsCompose.
- apply MonoidalFunctorsCompose.
- apply (ga_functor_monoidal g01).
- apply (me_mf s1).
- apply (ga_functor_monoidal g12).
- Defined.
+Instance compose_generalizedArrows (s0 s1 s2:SMMEs)
+ (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 :=
+ { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }.
+ apply ga_host_lang_pure.
+ Defined.