From efd5f75c0672773341b5ca1c1d4b2ad0c0d09daa Mon Sep 17 00:00:00 2001
From: Ohad Kammar <ohad.kammar@ed.ac.uk>
Date: Sun, 7 Aug 2022 18:23:04 +0100
Subject: Initial version

---
 src/Data/Setoid/Vect/Inductive.idr | 78 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 src/Data/Setoid/Vect/Inductive.idr

(limited to 'src/Data/Setoid/Vect/Inductive.idr')

diff --git a/src/Data/Setoid/Vect/Inductive.idr b/src/Data/Setoid/Vect/Inductive.idr
new file mode 100644
index 0000000..28076c5
--- /dev/null
+++ b/src/Data/Setoid/Vect/Inductive.idr
@@ -0,0 +1,78 @@
+||| The setoid of vectors over a given setoid, defined inductively
+module Data.Setoid.Vect.Inductive
+
+import Data.Setoid.Definition
+
+import Data.Vect
+import Data.HVect
+import Data.Vect.Properties
+
+%default total
+
+public export
+data (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a)) where
+  Nil : a.VectEquality [] []
+  (::) : (hdEq : a.equivalence.relation x y) ->
+         (tlEq : a.VectEquality xs ys) ->
+         a.VectEquality (x :: xs) (y :: ys)
+
+export
+(++) : a.VectEquality xs ys -> a.VectEquality as bs ->
+       a.VectEquality (xs ++ as) (ys ++ bs)
+[] ++ qs = qs
+(p :: ps) ++ qs = p :: (ps ++ qs)
+
+public export
+(.VectEqualityReflexive) : (a : Setoid) -> (xs : Vect n $ U a) -> a.VectEquality xs xs
+a.VectEqualityReflexive [] = []
+a.VectEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.VectEqualityReflexive xs
+
+public export
+(.VectEqualitySymmetric) : (a : Setoid) -> (xs,ys : Vect n $ U a) -> (prf : a.VectEquality xs ys) ->
+  a.VectEquality ys xs
+a.VectEqualitySymmetric [] [] [] = []
+a.VectEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
+  = a.equivalence.symmetric x y hdEq :: a.VectEqualitySymmetric xs ys tlEq
+
+public export
+(.VectEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : Vect n $ U a) ->
+  (prf1 : a.VectEquality xs ys) -> (prf2 : a.VectEquality ys zs) ->
+  a.VectEquality xs zs
+a.VectEqualityTransitive [] [] [] [] [] = []
+a.VectEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
+  = a.equivalence.transitive x  y  z  hdEq1 hdEq2 ::
+    a.VectEqualityTransitive xs ys zs tlEq1 tlEq2
+
+public export
+VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
+VectSetoid n a = MkSetoid (Vect n (U a))
+  $ MkEquivalence
+  { relation   = a.VectEquality
+  , reflexive  = a.VectEqualityReflexive
+  , symmetric  = a.VectEqualitySymmetric
+  , transitive = a.VectEqualityTransitive
+  }
+
+public export
+VectMapFunctionHomomorphism : (f : a ~> b) ->
+  SetoidHomomorphism (VectSetoid n a) (VectSetoid n b) (map f.H)
+VectMapFunctionHomomorphism f [] [] [] = []
+VectMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
+  f.homomorphic x y hdEq :: VectMapFunctionHomomorphism f xs ys tlEq
+
+public export
+VectMapHomomorphism : (f : a ~> b) -> (VectSetoid n a ~> VectSetoid n b)
+VectMapHomomorphism f = MkSetoidHomomorphism (map f.H) (VectMapFunctionHomomorphism f)
+
+public export
+VectMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (VectSetoid n a ~~> VectSetoid n b)
+  VectMapHomomorphism
+VectMapIsHomomorphism f g f_eq_g [] = []
+VectMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: VectMapIsHomomorphism f g f_eq_g xs
+
+public export
+VectMap : {0 a, b : Setoid} -> (a ~~> b) ~> (VectSetoid n a ~~> VectSetoid n b)
+VectMap = MkSetoidHomomorphism
+  { H           = VectMapHomomorphism
+  , homomorphic = VectMapIsHomomorphism
+  }
-- 
cgit v1.2.3