From 658181bed516646957267b055341d9d4b197ed0d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 9 Apr 2011 09:00:03 +0000 Subject: [PATCH] FreydCategories: add strictness requirement for unit object --- src/FreydCategories.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/FreydCategories.v b/src/FreydCategories.v index b0024fc..8b921df 100644 --- a/src/FreydCategories.v +++ b/src/FreydCategories.v @@ -25,7 +25,7 @@ Class FreydCategory `(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj)) (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *) - `(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=pmon_I(PreMonoidalCat:=C))) + `(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=pmon_I C)) (* an identity-on-objects functor J:C->Z(K) *) := { fc_J : Functor C (Center_is_Monoidal K) (fun x => x) @@ -35,7 +35,7 @@ Class FreydCategory (* and strict (meaning the functor's coherence maps are identities) *) ; fc_strict_first : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _ (* mf_consistent gives us mf_second *) -(* ; fc_strict_id : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _*) + ; fc_strict_id : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _ ; fc_C := C ; fc_K := K -- 1.7.10.4