Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
Require Import Enrichment_ch2_8.
apply MonoidalFunctorsCompose.
apply MonoidalFunctorsCompose.
apply (ga_functor_monoidal g01).
apply MonoidalFunctorsCompose.
apply MonoidalFunctorsCompose.
apply (ga_functor_monoidal g01).