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/Fun/Nary.idr               |  51 ++++++++++
 src/Data/Setoid.idr                 |  10 ++
 src/Data/Setoid/Definition.idr      | 193 ++++++++++++++++++++++++++++++++++++
 src/Data/Setoid/Either.idr          |  58 +++++++++++
 src/Data/Setoid/List.idr            |  84 ++++++++++++++++
 src/Data/Setoid/Pair.idr            | 115 +++++++++++++++++++++
 src/Data/Setoid/Vect.idr            |   4 +
 src/Data/Setoid/Vect/Functional.idr |  64 ++++++++++++
 src/Data/Setoid/Vect/Inductive.idr  |  78 +++++++++++++++
 9 files changed, 657 insertions(+)
 create mode 100644 src/Data/Fun/Nary.idr
 create mode 100644 src/Data/Setoid.idr
 create mode 100644 src/Data/Setoid/Definition.idr
 create mode 100644 src/Data/Setoid/Either.idr
 create mode 100644 src/Data/Setoid/List.idr
 create mode 100644 src/Data/Setoid/Pair.idr
 create mode 100644 src/Data/Setoid/Vect.idr
 create mode 100644 src/Data/Setoid/Vect/Functional.idr
 create mode 100644 src/Data/Setoid/Vect/Inductive.idr

(limited to 'src/Data')

diff --git a/src/Data/Fun/Nary.idr b/src/Data/Fun/Nary.idr
new file mode 100644
index 0000000..21a684b
--- /dev/null
+++ b/src/Data/Fun/Nary.idr
@@ -0,0 +1,51 @@
+module Data.Fun.Nary
+
+import Data.Vect
+
+%default total
+
+public export
+data Visibility = Visible | Hidden | Auto
+
+public export
+Pi : Visibility -> (a : Type) -> (a -> Type) -> Type
+Pi Visible a b = (x : a) -> b x
+Pi Hidden  a b = {x : a} -> b x
+Pi Auto    a b = {auto x : a} -> b x
+
+public export
+lam : (vis : Visibility) -> (0 b : a -> Type) ->
+      ((x : a) -> b x) -> Pi vis a b
+lam Visible b f = f
+lam Hidden  b f = f _
+lam Auto    b f = f %search
+
+public export
+app : (vis : Visibility) -> (0 b : a -> Type) ->
+      Pi vis a b -> ((x : a) -> b x)
+app Visible b f x = f x
+app Hidden  b f x = f
+app Auto    b f x = f
+
+public export
+PI : (n : Nat) -> Visibility -> (a : Type) -> (Vect n a -> Type) -> Type
+PI Z     vis a b = b []
+PI (S n) vis a b = Pi vis a (\ x => PI n vis a (b . (x ::)))
+
+public export
+curry : (n : Nat) -> (vis : Visibility) ->
+        (0 b : Vect n a -> Type) ->
+        ((as : Vect n a) -> b as) ->
+        PI n vis a b
+curry 0 vis b f = f []
+curry (S n) vis b f
+  = lam vis _ $ \ x => curry n vis (b . (x ::)) (\ xs => f (x :: xs))
+
+public export
+uncurry : (n : Nat) -> (vis : Visibility) ->
+          (0 b : Vect n a -> Type) ->
+          PI n vis a b ->
+          (as : Vect n a) -> b as
+uncurry 0 vis b f [] = f
+uncurry (S n) vis b f (x :: xs)
+  = uncurry n vis (b . (x ::)) (app vis _ f x) xs
diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr
new file mode 100644
index 0000000..536e3e6
--- /dev/null
+++ b/src/Data/Setoid.idr
@@ -0,0 +1,10 @@
+||| A setoid is a type equipped with an equivalence relation
+module Data.Setoid
+
+import public Data.Setoid.Definition
+import public Data.Setoid.Either
+import public Data.Setoid.Pair
+import public Data.Setoid.Vect
+import public Data.Setoid.List
+
+import public Syntax.PreorderReasoning.Setoid
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
+  }
-- 
cgit v1.2.3