diff options
Diffstat (limited to 'src/Data/Setoid/Product.idr')
| -rw-r--r-- | src/Data/Setoid/Product.idr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Setoid/Product.idr b/src/Data/Setoid/Product.idr index b1e8ce3..9fce498 100644 --- a/src/Data/Setoid/Product.idr +++ b/src/Data/Setoid/Product.idr @@ -95,6 +95,10 @@ mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is} mapIntro f = mapIntro' f.homomorphic public export +mapFunc : (f : x ~> y) -> Product x ~> Product y +mapFunc f = MkIndexedSetoidHomomorphism (\_ => map f.H) (\_, _, _ => mapIntro f) + +public export wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is} -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys) wrapIntro [] = [] |