From 2cd74f160389fe2ab2b30ab628fbb9b712f06faf Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 28 Oct 2025 12:34:23 -0500
Subject: Split System into smaller modules

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

(limited to 'Data/Setoid.agda')

diff --git a/Data/Setoid.agda b/Data/Setoid.agda
new file mode 100644
index 0000000..454d276
--- /dev/null
+++ b/Data/Setoid.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Setoid where
+
+open import Relation.Binary using (Setoid)
+open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public
+
+open Setoid renaming (Carrier to ∣_∣) public
-- 
cgit v1.2.3