summaryrefslogtreecommitdiff
path: root/src/Data/Setoid
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Setoid')
-rw-r--r--src/Data/Setoid/Definition.idr193
-rw-r--r--src/Data/Setoid/Either.idr58
-rw-r--r--src/Data/Setoid/List.idr84
-rw-r--r--src/Data/Setoid/Pair.idr115
-rw-r--r--src/Data/Setoid/Vect.idr4
-rw-r--r--src/Data/Setoid/Vect/Functional.idr64
-rw-r--r--src/Data/Setoid/Vect/Inductive.idr78
7 files changed, 596 insertions, 0 deletions
diff --git a/src/Data/Setoid/Definition.idr b/src/Data/Setoid/Definition.idr
new file mode 100644
index 0000000..c6bd647
--- /dev/null
+++ b/src/Data/Setoid/Definition.idr
@@ -0,0 +1,193 @@
+||| Basic definition and notation for setoids
+module Data.Setoid.Definition
+
+import public Control.Relation
+import public Control.Order
+
+import Data.Vect
+import public Data.Fun.Nary
+
+infix 5 ~>, ~~>, <~>
+
+%default total
+
+public export
+record Equivalence (A : Type) where
+ constructor MkEquivalence
+ 0 relation: Rel A
+ reflexive : (x : A) -> relation x x
+ symmetric : (x, y : A) -> relation x y -> relation y x
+ transitive: (x, y, z : A) -> relation x y -> relation y z
+ -> relation x z
+
+public export
+EqualEquivalence : (0 a : Type) -> Equivalence a
+EqualEquivalence a = MkEquivalence
+ { relation = (===)
+ , reflexive = \_ => Refl
+ , symmetric = \_,_, Refl => Refl
+ , transitive = \_,_,_,Refl,Refl => Refl
+ }
+
+public export
+record Setoid where
+ constructor MkSetoid
+ 0 U : Type
+ equivalence : Equivalence U
+
+public export
+record PreorderData A (rel : Rel A) where
+ constructor MkPreorderData
+ reflexive : (x : A) -> rel x x
+ transitive : (x,y,z : A) -> rel x y -> rel y z -> rel x z
+
+public export
+[PreorderWorkaround] (Reflexive ty rel, Transitive ty rel) => Preorder ty rel where
+
+public export
+MkPreorderWorkaround : {preorderData : PreorderData ty rel} -> Order.Preorder ty rel
+MkPreorderWorkaround {preorderData} =
+ let reflexiveArg = MkReflexive {ty, rel} $
+ lam Hidden (\y => rel y y) preorderData.reflexive
+ transitiveArg = MkTransitive {ty} {rel} $
+ Nary.curry 3 Hidden
+ (\[x,y,z] =>
+ x `rel` y ->
+ y `rel` z ->
+ x `rel` z)
+ (\[x,y,z] => preorderData.transitive _ _ _)
+
+ in PreorderWorkaround
+public export
+reflect : (a : Setoid) -> {x, y : U a} -> x = y -> a.equivalence.relation x y
+reflect a Refl = a.equivalence.reflexive _
+
+public export
+MkPreorder : {0 a : Type} -> {0 rel : Rel a}
+ -> (reflexive : (x : a) -> rel x x)
+ -> (transitive : (x,y,z : a) -> rel x y -> rel y z -> rel x z)
+ -> Preorder a rel
+MkPreorder reflexive transitive = MkPreorderWorkaround {preorderData = MkPreorderData reflexive transitive}
+
+public export
+cast : (a : Setoid) -> Preorder (U a) (a.equivalence.relation)
+cast a = MkPreorder a.equivalence.reflexive a.equivalence.transitive
+
+namespace ToSetoid
+ public export
+ irrelevantCast : (0 a : Type) -> Setoid
+ irrelevantCast a = MkSetoid a (EqualEquivalence a)
+
+public export
+Cast Type Setoid where
+ cast a = irrelevantCast a
+
+public export 0
+SetoidHomomorphism : (a,b : Setoid)
+ -> (f : U a -> U b) -> Type
+SetoidHomomorphism a b f
+ = (x,y : U a) -> a.equivalence.relation x y
+ -> b.equivalence.relation (f x) (f y)
+
+public export
+record (~>) (A,B : Setoid) where
+ constructor MkSetoidHomomorphism
+ H : U A -> U B
+ homomorphic : SetoidHomomorphism A B H
+
+public export
+mate : {b : Setoid} -> (a -> U b) -> (irrelevantCast a ~> b)
+mate f = MkSetoidHomomorphism f $ \x,y, prf => reflect b (cong f prf)
+
+||| Identity Setoid homomorphism
+public export
+id : (a : Setoid) -> a ~> a
+id a = MkSetoidHomomorphism Prelude.id $ \x, y, prf => prf
+
+||| Composition of Setoid homomorphisms
+public export
+(.) : {a,b,c : Setoid} -> b ~> c -> a ~> b -> a ~> c
+g . f = MkSetoidHomomorphism (H g . H f) $ \x,y,prf => g.homomorphic _ _ (f.homomorphic _ _ prf)
+
+public export
+(~~>) : (a,b : Setoid) -> Setoid
+(~~>) a b = MkSetoid (a ~> b) $
+ let 0 relation : (f, g : a ~> b) -> Type
+ relation f g = (x : U a) ->
+ b.equivalence.relation (f.H x) (g.H x)
+ in MkEquivalence
+ { relation
+ , reflexive = \f,v =>
+ b.equivalence.reflexive (f.H v)
+ , symmetric = \f,g,prf,w =>
+ b.equivalence.symmetric _ _ (prf w)
+ , transitive = \f,g,h,f_eq_g, g_eq_h, q =>
+ b.equivalence.transitive _ _ _
+ (f_eq_g q) (g_eq_h q)
+ }
+
+public export
+post : {a,b,c : Setoid} -> b ~> c -> (a ~~> b) ~> (a ~~> c)
+post h = MkSetoidHomomorphism
+ { H = (h .)
+ , homomorphic = \f1,f2,prf,x => h.homomorphic _ _ (prf x)
+ }
+
+||| Two setoid homomorphism are each other's inverses
+public export
+record Isomorphism {a, b : Setoid} (Fwd : a ~> b) (Bwd : b ~> a) where
+ constructor IsIsomorphism
+ BwdFwdId : (a ~~> a).equivalence.relation (Bwd . Fwd) (id a)
+ FwdBwdId : (b ~~> b).equivalence.relation (Fwd . Bwd) (id b)
+
+||| Setoid isomorphism
+public export
+record (<~>) (a, b : Setoid) where
+ constructor MkIsomorphism
+ Fwd : a ~> b
+ Bwd : b ~> a
+
+ Iso : Isomorphism Fwd Bwd
+
+||| Identity (isomorphism _)
+public export
+refl : {a : Setoid} -> a <~> a
+refl = MkIsomorphism (id a) (id a) (IsIsomorphism a.equivalence.reflexive a.equivalence.reflexive)
+
+||| Reverse an isomorphism
+public export
+sym : a <~> b -> b <~> a
+sym iso = MkIsomorphism iso.Bwd iso.Fwd (IsIsomorphism iso.Iso.FwdBwdId iso.Iso.BwdFwdId)
+
+||| Compose isomorphisms
+public export
+trans : {a,b,c : Setoid} -> (a <~> b) -> (b <~> c) -> (a <~> c)
+trans ab bc = MkIsomorphism (bc.Fwd . ab.Fwd) (ab.Bwd . bc.Bwd) (IsIsomorphism i1 i2)
+ where i1 : (x : U a) -> a.equivalence.relation (ab.Bwd.H (bc.Bwd.H (bc.Fwd.H (ab.Fwd.H x)))) x
+ i1 x = a.equivalence.transitive _ _ _ (ab.Bwd.homomorphic _ _ (bc.Iso.BwdFwdId _)) (ab.Iso.BwdFwdId x)
+
+ i2 : (x : U c) -> c.equivalence.relation (bc.Fwd.H (ab.Fwd.H (ab.Bwd.H (bc.Bwd.H x)))) x
+ i2 x = c.equivalence.transitive _ _ _ (bc.Fwd.homomorphic _ _ (ab.Iso.FwdBwdId _)) (bc.Iso.FwdBwdId x)
+
+public export
+IsoEquivalence : Equivalence Setoid
+IsoEquivalence = MkEquivalence (<~>) (\_ => refl) (\_,_ => sym) (\_,_,_ => trans)
+
+
+||| Quotient a type by an function into a setoid
+|||
+||| Instance of the more general coequaliser of two setoid morphisms.
+public export
+Quotient : (b : Setoid) -> (a -> U b) -> Setoid
+Quotient b q = MkSetoid a $
+ let 0 relation : a -> a -> Type
+ relation x y = b.equivalence.relation (q x) (q y)
+ in MkEquivalence
+ { relation = relation
+ , reflexive = \x =>
+ b.equivalence.reflexive (q x)
+ , symmetric = \x,y =>
+ b.equivalence.symmetric (q x) (q y)
+ , transitive = \x,y,z =>
+ b.equivalence.transitive (q x) (q y) (q z)
+ }
diff --git a/src/Data/Setoid/Either.idr b/src/Data/Setoid/Either.idr
new file mode 100644
index 0000000..27cf661
--- /dev/null
+++ b/src/Data/Setoid/Either.idr
@@ -0,0 +1,58 @@
+||| Coproduct of setoids
+module Data.Setoid.Either
+
+import Data.Setoid.Definition
+
+%default total
+
+namespace Relation
+ ||| Binary relation disjunction
+ public export
+ data Or : (p : Rel a) -> (q : Rel b) -> Rel (Either a b) where
+ Left : {0 q : Rel b} -> p x y -> (p `Or` q) (Left x) (Left y)
+ Right : {0 p : Rel a} -> q x y -> (p `Or` q) (Right x) (Right y)
+
+||| Coproduct of setoids
+public export
+Either : (a,b : Setoid) -> Setoid
+Either a b = MkSetoid
+ { U = U a `Either` U b
+ , equivalence = MkEquivalence
+ { relation = a.equivalence.relation `Or` b.equivalence.relation
+ , reflexive = \case
+ Left x => Left $ a.equivalence.reflexive x
+ Right y => Right $ b.equivalence.reflexive y
+ , symmetric = \x,y => \case
+ Left prf => Left $ a.equivalence.symmetric _ _ prf
+ Right prf => Right $ b.equivalence.symmetric _ _ prf
+ , transitive = \x,y,z => \case
+ Left prf1 => \case {Left prf2 => Left $ a.equivalence.transitive _ _ _ prf1 prf2}
+ Right prf1 => \case {Right prf2 => Right $ b.equivalence.transitive _ _ _ prf1 prf2}
+ }
+ }
+
+||| Setoid homomorphism smart constructor
+public export
+Left : {0 a, b: Setoid} -> a ~> (a `Either` b)
+Left = MkSetoidHomomorphism
+ { H = Left
+ , homomorphic = \x,y,prf => Left prf
+ }
+
+||| Setoid homomorphism smart constructor
+public export
+Right : {0 a, b: Setoid} -> b ~> (a `Either` b)
+Right = MkSetoidHomomorphism
+ { H = Right
+ , homomorphic = \x,y,prf => Right prf
+ }
+
+||| Setoid homomorphism deconstructor
+public export
+either : {0 a, b, c : Setoid} -> (a ~> c) -> (b ~> c) -> (a `Either` b) ~> c
+either lft rgt = MkSetoidHomomorphism
+ { H = either lft.H rgt.H
+ , homomorphic = \x,y => \case
+ Left prf => lft.homomorphic _ _ prf
+ Right prf => rgt.homomorphic _ _ prf
+ }
diff --git a/src/Data/Setoid/List.idr b/src/Data/Setoid/List.idr
new file mode 100644
index 0000000..76a79cd
--- /dev/null
+++ b/src/Data/Setoid/List.idr
@@ -0,0 +1,84 @@
+||| Setoid of lists over a setoid and associated definitions
+module Data.Setoid.List
+
+import Data.List
+import Data.Setoid.Definition
+
+%default total
+
+namespace Relation
+ public export
+ data (.ListEquality) : (a : Setoid) -> Rel (List $ U a) where
+ Nil : a.ListEquality [] []
+ (::) : (hdEq : a.equivalence.relation x y) -> (tlEq : a.ListEquality xs ys) ->
+ a.ListEquality (x :: xs) (y :: ys)
+
+public export
+(.ListEqualityReflexive) : (a : Setoid) -> (xs : List $ U a) -> a.ListEquality xs xs
+a.ListEqualityReflexive [] = []
+a.ListEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.ListEqualityReflexive xs
+
+public export
+(.ListEqualitySymmetric) : (a : Setoid) -> (xs,ys : List $ U a) -> (prf : a.ListEquality xs ys) ->
+ a.ListEquality ys xs
+a.ListEqualitySymmetric [] [] [] = []
+a.ListEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
+ = a.equivalence.symmetric x y hdEq :: a.ListEqualitySymmetric xs ys tlEq
+
+public export
+(.ListEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : List $ U a) ->
+ (prf1 : a.ListEquality xs ys) -> (prf2 : a.ListEquality ys zs) ->
+ a.ListEquality xs zs
+a.ListEqualityTransitive [] [] [] [] [] = []
+a.ListEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
+ = a.equivalence.transitive x y z hdEq1 hdEq2 ::
+ a.ListEqualityTransitive xs ys zs tlEq1 tlEq2
+
+public export
+ListSetoid : (a : Setoid) -> Setoid
+ListSetoid a = MkSetoid (List $ U a)
+ $ MkEquivalence
+ { relation = a.ListEquality
+ , reflexive = a.ListEqualityReflexive
+ , symmetric = a.ListEqualitySymmetric
+ , transitive = a.ListEqualityTransitive
+ }
+
+public export
+ListMapFunctionHomomorphism : (f : a ~> b) ->
+ SetoidHomomorphism (ListSetoid a) (ListSetoid b) (map f.H)
+ListMapFunctionHomomorphism f [] [] [] = []
+ListMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
+ f.homomorphic x y hdEq :: ListMapFunctionHomomorphism f xs ys tlEq
+
+public export
+ListMapHomomorphism : (f : a ~> b) -> (ListSetoid a ~> ListSetoid b)
+ListMapHomomorphism f = MkSetoidHomomorphism (map f.H) (ListMapFunctionHomomorphism f)
+
+public export
+ListMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (ListSetoid a ~~> ListSetoid b)
+ ListMapHomomorphism
+ListMapIsHomomorphism f g f_eq_g [] = []
+ListMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: ListMapIsHomomorphism f g f_eq_g xs
+
+public export
+ListMap : {0 a, b : Setoid} -> (a ~~> b) ~> (ListSetoid a ~~> ListSetoid b)
+ListMap = MkSetoidHomomorphism
+ { H = ListMapHomomorphism
+ , homomorphic = ListMapIsHomomorphism
+ }
+
+public export
+reverseHomomorphic : {a : Setoid} -> (x, y : List (U a)) ->
+ (a.ListEquality x y) -> a.ListEquality (reverse x) (reverse y)
+reverseHomomorphic x y prf = roh [] [] x y (a.ListEqualityReflexive _) prf
+ where roh : (ws, xs, ys, zs : List (U a)) -> a.ListEquality ws xs -> a.ListEquality ys zs ->
+ a.ListEquality (reverseOnto ws ys) (reverseOnto xs zs)
+ roh ws xs [] [] wx [] = wx
+ roh ws xs (y::ys) (z::zs) wx (yzh :: yzt) = roh (y::ws) (z::xs) ys zs (yzh :: wx) yzt
+
+public export
+appendCongruence : {a : Setoid} -> (x1, x2, y1, y2 : List (U a)) ->
+ a.ListEquality x1 y1 -> a.ListEquality x2 y2 -> a.ListEquality (x1 ++ x2) (y1 ++ y2)
+appendCongruence [] x2 [] y2 [] p = p
+appendCongruence (x::xs) x2 (y::ys) y2 (ph::pt) p = ph :: appendCongruence _ _ _ _ pt p
diff --git a/src/Data/Setoid/Pair.idr b/src/Data/Setoid/Pair.idr
new file mode 100644
index 0000000..2cb9357
--- /dev/null
+++ b/src/Data/Setoid/Pair.idr
@@ -0,0 +1,115 @@
+||| Product of setoids
+module Data.Setoid.Pair
+
+import Data.Setoid.Definition
+import Data.Setoid.Either
+
+%default total
+
+||| Binary relation conjunction
+public export
+record And {A,B : Type} (p : Rel A) (q : Rel B) (xy1, xy2 : (A, B)) where
+ constructor MkAnd
+ fst : p (fst xy1) (fst xy2)
+ snd : q (snd xy1) (snd xy2)
+
+||| Product of setoids
+public export
+Pair : (a,b : Setoid) -> Setoid
+Pair a b = MkSetoid
+ { U = (U a, U b)
+ , equivalence = MkEquivalence
+ { relation = a.equivalence.relation `And` b.equivalence.relation
+ , reflexive = \xy => MkAnd
+ (a.equivalence.reflexive $ fst xy)
+ (b.equivalence.reflexive $ snd xy)
+ , symmetric = \xy1,xy2,prf => MkAnd
+ (a.equivalence.symmetric (fst xy1) (fst xy2) prf.fst)
+ (b.equivalence.symmetric (snd xy1) (snd xy2) prf.snd)
+ , transitive = \xy1,xy2,xy3,prf1,prf2 => MkAnd
+ (a.equivalence.transitive (fst xy1) (fst xy2) (fst xy3) prf1.fst prf2.fst)
+ (b.equivalence.transitive (snd xy1) (snd xy2) (snd xy3) prf1.snd prf2.snd)
+ }
+ }
+
+||| Left projection setoid homomorphism
+public export
+(.fst) : {0 a,b : Setoid} -> Pair a b ~> a
+(.fst) = MkSetoidHomomorphism
+ { H = Builtin.fst
+ , homomorphic = \xy1,xy2,prf => prf.fst
+ }
+
+||| Right projection setoid homomorphism
+public export
+(.snd) : {0 a,b : Setoid} -> Pair a b ~> b
+(.snd) = MkSetoidHomomorphism
+ { H = Builtin.snd
+ , homomorphic = \xy1,xy2,prf => prf.snd
+ }
+
+||| Setoid homomorphism constructor
+public export
+tuple : {0 a,b,c : Setoid} -> c ~> a -> c ~> b -> c ~> Pair a b
+tuple f g = MkSetoidHomomorphism
+ { H = \z => (f.H z, g.H z)
+ , homomorphic = \z1,z2,prf => MkAnd
+ (f.homomorphic z1 z2 prf)
+ (g.homomorphic z1 z2 prf)
+ }
+
+||| Unique value of type unit
+public export
+unitVal : (x,y : Unit) -> x = y
+unitVal () () = Refl
+
+||| The unique setoid map into the terminal type
+public export
+unit : {a : Setoid} -> a ~> cast Unit
+unit = MkSetoidHomomorphism
+ { H = const ()
+ , homomorphic = \_,_,_ => unitVal () ()
+ }
+
+||| The constant function as a setoid morphism
+public export
+const : {a,b : Setoid} -> (x : U b) -> a ~> b
+const x = mate (Prelude.const x) . unit
+
+||| Setoid homomorphism constructor
+public export
+bimap : {a,b,c,d : Setoid} -> c ~> a -> d ~> b -> Pair c d ~> Pair a b
+bimap f g = tuple (f . (.fst)) (g . (.snd))
+
+-- Distribution of products over sums, degenerate case:
+
+||| Function underlying the bijection 2 x s <~> s + s
+public export
+distributeFunction : {s : Setoid} -> (Bool, U s) -> (U s `Either` U s)
+distributeFunction (False, x) = Left x
+distributeFunction (True , x) = Right x
+
+||| States: the function underlying the bijection 2 x s <~> s + s is a setoid homomorphism
+public export
+distributeHomomorphism : {s : Setoid} ->
+ SetoidHomomorphism ((cast Bool) `Pair` s) (s `Either` s)
+ (distributeFunction {s})
+distributeHomomorphism (b1,x1) (b2,x2) prf =
+ case prf.fst of
+ Refl => case b2 of
+ False => Left prf.snd
+ True => Right prf.snd
+
+||| Setoid homomorphism involved in the bijection 2 x s <~> s + s
+public export
+distribute : {s : Setoid} -> ((cast Bool) `Pair` s) ~> (s `Either` s)
+distribute = MkSetoidHomomorphism
+ { H = distributeFunction
+ , homomorphic = distributeHomomorphism
+ }
+
+public export
+pairIso : {a,b,c,d : Setoid} -> (a <~> c) -> (b <~> d) -> (Pair a b <~> Pair c d)
+pairIso ac bd = MkIsomorphism (bimap ac.Fwd bd.Fwd) (bimap ac.Bwd bd.Bwd)
+ (IsIsomorphism (\(x,y) => MkAnd (ac.Iso.BwdFwdId x) (bd.Iso.BwdFwdId y))
+ (\(x,y) => MkAnd (ac.Iso.FwdBwdId x) (bd.Iso.FwdBwdId y)))
diff --git a/src/Data/Setoid/Vect.idr b/src/Data/Setoid/Vect.idr
new file mode 100644
index 0000000..7416f8a
--- /dev/null
+++ b/src/Data/Setoid/Vect.idr
@@ -0,0 +1,4 @@
+||| The setoid of vectors over a given setoid
+module Data.Setoid.Vect
+
+import public Data.Setoid.Vect.Functional
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 _ _ _)
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
+ }
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 18:09:06 +0000