From 57a299ee52f29aa553a9d93c24f4c1e9eee4fa27 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 25 Nov 2022 15:40:03 +0000
Subject: Define the trivial indexed setoid.

---
 src/Soat/Relation.idr | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src')

diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr
index cb94216..6d6b691 100644
--- a/src/Soat/Relation.idr
+++ b/src/Soat/Relation.idr
@@ -74,6 +74,10 @@ record ISetoid (a : Type) where
   0 relation  : IRel U
   equivalence : IEquivalence U relation
 
+public export
+isetoid : (a -> Type) -> ISetoid a
+isetoid u = MkISetoid u (\_ => Equal) (\_ => equiv)
+
 public export
 IFunc : {a : Type} -> (x, y : a -> Type) -> Type
 IFunc {a} x y = (i : a) -> x i -> y i
-- 
cgit v1.2.3