Initial version

24 files changed, 921 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..0f01d85
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build/
+*.*~
\ No newline at end of file
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..a21fd50
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,32 @@
+Copyright (c) 2019 Ohad Kammar
+    School of Informatics, University of Edinburgh
+All rights reserved.
+
+This code is derived from software written by Ohad Kammar
+(ohad.kammar@ed.ac.uk).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. None of the names of the copyright holders may be used to endorse
+   or promote products derived from this software without specific
+   prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*** End of disclaimer. ***
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
index 0000000..caaf4af
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,12 @@
+all: Tutorial.md
+
+.PHONY: all ttms
+
+ttms:
+	pack build setoid-doc.ipkg
+
+%.md: .PHONY
+	pack run katla markdown sources/$*.md ./build/ttc/$*.ttm > $*.md
+
+install-deps:
+	pack install-deps setoid-doc.ipkg
diff --git a/doc/Tutorial.md b/doc/Tutorial.md
new file mode 100644
index 0000000..20678f2
--- /dev/null
+++ b/doc/Tutorial.md
@@ -0,0 +1,46 @@
+<style>
+.IdrisData {
+  color: darkred
+}
+.IdrisType {
+  color: blue
+}
+.IdrisBound {
+  color: black
+}
+.IdrisFunction {
+  color: darkgreen
+}
+.IdrisKeyword {
+  text-decoration: underline;
+}
+.IdrisComment {
+  color: #b22222
+}
+.IdrisNamespace {
+  font-style: italic;
+  color: black
+}
+.IdrisPostulate {
+  font-weight: bold;
+  color: red
+}
+.IdrisModule {
+  font-style: italic;
+  color: black
+}
+.IdrisCode {
+  display: block;
+  background-color: whitesmoke;
+}
+</style>
+# Tutorial: setoids
+A _setoid_ is a type equipped with an equivalence relation
+
+
+
+<code class="IdrisCode">
+<span class="IdrisFunction">F</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisType">Nat</span><br />
+<span class="IdrisFunction">F</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">0</span><br />
+</code>
+
diff --git a/doc/pack.toml b/doc/pack.toml
new file mode 100644
index 0000000..d555f03
--- /dev/null
+++ b/doc/pack.toml
@@ -0,0 +1,4 @@
+[doc.setoid]
+type = "local"
+path = ".."
+ipkg = "setoid.ipkg"
diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg
new file mode 100644
index 0000000..5d183fd
--- /dev/null
+++ b/doc/setoid-doc.ipkg
@@ -0,0 +1,42 @@
+package setoid-doc
+-- version =
+authors = "Ohad Kammar"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+-- depends =
+
+modules
+  = Tutorial
+
+-- name of executable
+sourcedir = "sources"
+builddir = "build"
+outputdir = "build"
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md
new file mode 100644
index 0000000..dc7dc71
--- /dev/null
+++ b/doc/sources/Tutorial.md
@@ -0,0 +1,11 @@
+# Tutorial: setoids
+A _setoid_ is a type equipped with an equivalence relation
+
+```idris hide
+module Tutorial
+```
+
+```idris
+Example1 : Nat
+Example1 = 0
+```
diff --git a/logo/README.md b/logo/README.md
new file mode 100644
index 0000000..cef2495
--- /dev/null
+++ b/logo/README.md
@@ -0,0 +1,3 @@
+Public domain image taken from:
+  http://www.publicdomainfiles.com/show_file.php?id=13925350213405
+  by Merlin2525
diff --git a/logo/abstract-dragon.png b/logo/abstract-dragon.png
new file mode 100644
index 0000000..62b7be0
--- /dev/null
+++ b/logo/abstract-dragon.png
diff --git a/logo/idris-512x512.png b/logo/idris-512x512.png
new file mode 100644
index 0000000..24b2424
--- /dev/null
+++ b/logo/idris-512x512.png
diff --git a/logo/setoid-logo.png b/logo/setoid-logo.png
new file mode 100644
index 0000000..5539cd7
--- /dev/null
+++ b/logo/setoid-logo.png
diff --git a/logo/setoid-logo.xcf b/logo/setoid-logo.xcf
new file mode 100644
index 0000000..8debc8f
--- /dev/null
+++ b/logo/setoid-logo.xcf
diff --git a/setoid.ipkg b/setoid.ipkg
new file mode 100644
index 0000000..06cdc2a
--- /dev/null
+++ b/setoid.ipkg
@@ -0,0 +1,58 @@
+package setoid
+version = 0.1.0
+authors = "Ohad Kammar"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+depends
+  = contrib
+
+-- modules to install
+modules
+  = Data.Setoid
+  , Data.Setoid.Definition
+  , Data.Setoid.Either
+  , Data.Setoid.Pair
+  , Data.Setoid.Vect
+  , Data.Setoid.Vect.Functional
+  , Data.Setoid.Vect.Inductive
+  , Data.Setoid.List
+  , Syntax.PreorderReasoning.Setoid
+  , Data.Fun.Nary
+
+-- main file (i.e. file to load at REPL)
+-- main =
+
+-- name of executable
+-- executable =
+-- opts =
+sourcedir = "src"
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =
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
+  }
diff --git a/src/Setoid.idr b/src/Setoid.idr
new file mode 100644
index 0000000..12c0a7d
--- /dev/null
+++ b/src/Setoid.idr
@@ -0,0 +1 @@
+module Setoid
diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
new file mode 100644
index 0000000..29ec715
--- /dev/null
+++ b/src/Syntax/PreorderReasoning/Setoid.idr
@@ -0,0 +1,53 @@
+||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
+module Syntax.PreorderReasoning.Setoid
+
+import Data.Setoid.Definition
+
+infixl 0  ~~
+prefix 1  |~
+infix  1  ...,..<,..>,.=.,.=<,.=>
+
+public export
+data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where
+  (...) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
+    a.equivalence.relation x y -> Step a x y
+
+public export
+data FastDerivation : (a : Setoid) -> (x, y : U a) -> Type where
+  (|~) : {0 a : Setoid} -> (x : U a) -> FastDerivation a x x
+  (~~) : {0 a : Setoid} -> {x, y : U a}
+         -> FastDerivation a x y -> {z : U a} -> (step : Step a y z)
+         -> FastDerivation a x z
+
+public export
+CalcWith : (a : Setoid) -> {0 x : U a} -> {0 y : U a} -> FastDerivation a x y ->
+  a.equivalence.relation x y
+CalcWith a (|~ x) = a.equivalence.reflexive x
+CalcWith a ((~~) der (z ... step)) = a.equivalence.transitive _ _ _
+    (CalcWith a der) step
+
+-- Smart constructors
+public export
+(..<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    a.equivalence.relation y x -> Step a x y
+(y ..<(prf)) {x} = (y ...(a.equivalence.symmetric _ _ prf))
+
+public export
+(..>) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
+    a.equivalence.relation x y -> Step a x y
+(..>) = (...)
+
+public export
+(.=.) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    x === y -> Step a x y
+(y .=.(Refl)) = (y ...(a.equivalence.reflexive y))
+
+public export
+(.=>) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    x === y -> Step a x y
+(.=>) = (.=.)
+
+public export
+(.=<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    y === x -> Step a x y
+(y .=<(Refl)) = (y ...(a.equivalence.reflexive y))