demote priority of cocartesian monoidal structure

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Oct 10, 2024 · e85030d · e85030d
1 parent 9ed2b66
commit e85030d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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).