1 files changed, 18 insertions, 0 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index f92c23c..c4a2acc 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -2,6 +2,7 @@ module Soat.Data.Product
 
 import Control.Relation
 import Data.List.Elem
+import Soat.Relation
 
 %default total
 
@@ -67,6 +68,23 @@ map f []        = []
 map f (x :: xs) = f _ x :: map f xs
 
 public export
+indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is)
+  -> index (map f xs) elem = f i (index xs elem)
+indexMap (x :: xs) Here         = Refl
+indexMap (x :: xs) (There elem) = indexMap xs elem
+
+public export
+mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
+mapId []        = Refl
+mapId (x :: xs) = cong ((::) x) $ mapId xs
+
+public export
+mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is)
+  -> map (\i => f i . g i) xs = map f (map g xs)
+mapComp []        = Refl
+mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs
+
+public export
 (++) : x ^ is -> x ^ js -> x ^ (is ++ js)
 (++) []        ys = ys
 (++) (x :: xs) ys = x :: (xs ++ ys)