From: Adam Megacz <adam@megacz.com>
Date: Tue, 22 Mar 2011 00:45:46 +0000 (-0700)
Subject: make the codomain of the FreydCategory functor a parameter rather than a field
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=f4d377789a2265a19ff3d1dd65e87f570aef49c3;hp=d490aac37c55dcdaaf3fca152846f13acbb447c6

make the codomain of the FreydCategory functor a parameter rather than a field
---

diff --git a/src/FreydCategories.v b/src/FreydCategories.v
index de6e4ee..7fe727d 100644
--- a/src/FreydCategories.v
+++ b/src/FreydCategories.v
@@ -23,9 +23,11 @@ Class FreydCategory
 { freyd_C                     :  Category Ob HomC                       }
 { freyd_C_terminal            :  Terminal    freyd_C                    }
 { freyd_C_binoidal            :  BinoidalCat freyd_C freyd_bobj         }
-( freyd_C_monoidal            :  PreMonoidalCat freyd_C_binoidal 1         ) :=
-{ freyd_K_hom                 :  Ob -> Ob -> Type
-; freyd_K                     :> Category Ob freyd_K_hom
+( freyd_C_monoidal            :  PreMonoidalCat freyd_C_binoidal 1      )
+{ freyd_K_hom                 :  Ob -> Ob -> Type                       }
+( freyd_K                     :  Category Ob freyd_K_hom                )
+:=
+{ freyd_K_                    := freyd_K
 ; freyd_C_cartesian           :  CartesianCat freyd_C_monoidal
 ; freyd_K_binoidal            :> BinoidalCat  freyd_K freyd_bobj
 ; freyd_K_monoidal            :> PreMonoidalCat  freyd_K_binoidal (one(Terminal:=freyd_C_terminal))
@@ -41,4 +43,4 @@ Class FreydCategory
 }.
 Coercion freyd_K_monoidal : FreydCategory >-> PreMonoidalCat.
 Coercion freyd_F          : FreydCategory >-> PreMonoidalFunctor.
-Coercion freyd_K          : FreydCategory >-> Category.
+Coercion freyd_K_         : FreydCategory >-> Category.