diff options
| -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 |