From: Adam Megacz Date: Sat, 9 Apr 2011 09:00:03 +0000 (+0000) Subject: FreydCategories: add strictness requirement for unit object X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=658181bed516646957267b055341d9d4b197ed0d;ds=inline FreydCategories: add strictness requirement for unit object --- 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