From 6272b4e84650b9833a53239b354770e0deba7b9a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 9 Dec 2025 13:25:39 -0600
Subject: Add shorter name for singleton setoid

---
 Data/Setoid/Unit.agda | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 Data/Setoid/Unit.agda

(limited to 'Data/Setoid/Unit.agda')

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} {ℓ}
-- 
cgit v1.2.3