From f4d377789a2265a19ff3d1dd65e87f570aef49c3 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 21 Mar 2011 17:45:46 -0700 Subject: [PATCH 1/1] make the codomain of the FreydCategory functor a parameter rather than a field --- src/FreydCategories.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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. -- 1.7.10.4