make the Functor of {Pre}MonoidalFunctor a parameter rather than a field

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 1ca2009..8355319 100644 (file)
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -32,21 +32,19 @@ Coercion mon_pm          : MonoidalCat >-> PreMonoidalCat.
 Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
 
 (* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
-Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) := PreMonoidalFunctor m1 m2.
+Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) {fobj}(F:Functor m1 m2 fobj) := PreMonoidalFunctor m1 m2 F.
 
 Definition MonoidalFunctorsCompose
-  `{M1   :MonoidalCat(C:=C1)}
-  `{M2   :MonoidalCat(C:=C2)}
+  `{PM1   :MonoidalCat(C:=C1)}
+  `{PM2   :MonoidalCat(C:=C2)}
    {fobj12:C1 -> C2                    }
-   (MF12 :MonoidalFunctor M1 M2 fobj12)
-  `{M3   :MonoidalCat(C:=C3)}
+   {PMFF12:Functor C1 C2 fobj12        }
+   (PMF12 :MonoidalFunctor PM1 PM2 PMFF12)
+  `{PM3   :MonoidalCat(C:=C3)}
    {fobj23:C2 -> C3                    }
-   (MF23 :MonoidalFunctor M2 M3 fobj23)
-   : MonoidalFunctor M1 M3 (fobj23 ○ fobj12).
-   apply PreMonoidalFunctorsCompose.
-   apply MF12.
-   apply MF23.
-   Defined.
+   {PMFF23:Functor C2 C3 fobj23        }
+   (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
+   := PreMonoidalFunctorsCompose PMF12 PMF23.
 
 Section BinoidalCat_from_Bifunctor.
   Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).

diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v
index 07513d8..fdda1a5 100644 (file)
--- a/src/PreMonoidalCategories.v
+++ b/src/PreMonoidalCategories.v
@@ -145,10 +145,11 @@ Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a
     Qed.
 
 Class PreMonoidalFunctor
-`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
-`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
- (fobj : C1 -> C2                 ) :=
-{ mf_F          :> Functor C1 C2 fobj
+`(PM1  : PreMonoidalCat(C:=C1)(I:=I1))
+`(PM2  : PreMonoidalCat(C:=C2)(I:=I2))
+ {fobj : C1 -> C2                 }
+ (F    : Functor C1 C2 fobj       ) :=
+{ mf_F          := F
 ; mf_i          :  I2 ≅ mf_F I1
 ; mf_first      :  ∀ a,              mf_F >>>> bin_first  (mf_F a)  <~~~>  bin_first  a >>>> mf_F
 ; mf_second     :  ∀ a,              mf_F >>>> bin_second (mf_F a)  <~~~>  bin_second a >>>> mf_F
@@ -166,10 +167,12 @@ Section PreMonoidalFunctorsCompose.
   `{PM1   :PreMonoidalCat(C:=C1)(I:=I1)}
   `{PM2   :PreMonoidalCat(C:=C2)(I:=I2)}
    {fobj12:C1 -> C2                    }
-   (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
+   {PMFF12:Functor C1 C2 fobj12        }
+   (PMF12 :PreMonoidalFunctor PM1 PM2 PMFF12)
   `{PM3   :PreMonoidalCat(C:=C3)(I:=I3)}
    {fobj23:C2 -> C3                    }
-   (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
+   {PMFF23:Functor C2 C3 fobj23        }
+   (PMF23 :PreMonoidalFunctor PM2 PM3 PMFF23).
 
   Definition compose_mf := PMF12 >>>> PMF23.
 
@@ -344,9 +347,8 @@ Section PreMonoidalFunctorsCompose.
       Implicit Arguments id [[Ob][Hom][Category]].
 
   (* this proof is really gross; I will write a better one some other day *)
-  Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
+  Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 compose_mf :=
   { mf_i      := compose_mf_i
-  ; mf_F      := compose_mf
   ; mf_first  := compose_mf_first  
   ; mf_second := compose_mf_second }.