From 6272b4e84650b9833a53239b354770e0deba7b9a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 9 Dec 2025 13:25:39 -0600 Subject: Add shorter name for singleton setoid --- Data/Monoid.agda | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'Data/Monoid.agda') 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′ -- cgit v1.2.3