From 1e64c562ad58d0fb264a11f11bc32b9311e728c4 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 6 Dec 2022 13:33:06 +0000
Subject: refactor: rename Soat.Data -> Data.

---
 soat.ipkg                             |   4 +-
 src/Data/List/Sublist.idr             |  76 ++++++++++++
 src/Data/Product.idr                  | 227 ++++++++++++++++++++++++++++++++++
 src/Soat/Data/Product.idr             | 227 ----------------------------------
 src/Soat/Data/Sublist.idr             |  76 ------------
 src/Soat/FirstOrder/Algebra.idr       |   3 +-
 src/Soat/FirstOrder/Term.idr          |   2 +-
 src/Soat/SecondOrder/Algebra.idr      |   6 +-
 src/Soat/SecondOrder/Algebra/Lift.idr |   4 +-
 9 files changed, 313 insertions(+), 312 deletions(-)
 create mode 100644 src/Data/List/Sublist.idr
 create mode 100644 src/Data/Product.idr
 delete mode 100644 src/Soat/Data/Product.idr
 delete mode 100644 src/Soat/Data/Sublist.idr

diff --git a/soat.ipkg b/soat.ipkg
index e5b4f05..ed3a86d 100644
--- a/soat.ipkg
+++ b/soat.ipkg
@@ -4,8 +4,8 @@ sourcedir = "src"
 
 depends = setoid
 
-modules = Soat.Data.Product
-        , Soat.Data.Sublist
+modules = Data.List.Sublist
+        , Data.Product
         , Soat.FirstOrder.Algebra
         , Soat.FirstOrder.Algebra.Coproduct
         , Soat.FirstOrder.Signature
diff --git a/src/Data/List/Sublist.idr b/src/Data/List/Sublist.idr
new file mode 100644
index 0000000..4e4301a
--- /dev/null
+++ b/src/Data/List/Sublist.idr
@@ -0,0 +1,76 @@
+module Data.List.Sublist
+
+import public Control.Relation
+import Data.List.Elem
+import Data.Product
+
+%default total
+
+infix 5 ++
+
+public export
+data Sublist : Rel (List a) where
+  Nil  : Sublist [] ys
+  (::) : (mem : Elem x ys) -> (mems : Sublist xs ys) -> Sublist (x :: xs) ys
+
+public export
+curry : xs `Sublist` ys -> forall x . Elem x xs -> Elem x ys
+curry (mem :: mems) Here      = mem
+curry (mem :: mems) (There y) = curry mems y
+
+public export
+uncurry : {xs : List a} -> (forall x . Elem x xs -> Elem x ys) -> xs `Sublist` ys
+uncurry {xs = []}        f = []
+uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There)
+
+public export
+uncurryCurry : (f : xs `Sublist` ys) -> uncurry (curry f) = f
+uncurryCurry []            = Refl
+uncurryCurry (mem :: mems) = cong ((::) mem) (uncurryCurry mems)
+
+public export
+curryUncurry : (0 f : forall x . Elem x xs -> Elem x ys) -> (i : Elem x xs)
+  -> curry (uncurry f) i = f i
+curryUncurry f Here         = Refl
+curryUncurry f (There elem) = curryUncurry (f . There) elem
+
+public export
+Reflexive (List a) Sublist where
+  reflexive = uncurry id
+
+public export
+Transitive (List a) Sublist where
+  transitive f g = uncurry (curry g . curry f)
+
+public export
+elemJoinL : Elem x xs -> Elem x (xs ++ ys)
+elemJoinL Here         = Here
+elemJoinL (There elem) = There (elemJoinL elem)
+
+public export
+elemJoinR : (xs : List a) -> Elem x ys -> Elem x (xs ++ ys)
+elemJoinR []        elem = elem
+elemJoinR (x :: xs) elem = There (elemJoinR xs elem)
+
+public export
+elemSplit : (xs : List a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys)
+elemSplit []        elem         = Right elem
+elemSplit (x :: xs) Here         = Left Here
+elemSplit (x :: xs) (There elem) = bimap There id (elemSplit xs elem)
+
+public export
+(++) : {xs, ys, us : List a}
+  -> xs `Sublist` ys -> us `Sublist` vs -> (xs ++ us) `Sublist` (ys ++ vs)
+(++) mems mems' = uncurry
+  (either (elemJoinL . curry mems) (elemJoinR ys . curry mems') . elemSplit xs)
+
+public export
+shuffle : is `Sublist` js -> x ^ js -> x ^ is
+shuffle []            xs = []
+shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs
+
+public export
+indexShuffle : (f : is `Sublist` js) -> {0 xs : x ^ js} -> (elem : Elem i is)
+  -> index (shuffle f xs) elem = index xs (curry f elem)
+indexShuffle (mem :: mems) Here         = Refl
+indexShuffle (mem :: mems) (There elem) = indexShuffle mems elem
diff --git a/src/Data/Product.idr b/src/Data/Product.idr
new file mode 100644
index 0000000..348fa44
--- /dev/null
+++ b/src/Data/Product.idr
@@ -0,0 +1,227 @@
+module Data.Product
+
+import Data.List.Elem
+import Data.Setoid.Indexed
+
+%default total
+
+infix 10 ^
+infix 5 ++
+
+-- Definitions
+
+public export
+data (^) : (0 _ : a -> Type) -> List a -> Type where
+  Nil  : x ^ []
+  (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is)
+
+public export
+ary : List Type -> Type -> Type
+ary []        y = y
+ary (x :: xs) y = x -> ary xs y
+
+-- Conversions
+
+public export
+uncurry : map x is `ary` a -> x ^ is -> a
+uncurry f []        = f
+uncurry f (x :: xs) = uncurry (f x) xs
+
+-- Destructors
+
+public export
+head : x ^ (i :: is) -> x i
+head (x :: xs) = x
+
+public export
+tail : x ^ (i :: is) -> x ^ is
+tail (x :: xs) = xs
+
+public export
+consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
+consHeadTail (x :: xs) = Refl
+
+public export
+index : x ^ is -> Elem i is -> x i
+index xs Here         = head xs
+index xs (There elem) = index (tail xs) elem
+
+-- Constructors
+
+public export
+tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
+tabulate {is = []}        f = []
+tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)
+
+public export
+indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is)
+  -> index (tabulate f) elem = f elem
+indexTabulate f Here         = Refl
+indexTabulate f (There elem) = indexTabulate (f . There) elem
+
+-- Operations
+
+public export
+map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
+map f []        = []
+map f (x :: xs) = f _ x :: map f xs
+
+public export
+indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is)
+  -> index (map f xs) elem = f i (index xs elem)
+indexMap (x :: xs) Here         = Refl
+indexMap (x :: xs) (There elem) = indexMap xs elem
+
+public export
+mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
+mapId []        = Refl
+mapId (x :: xs) = cong ((::) x) $ mapId xs
+
+public export
+mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i}
+  -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs)
+mapComp []        = Refl
+mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs
+
+public export
+(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
+(++) []        ys = ys
+(++) (x :: xs) ys = x :: (xs ++ ys)
+
+public export
+wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
+wrap f []        = []
+wrap f (x :: xs) = x :: wrap f xs
+
+public export
+mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
+  -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
+mapWrap g []        = Refl
+mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs
+
+public export
+unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
+unwrap f {is = []}        []        = []
+unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
+
+public export
+mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b)
+  -> {is : _} -> (xs : x ^ map g is)
+  -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
+mapUnwrap g {is = []}        []        = Refl
+mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs
+
+public export
+unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
+unwrapWrap u []        = Refl
+unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs
+
+public export
+wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
+wrapUnwrap {is = []}        []        = Refl
+wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs
+
+-- Relations
+
+namespace Pointwise
+  public export
+  data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
+    Nil  : Pointwise rel [] []
+    (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
+      -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)
+
+  -- Destructors
+
+  public export
+  index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
+  index (r :: rs) Here         = r
+  index (r :: rs) (There elem) = index rs elem
+
+  -- Operators
+
+  public export
+  map : forall b . {0 r, s : (i : a) -> Rel (b i)}
+    -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
+    -> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys
+  map f []        = []
+  map f (r :: rs) = f _ r :: map f rs
+
+  -- Relational Properties
+
+  pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
+  pwEqImpliesEqual []        = Refl
+  pwEqImpliesEqual (r :: rs) = trans
+    (sym $ consHeadTail _)
+    (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
+
+  equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys
+  equalImpliesPwEq {xs = []}        {ys = []}        eq = []
+  equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq =
+    cong head eq :: equalImpliesPwEq (cong tail eq)
+
+  pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> (u : x i) -> rel i u u)
+    -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs
+  pwRefl refl []        = []
+  pwRefl refl (x :: xs) = refl _ x :: pwRefl refl xs
+
+  pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> (u, v : x i) -> rel i u v -> rel i v u)
+    -> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
+  pwSym sym []        = []
+  pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs
+
+  pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> (u, v, w : x i) -> rel i u v -> rel i v w -> rel i u w)
+    -> {is : List a} -> {xs, ys, zs : x ^ is}
+    -> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
+  pwTrans trans []        []        = []
+  pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss
+
+  public export
+  pwEquivalence : IndexedEquivalence a x -> IndexedEquivalence (List a) ((^) x)
+  pwEquivalence eq = MkIndexedEquivalence
+    { relation   = \_ => Pointwise eq.relation
+    , reflexive  = \_ => pwRefl eq.reflexive
+    , symmetric  = \_, _, _ => pwSym eq.symmetric
+    , transitive = \_, _, _, _ => pwTrans eq.transitive
+    }
+
+  public export
+  pwSetoid : IndexedSetoid a -> IndexedSetoid (List a)
+  pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
+
+  -- Introductors and Eliminators
+
+  public export
+  mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
+    -> {0 f, g : (i : a) -> x i -> y i}
+    -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
+    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
+  mapIntro'' cong []        = []
+  mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs
+
+  public export
+  mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
+    -> {0 f, g : (i : a) -> x i -> y i}
+    -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
+    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
+  mapIntro' cong = mapIntro'' (\t, _, _ => cong t)
+
+  public export
+  mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is}
+    -> Pointwise x.equivalence.relation xs ys
+    -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys)
+  mapIntro f = mapIntro' f.homomorphic
+
+  public export
+  wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is}
+    -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
+  wrapIntro []        = []
+  wrapIntro (r :: rs) = r :: wrapIntro rs
+
+  public export
+  unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {0 xs, ys : x ^ map f is}
+    -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
+  unwrapIntro {is = []}        []        = []
+  unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
deleted file mode 100644
index 1532d4b..0000000
--- a/src/Soat/Data/Product.idr
+++ /dev/null
@@ -1,227 +0,0 @@
-module Soat.Data.Product
-
-import Data.List.Elem
-import Data.Setoid.Indexed
-
-%default total
-
-infix 10 ^
-infix 5 ++
-
--- Definitions
-
-public export
-data (^) : (0 _ : a -> Type) -> List a -> Type where
-  Nil  : x ^ []
-  (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is)
-
-public export
-ary : List Type -> Type -> Type
-ary []        y = y
-ary (x :: xs) y = x -> ary xs y
-
--- Conversions
-
-public export
-uncurry : map x is `ary` a -> x ^ is -> a
-uncurry f []        = f
-uncurry f (x :: xs) = uncurry (f x) xs
-
--- Destructors
-
-public export
-head : x ^ (i :: is) -> x i
-head (x :: xs) = x
-
-public export
-tail : x ^ (i :: is) -> x ^ is
-tail (x :: xs) = xs
-
-public export
-consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
-consHeadTail (x :: xs) = Refl
-
-public export
-index : x ^ is -> Elem i is -> x i
-index xs Here         = head xs
-index xs (There elem) = index (tail xs) elem
-
--- Constructors
-
-public export
-tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
-tabulate {is = []}        f = []
-tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)
-
-public export
-indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is)
-  -> index (tabulate f) elem = f elem
-indexTabulate f Here         = Refl
-indexTabulate f (There elem) = indexTabulate (f . There) elem
-
--- Operations
-
-public export
-map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
-map f []        = []
-map f (x :: xs) = f _ x :: map f xs
-
-public export
-indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is)
-  -> index (map f xs) elem = f i (index xs elem)
-indexMap (x :: xs) Here         = Refl
-indexMap (x :: xs) (There elem) = indexMap xs elem
-
-public export
-mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
-mapId []        = Refl
-mapId (x :: xs) = cong ((::) x) $ mapId xs
-
-public export
-mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i}
-  -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs)
-mapComp []        = Refl
-mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs
-
-public export
-(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
-(++) []        ys = ys
-(++) (x :: xs) ys = x :: (xs ++ ys)
-
-public export
-wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
-wrap f []        = []
-wrap f (x :: xs) = x :: wrap f xs
-
-public export
-mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
-  -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs)
-mapWrap g []        = Refl
-mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs
-
-public export
-unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
-unwrap f {is = []}        []        = []
-unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
-
-public export
-mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b)
-  -> {is : _} -> (xs : x ^ map g is)
-  -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs)
-mapUnwrap g {is = []}        []        = Refl
-mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs
-
-public export
-unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
-unwrapWrap u []        = Refl
-unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs
-
-public export
-wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
-wrapUnwrap {is = []}        []        = Refl
-wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs
-
--- Relations
-
-namespace Pointwise
-  public export
-  data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
-    Nil  : Pointwise rel [] []
-    (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
-      -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)
-
-  -- Destructors
-
-  public export
-  index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
-  index (r :: rs) Here         = r
-  index (r :: rs) (There elem) = index rs elem
-
-  -- Operators
-
-  public export
-  map : forall b . {0 r, s : (i : a) -> Rel (b i)}
-    -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
-    -> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys
-  map f []        = []
-  map f (r :: rs) = f _ r :: map f rs
-
-  -- Relational Properties
-
-  pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
-  pwEqImpliesEqual []        = Refl
-  pwEqImpliesEqual (r :: rs) = trans
-    (sym $ consHeadTail _)
-    (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
-
-  equalImpliesPwEq : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys
-  equalImpliesPwEq {xs = []}        {ys = []}        eq = []
-  equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} eq =
-    cong head eq :: equalImpliesPwEq (cong tail eq)
-
-  pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> (u : x i) -> rel i u u)
-    -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs
-  pwRefl refl []        = []
-  pwRefl refl (x :: xs) = refl _ x :: pwRefl refl xs
-
-  pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> (u, v : x i) -> rel i u v -> rel i v u)
-    -> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
-  pwSym sym []        = []
-  pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs
-
-  pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> (u, v, w : x i) -> rel i u v -> rel i v w -> rel i u w)
-    -> {is : List a} -> {xs, ys, zs : x ^ is}
-    -> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
-  pwTrans trans []        []        = []
-  pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss
-
-  public export
-  pwEquivalence : IndexedEquivalence a x -> IndexedEquivalence (List a) ((^) x)
-  pwEquivalence eq = MkIndexedEquivalence
-    { relation   = \_ => Pointwise eq.relation
-    , reflexive  = \_ => pwRefl eq.reflexive
-    , symmetric  = \_, _, _ => pwSym eq.symmetric
-    , transitive = \_, _, _, _ => pwTrans eq.transitive
-    }
-
-  public export
-  pwSetoid : IndexedSetoid a -> IndexedSetoid (List a)
-  pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
-
-  -- Introductors and Eliminators
-
-  public export
-  mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
-    -> {0 f, g : (i : a) -> x i -> y i}
-    -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
-    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
-  mapIntro'' cong []        = []
-  mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs
-
-  public export
-  mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)}
-    -> {0 f, g : (i : a) -> x i -> y i}
-    -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
-    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
-  mapIntro' cong = mapIntro'' (\t, _, _ => cong t)
-
-  public export
-  mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is}
-    -> Pointwise x.equivalence.relation xs ys
-    -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys)
-  mapIntro f = mapIntro' f.homomorphic
-
-  public export
-  wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is}
-    -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
-  wrapIntro []        = []
-  wrapIntro (r :: rs) = r :: wrapIntro rs
-
-  public export
-  unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {0 xs, ys : x ^ map f is}
-    -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
-  unwrapIntro {is = []}        []        = []
-  unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs
diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr
deleted file mode 100644
index ec73723..0000000
--- a/src/Soat/Data/Sublist.idr
+++ /dev/null
@@ -1,76 +0,0 @@
-module Soat.Data.Sublist
-
-import public Control.Relation
-import Data.List.Elem
-import Soat.Data.Product
-
-%default total
-
-infix 5 ++
-
-public export
-data Sublist : Rel (List a) where
-  Nil  : Sublist [] ys
-  (::) : (mem : Elem x ys) -> (mems : Sublist xs ys) -> Sublist (x :: xs) ys
-
-public export
-curry : xs `Sublist` ys -> forall x . Elem x xs -> Elem x ys
-curry (mem :: mems) Here      = mem
-curry (mem :: mems) (There y) = curry mems y
-
-public export
-uncurry : {xs : List a} -> (forall x . Elem x xs -> Elem x ys) -> xs `Sublist` ys
-uncurry {xs = []}        f = []
-uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There)
-
-public export
-uncurryCurry : (f : xs `Sublist` ys) -> uncurry (curry f) = f
-uncurryCurry []            = Refl
-uncurryCurry (mem :: mems) = cong ((::) mem) (uncurryCurry mems)
-
-public export
-curryUncurry : (0 f : forall x . Elem x xs -> Elem x ys) -> (i : Elem x xs)
-  -> curry (uncurry f) i = f i
-curryUncurry f Here         = Refl
-curryUncurry f (There elem) = curryUncurry (f . There) elem
-
-public export
-Reflexive (List a) Sublist where
-  reflexive = uncurry id
-
-public export
-Transitive (List a) Sublist where
-  transitive f g = uncurry (curry g . curry f)
-
-public export
-elemJoinL : Elem x xs -> Elem x (xs ++ ys)
-elemJoinL Here         = Here
-elemJoinL (There elem) = There (elemJoinL elem)
-
-public export
-elemJoinR : (xs : List a) -> Elem x ys -> Elem x (xs ++ ys)
-elemJoinR []        elem = elem
-elemJoinR (x :: xs) elem = There (elemJoinR xs elem)
-
-public export
-elemSplit : (xs : List a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys)
-elemSplit []        elem         = Right elem
-elemSplit (x :: xs) Here         = Left Here
-elemSplit (x :: xs) (There elem) = bimap There id (elemSplit xs elem)
-
-public export
-(++) : {xs, ys, us : List a}
-  -> xs `Sublist` ys -> us `Sublist` vs -> (xs ++ us) `Sublist` (ys ++ vs)
-(++) mems mems' = uncurry
-  (either (elemJoinL . curry mems) (elemJoinR ys . curry mems') . elemSplit xs)
-
-public export
-shuffle : is `Sublist` js -> x ^ js -> x ^ is
-shuffle []            xs = []
-shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs
-
-public export
-indexShuffle : (f : is `Sublist` js) -> {0 xs : x ^ js} -> (elem : Elem i is)
-  -> index (shuffle f xs) elem = index xs (curry f elem)
-indexShuffle (mem :: mems) Here         = Refl
-indexShuffle (mem :: mems) (There elem) = indexShuffle mems elem
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 31b25b4..876958f 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -1,7 +1,8 @@
 module Soat.FirstOrder.Algebra
 
+import public Data.Product
 import Data.Setoid.Indexed
-import public Soat.Data.Product
+
 import Soat.FirstOrder.Signature
 
 import Syntax.PreorderReasoning.Setoid
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 69bdcfc..00f7686 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,8 +1,8 @@
 module Soat.FirstOrder.Term
 
+import Data.Product
 import Data.Setoid.Indexed
 
-import Soat.Data.Product
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Signature
 
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 06d8674..95e5868 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -1,10 +1,10 @@
 module Soat.SecondOrder.Algebra
 
-import Data.Setoid.Indexed
 import Data.List.Elem
+import Data.List.Sublist
+import Data.Product
+import Data.Setoid.Indexed
 
-import Soat.Data.Product
-import Soat.Data.Sublist
 import Soat.SecondOrder.Signature
 
 infix 5 ~>
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index bb3d24b..93043c4 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -1,10 +1,10 @@
 module Soat.SecondOrder.Algebra.Lift
 
 import Data.List.Elem
+import Data.List.Sublist
+import Data.Product
 import Data.Setoid.Indexed
 
-import Soat.Data.Product
-import Soat.Data.Sublist
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Term
 import Soat.SecondOrder.Algebra
-- 
cgit v1.2.3