diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-09 13:25:39 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-09 13:25:39 -0600 |
| commit | 6272b4e84650b9833a53239b354770e0deba7b9a (patch) | |
| tree | d69dfd53369f4630fe9e8beceabad3ac55a1dc0e /Data/Monoid.agda | |
| parent | 3c62ac510f286f228c9993fe6c37abdcad9e1fb2 (diff) | |
Add shorter name for singleton setoid
Diffstat (limited to 'Data/Monoid.agda')
| -rw-r--r-- | Data/Monoid.agda | 4 |
1 files changed, 1 insertions, 3 deletions
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′ |