From f494aec0e2a8f5ccb7a5f560dd4f8a0b302feb40 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 02:36:25 +0000 Subject: [PATCH] make EBinoidalCat action-on-objects a parameter instead of field --- src/Enrichment_ch2_8.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v index a3f4c3e..3d3aac9 100644 --- a/src/Enrichment_ch2_8.v +++ b/src/Enrichment_ch2_8.v @@ -363,11 +363,11 @@ Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 Defined. Coercion UnderlyingFunctor : EFunctor >-> Functor. -Class EBinoidalCat `(ec:ECategory) := -{ ebc_bobj : ec -> ec -> ec -; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a) -; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x) +Class EBinoidalCat `(ec:ECategory)(bobj : ec -> ec -> ec) := +{ ebc_first : forall a:ec, EFunctor ec ec (fun x => bobj x a) +; ebc_second : forall a:ec, EFunctor ec ec (fun x => bobj a x) ; ebc_ec := ec (* this isn't a coercion - avoids duplicate paths *) +; ebc_bobj := bobj }. Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj. -- 1.7.10.4