1 files changed, 11 insertions, 0 deletions
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} {ℓ}