From e62bc618513cd9daa9f5cbcc98daa3a4fbf9fb99 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 6 Dec 2025 16:31:59 -0600
Subject: Make setoids monoidal structure opaque

---
 Category/Instance/Setoids/SymmetricMonoidal.agda | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'Category/Instance/Setoids')

diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
index 8f448dc..f21124e 100644
--- a/Category/Instance/Setoids/SymmetricMonoidal.agda
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -17,11 +17,23 @@ open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ))
 open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal)
 open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric)
 
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+
+opaque
+
+  ×-monoidal′ : Monoidal (Setoids c ℓ)
+  ×-monoidal′ = ×-monoidal {c} {ℓ}
+
+  ×-symmetric′ : Symmetric ×-monoidal′
+  ×-symmetric′ = ×-symmetric
+
 Setoids-× : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
 Setoids-× = record
     { U = Setoids c ℓ
-    ; monoidal = ×-monoidal
-    ; symmetric = ×-symmetric
+    ; monoidal = ×-monoidal′
+    ; symmetric = ×-symmetric′
     }
 
 Setoids-+ : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
-- 
cgit v1.2.3