aboutsummaryrefslogtreecommitdiff
path: root/Category
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-12-09 13:25:39 -0600
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-12-09 13:25:39 -0600
commit6272b4e84650b9833a53239b354770e0deba7b9a (patch)
treed69dfd53369f4630fe9e8beceabad3ac55a1dc0e /Category
parent3c62ac510f286f228c9993fe6c37abdcad9e1fb2 (diff)
Add shorter name for singleton setoid
Diffstat (limited to 'Category')
-rw-r--r--Category/Instance/Setoids/SymmetricMonoidal.agda3
1 files changed, 3 insertions, 0 deletions
diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
index f21124e..995ddf3 100644
--- a/Category/Instance/Setoids/SymmetricMonoidal.agda
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -42,3 +42,6 @@ Setoids-+ = record
; monoidal = +-monoidal
; symmetric = +-symmetric
}
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+module Setoids-+ = SymmetricMonoidalCategory Setoids-+