Add shorter name for singleton setoid

4 files changed, 14 insertions, 6 deletions

diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
index 6aec0c8..8aaf869 100644
--- a/Data/CMonoid.agda
+++ b/Data/CMonoid.agda
@@ -9,7 +9,6 @@ open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoi
 open import Categories.Object.Monoid using (Monoid)
 
 open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
 
 import Algebra.Bundles as Alg
 
@@ -39,7 +38,7 @@ toCMonoid M = record
       comm x y = commutative {x , y}
 
 open import Function.Construct.Constant using () renaming (function to Const)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 
 fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
 fromCMonoid M = record
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
index dba3e79..1ba0af4 100644
--- a/Data/Monoid.agda
+++ b/Data/Monoid.agda
@@ -7,8 +7,6 @@ open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory
 open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
 open import Categories.Object.Monoid using (Monoid; Monoid⇒)
 
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-
 import Algebra.Bundles as Alg
 
 open import Data.Setoid using (∣_∣)
@@ -20,7 +18,7 @@ open Func
 -- A monoid object in the (monoidal) category of setoids is just a monoid
 
 open import Function.Construct.Constant using () renaming (function to Const)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 
 opaque
   unfolding ×-monoidal′
diff --git a/Data/Setoid/Unit.agda b/Data/Setoid/Unit.agda
new file mode 100644
index 0000000..8b8edde
--- /dev/null
+++ b/Data/Setoid/Unit.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Setoid.Unit {c ℓ : Level} where
+
+open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Relation.Binary using (Setoid)
+
+⊤ₛ : Setoid c ℓ
+⊤ₛ = SingletonSetoid {c} {ℓ}
diff --git a/Data/System.agda b/Data/System.agda
index 5d5e484..d71c2a8 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -8,10 +8,10 @@ import Relation.Binary.Properties.Preorder as PreorderProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Categories.Category using (Category)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Data.Circuit.Value using (Monoid)
 open import Data.Nat using (ℕ)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Data.System.Values Monoid using (Values; _≋_; module ≋; <ε>)
 open import Function using (Func; _⟨$⟩_; flip)
 open import Function.Construct.Constant using () renaming (function to Const)