diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:40:03 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:40:03 +0000 |
| commit | 57a299ee52f29aa553a9d93c24f4c1e9eee4fa27 (patch) | |
| tree | 95b673758c571932dd4127dee5bd684f10c2c54e | |
| parent | a34e0b84874ff1c7f348821c65af660d1de3ece0 (diff) | |
Define the trivial indexed setoid.
| -rw-r--r-- | src/Soat/Relation.idr | 4 |
1 files changed, 4 insertions, 0 deletions
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 @@ -75,6 +75,10 @@ record ISetoid (a : Type) where 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 |