From aa13e2ec1d82ddb20888b1f60230de9798081bae Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 2 Dec 2022 16:15:31 +0000
Subject: Define indexed setoids.

---
 src/Data/Setoid/Indexed.idr | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 src/Data/Setoid/Indexed.idr

(limited to 'src/Data/Setoid/Indexed.idr')

diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr
new file mode 100644
index 0000000..5e9ef46
--- /dev/null
+++ b/src/Data/Setoid/Indexed.idr
@@ -0,0 +1,4 @@
+||| An indexed setoid is a type family equipped with a homogeneous equivalence relation
+module Data.Setoid.Indexed
+
+import public Data.Setoid.Indexed.Definition
-- 
cgit v1.2.3