diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-07 11:39:25 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-07 11:39:25 +0000 |
| commit | 7e7efc75650f08fb22b29d97cefbbd8a16c70ce1 (patch) | |
| tree | 4f973970f3ee9d81d0a0fa058559c96c9fca057c | |
| parent | fcd024cb01e484dc3c92212f4317b254bbd7580b (diff) | |
Prove map lifts a setoid function.
| -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 [] = [] |