1 files changed, 64 insertions, 0 deletions
diff --git a/src/Data/Setoid/Vect/Functional.idr b/src/Data/Setoid/Vect/Functional.idr
new file mode 100644
index 0000000..8fd6e3b
--- /dev/null
+++ b/src/Data/Setoid/Vect/Functional.idr
@@ -0,0 +1,64 @@
+||| The setoid of vectors over a given setoid, defined using a function
+module Data.Setoid.Vect.Functional
+
+import Data.Setoid.Definition
+
+import Data.Vect
+import Data.HVect
+import Data.Vect.Properties
+import Data.Setoid.Vect.Inductive
+import Control.Order
+import Syntax.PreorderReasoning.Setoid
+
+
+%default total
+
+public export
+0 (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a))
+a.VectEquality xs ys = (i : Fin n) ->
+  a.equivalence.relation (index i xs) (index i ys)
+
+-- Not using the more sensible type definition
+-- Inductive.(.VectEquality) a xs ys -> Functional.(.VectEquality) a xs ys
+-- so that the arguments are in the order as Vect's index.
+export
+index : (i : Fin n) ->
+        Inductive.(.VectEquality) a xs ys ->
+        a.equivalence.relation (index i xs) (index i ys)
+index FZ     (hdEq :: _) = hdEq
+index (FS k) (_ :: tlEq) = index k tlEq
+
+%hide Inductive.(.VectEquality)
+%hide Inductive.VectSetoid
+
+public export
+VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
+VectSetoid n a = MkSetoid (Vect n (U a))
+  $ MkEquivalence
+  { relation   = (.VectEquality) a
+  , reflexive  = \xs                    , i =>
+      a.equivalence.reflexive  _
+  , symmetric  = \xs,ys, prf            , i =>
+      a.equivalence.symmetric  _ _   (prf  i)
+  , transitive = \xs, ys, zs, prf1, prf2, i =>
+      a.equivalence.transitive _ _ _ (prf1 i) (prf2 i)
+  }
+
+public export
+VectMap : {a, b : Setoid} -> (a ~~> b) ~>
+  (VectSetoid n a ~~> VectSetoid n b)
+VectMap = MkSetoidHomomorphism
+  (\f => MkSetoidHomomorphism
+    (\xs => map f.H xs)
+    $ \xs, ys, prf, i  => CalcWith b $
+    |~ index i (map f.H xs)
+    ~~ f.H (index i xs)
+                        .=.(indexNaturality _ _ _)
+    ~~ f.H (index i ys) ...(f.homomorphic _ _ $ prf i)
+    ~~ index i (map f.H ys)
+                          .=<(indexNaturality _ _ _))
+  $ \f,g,prf,xs,i => CalcWith b $
+  |~ index i (map f.H xs)
+  ~~ f.H (index i xs) .=.(indexNaturality _ _ _)
+  ~~ g.H (index i xs) ...(prf _)
+  ~~ index i (map g.H xs) .=<(indexNaturality _ _ _)