From 7e7efc75650f08fb22b29d97cefbbd8a16c70ce1 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 7 Dec 2022 11:39:25 +0000 Subject: Prove map lifts a setoid function. --- src/Data/Setoid/Product.idr | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Data/Setoid/Product.idr') 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 @@ -94,6 +94,10 @@ mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is} -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys) 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) -- cgit v1.2.3