refactor: split product setoid into a new module.

7 files changed, 113 insertions, 107 deletions

diff --git a/src/Data/Product.idr b/src/Data/Product.idr
index 348fa44..f1b5cc2 100644
--- a/src/Data/Product.idr
+++ b/src/Data/Product.idr
@@ -1,7 +1,6 @@
 module Data.Product
 
 import Data.List.Elem
-import Data.Setoid.Indexed
 
 %default total
 
@@ -120,108 +119,3 @@ 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/Data/Setoid/Product.idr b/src/Data/Setoid/Product.idr
new file mode 100644
index 0000000..90510e5
--- /dev/null
+++ b/src/Data/Setoid/Product.idr
@@ -0,0 +1,107 @@
+module Data.Setoid.Product
+
+import Data.List.Elem
+import public Data.Product
+import Data.Setoid.Indexed
+
+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/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 876958f..97b6adc 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.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Product
 
 import Soat.FirstOrder.Signature
 
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index a8e4c0e..88db184 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -2,6 +2,7 @@ module Soat.FirstOrder.Algebra.Coproduct
 
 import Data.Setoid.Indexed
 import Data.Setoid.Either
+import Data.Setoid.Product
 
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Signature
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 00f7686..ee17093 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -2,6 +2,7 @@ module Soat.FirstOrder.Term
 
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Product
 
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Signature
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 95e5868..e7927ae 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -4,6 +4,7 @@ import Data.List.Elem
 import Data.List.Sublist
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Product
 
 import Soat.SecondOrder.Signature
 
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 93043c4..116b5e4 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -4,6 +4,7 @@ import Data.List.Elem
 import Data.List.Sublist
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Product
 
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Term