From e85030dc3a80a281718d31a38f2fa433f0246404 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 10 Oct 2024 11:51:08 +0100 Subject: [PATCH] demote priority of cocartesian monoidal structure Signed-off-by: Ali Caglayan --- theories/WildCat/Coproducts.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v index f1ae1fcb3a5..d191f0f5516 100644 --- a/theories/WildCat/Coproducts.v +++ b/theories/WildCat/Coproducts.v @@ -381,7 +381,7 @@ Definition cat_bincoprod_swap_rec {A : Type} `{Is1Cat A} Global Instance ismonoidal_cat_bincoprod {A : Type} `{HasEquivs A} `{!HasBinaryCoproducts A} (zero : A) `{!IsInitial zero} - : IsMonoidal A (fun x y => cat_bincoprod x y) zero. + : IsMonoidal A (fun x y => cat_bincoprod x y) zero | 10. Proof. nrapply ismonoidal_op'. nrapply (ismonoidal_cat_binprod (A:=A^op) zero). @@ -390,7 +390,7 @@ Defined. Global Instance issymmetricmonoidal_cat_bincoprod {A : Type} `{HasEquivs A} `{!HasBinaryCoproducts A} (zero : A) `{!IsInitial zero} - : IsSymmetricMonoidal A (fun x y => cat_bincoprod x y) zero. + : IsSymmetricMonoidal A (fun x y => cat_bincoprod x y) zero | 10. Proof. nrapply issymmetricmonoidal_op'. nrapply (issymmetricmonoidal_cat_binprod (A:=A^op) zero).