Migrate to use idris-setoid library.

3 files changed, 178 insertions, 206 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6e39612..31b25b4 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -1,12 +1,12 @@
 module Soat.FirstOrder.Algebra
 
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 import public Soat.Data.Product
 import Soat.FirstOrder.Signature
 
+import Syntax.PreorderReasoning.Setoid
+
 %default total
-%hide Control.Relation.Equivalence
 
 infix 5 ~>
 
@@ -24,15 +24,15 @@ public export
 record RawSetoidAlgebra (0 sig : Signature) where
   constructor MkRawSetoidAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel raw.U
+  0 relation : (t : sig.T) -> Rel (raw.U t)
 
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  0 relation  : IRel a.U
-  equivalence : IEquivalence a.U relation
+  equivalence : IndexedEquivalence sig.T a.U
   semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-    -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms')
+    -> Pointwise equivalence.relation tms tms'
+    -> equivalence.relation t (a.sem op tms) (a.sem op tms')
 
 public export
 record Algebra (0 sig : Signature) where
@@ -41,12 +41,12 @@ record Algebra (0 sig : Signature) where
   algebra    : IsAlgebra sig raw
 
 public export 0
-(.relation) : (0 a : Algebra sig) -> IRel a.raw.U
-(.relation) a = a.algebra.relation
+(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
+(.relation) a = a.algebra.equivalence.relation
 
 public export
-(.setoid) : Algebra sig -> ISetoid sig.T
-(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid sig.T
+(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence
 
 public export
 (.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
@@ -56,19 +56,16 @@ public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func    : (t : sig.T) -> a.raw.U t -> b.raw.U t
-  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
-    -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+  func    : a.setoid ~> b.setoid
   semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-    -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
+    -> b.relation t (func.H t (a.raw.sem op tms)) (b.raw.sem op (map func.H tms))
 
 public export
 id : {a : Algebra sig} -> a ~> a
 id = MkHomomorphism
-  { func    = \_ => id
-  , cong    = \_ => id
+  { func    = id a.setoid
   , semHomo = \op, tms =>
-    (a.algebra.equivalence _).equalImpliesEq $
+    reflect (index a.setoid _) $
     sym $
     cong (a.raw.sem op) $
     mapId tms
@@ -77,15 +74,11 @@ id = MkHomomorphism
 public export
 (.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
 (.) f g = MkHomomorphism
-  { func    = \t => f.func t . g.func t
-  , cong    = \t => f.cong t . g.cong t
+  { func    = f.func . g.func
   , semHomo = \op, tms =>
-    (c.algebra.equivalence _).transitive
-      (f.cong _ $ g.semHomo op tms) $
-    (c.algebra.equivalence _).transitive
-      (f.semHomo op (map g.func tms)) $
-    (c.algebra.equivalence _).equalImpliesEq $
-    sym $
-    cong (c.raw.sem op) $
-    mapComp tms
+    CalcWith (index c.setoid _) $
+    |~ f.func.H _ (g.func.H _ (a.raw.sem op tms))
+    ~~ f.func.H _ (b.raw.sem op (map g.func.H tms))   ...(f.func.homomorphic _ _ _ $ g.semHomo op tms)
+    ~~ c.raw.sem op (map f.func.H (map g.func.H tms)) ...(f.semHomo op $ map g.func.H tms)
+    ~~ c.raw.sem op (map ((f.func . g.func).H) tms)   .=<(cong (c.raw.sem op) $ mapComp tms)
   }
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5cb4c45..a8e4c0e 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -1,6 +1,5 @@
 module Soat.FirstOrder.Algebra.Coproduct
 
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 import Data.Setoid.Either
 
@@ -17,7 +16,9 @@ CoproductSet : (0 sig : Signature) -> (0 x, y : sig.T -> Type) -> sig.T -> Type
 CoproductSet sig x y = Term sig (\i => Either (x i) (y i))
 
 public export
-data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where
+data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> (t : sig.T)
+  -> Rel (CoproductSet sig x.raw.U y.raw.U t)
+  where
   DoneL    : {0 x, y : RawSetoidAlgebra sig}
     -> {t : sig.T} -> {i, j : x.raw.U t} -> x.relation t i j
     -> (~=~) x y t (Done $ Left i) (Done $ Left j)
@@ -36,31 +37,29 @@ data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y
     -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm'' -> (~=~) x y t tm tm''
 
 parameters {0 x, y : RawSetoidAlgebra sig}
-  coprodRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+  coprodRelRefl : (xRefl : (t : sig.T) -> (a : x.raw.U t) -> x.relation t a a)
+    -> (yRefl : (t : sig.T) -> (a : y.raw.U t) -> y.relation t a a)
     -> {t : _} -> (tm : _) -> (~=~) x y t tm tm
-  coprodsRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+  coprodsRelRefl : (xRefl : (t : sig.T) -> (a : x.raw.U t) -> x.relation t a a)
+    -> (yRefl : (t : sig.T) -> (a : y.raw.U t) -> y.relation t a a)
     -> {ts : _} -> (tms : _ ^ ts) -> Pointwise ((~=~) x y) tms tms
 
-  coprodRelRefl x y (Done (Left i))  = DoneL $ reflexive @{x _}
-  coprodRelRefl x y (Done (Right i)) = DoneR $ reflexive @{y _}
+  coprodRelRefl x y (Done (Left i))  = DoneL $ x _ i
+  coprodRelRefl x y (Done (Right i)) = DoneR $ y _ i
   coprodRelRefl x y (Call op ts)     = Call op $ coprodsRelRefl x y ts
 
   coprodsRelRefl x y []        = []
   coprodsRelRefl x y (t :: ts) = coprodRelRefl x y t :: coprodsRelRefl x y ts
 
-  coprodsRelReflexive : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
-    -> {ts : _} -> {tms, tms' : _ ^ ts} -> tms = tms' -> Pointwise ((~=~) x y) tms tms'
-  coprodsRelReflexive x y Refl = coprodsRelRefl x y _
-
-  tmRelImpliesCoprodRel : Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i)) t tm tm'
+  tmRelImpliesCoprodRel : Term.Rel.(~=~) (\i => x.relation i `Or` y.relation i) t tm tm'
     -> (~=~) x y t tm tm'
   tmRelsImpliesCoprodRels : {0 tms, tms' : _ ^ ts}
-    -> Pointwise (Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i))) tms tms'
+    -> Pointwise (Term.Rel.(~=~) (\i => x.relation i `Or` y.relation i)) tms tms'
     -> Pointwise ((~=~) x y) tms tms'
 
-  tmRelImpliesCoprodRel (Done' (Left eq))  = DoneL eq
-  tmRelImpliesCoprodRel (Done' (Right eq)) = DoneR eq
-  tmRelImpliesCoprodRel (Call' op eqs)     = Call op $ tmRelsImpliesCoprodRels eqs
+  tmRelImpliesCoprodRel (Done (Left eq))  = DoneL eq
+  tmRelImpliesCoprodRel (Done (Right eq)) = DoneR eq
+  tmRelImpliesCoprodRel (Call op eqs)     = Call op $ tmRelsImpliesCoprodRels eqs
 
   tmRelsImpliesCoprodRels []          = []
   tmRelsImpliesCoprodRels (eq :: eqs) = tmRelImpliesCoprodRel eq :: tmRelsImpliesCoprodRels eqs
@@ -76,17 +75,17 @@ public export
 CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y
   -> IsAlgebra sig (Coproduct x y)
 CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
-  { relation =
-    (~=~)
-      (MkRawSetoidAlgebra x xIsAlgebra.relation)
-      (MkRawSetoidAlgebra y yIsAlgebra.relation)
-  , equivalence = \t => MkEquivalence
-    { refl  = MkReflexive $ coprodRelRefl
-        (\t => (xIsAlgebra.equivalence t).refl)
-        (\t => (yIsAlgebra.equivalence t).refl)
-        _
-    , sym   = MkSymmetric $ Sym
-    , trans = MkTransitive $ Trans
+  { equivalence = MkIndexedEquivalence
+    { relation   =
+        (~=~)
+          (MkRawSetoidAlgebra x xIsAlgebra.equivalence.relation)
+          (MkRawSetoidAlgebra y yIsAlgebra.equivalence.relation)
+    , reflexive  = \_ =>
+      coprodRelRefl
+        xIsAlgebra.equivalence.reflexive
+        yIsAlgebra.equivalence.reflexive
+    , symmetric  = \_, _, _ => Sym
+    , transitive = \_, _, _, _ => Trans
     }
   , semCong = Call
   }
@@ -98,87 +97,84 @@ CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.
 public export
 injectLHomo : x ~> CoproductAlgebra x y
 injectLHomo = MkHomomorphism
-  { func    = \_ => Done . Left
-  , cong    = \_ => DoneL
+  { func    = MkIndexedSetoidHomomorphism (\_ => Done . Left) (\_, _, _ => DoneL)
   , semHomo = InjectL
   }
 
 public export
 injectRHomo : y ~> CoproductAlgebra x y
 injectRHomo = MkHomomorphism
-  { func    = \_ => Done . Right
-  , cong    = \_ => DoneR
+  { func    = MkIndexedSetoidHomomorphism (\_ => Done . Right) (\_, _, _ => DoneR)
   , semHomo = InjectR
   }
 
 public export
-coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
+coproduct : {z : RawAlgebra sig}
+  -> (f : (t : sig.T) -> x t -> z.U t) -> (g : (t : sig.T) -> y t -> z.U t)
+  -> (t : sig.T) -> CoproductSet sig x y t -> z.U t
 coproduct f g _ = bindTerm (\i => either (f i) (g i))
 
 public export
-coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
-  -> CoproductSet sig x y ^ ts -> z.U ^ ts
+coproducts : {z : RawAlgebra sig}
+  -> (f : (t : sig.T) -> x t -> z.U t) -> (g : (t : sig.T) -> y t -> z.U t)
+  -> (ts : List sig.T) -> CoproductSet sig x y ^ ts -> z.U ^ ts
 coproducts f g _ = bindTerms (\i => either (f i) (g i))
 
 public export
 coproductCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-  -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
-  -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
+  -> {t : sig.T} -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
+  -> (z.relation t `on` coproduct {z = z.raw} f.func.H g.func.H t) tm tm'
 
 public export
 coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-  -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
+  -> {ts : List sig.T} -> {tms, tms' : _ ^ ts}
   -> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
-  -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
-
-coproductCong f g _ (DoneL eq)       = f.cong _ eq
-coproductCong f g _ (DoneR eq)       = g.cong _ eq
-coproductCong f g _ (Call op eqs)    =
-  z.algebra.semCong op $
-  coproductsCong f g _ eqs
-coproductCong f g _ (InjectL op ts)  = CalcWith (z.setoid.index _) $
-  |~ f.func _ (x.raw.sem op ts)
-  ~~ z.raw.sem op (map f.func ts)                                              ...(f.semHomo op ts)
-  ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
-  ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
-coproductCong f g _ (InjectR op ts)  = CalcWith (z.setoid.index _) $
-  |~ g.func _ (y.raw.sem op ts)
-  ~~ z.raw.sem op (map g.func ts)                                               ...(g.semHomo op ts)
-  ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
-  ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
-coproductCong f g _ (Sym eq)         = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
-coproductCong f g _ (Trans eq eq')   = (z.algebra.equivalence _).transitive
-  (coproductCong f g _ eq)
-  (coproductCong f g _ eq')
-
-coproductsCong f g _ []          = []
-coproductsCong f g _ (eq :: eqs) =
-  coproductCong f g _ eq :: coproductsCong f g _ eqs
+  -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func.H g.func.H ts)) tms tms'
+
+coproductCong f g (DoneL eq)       = f.func.homomorphic _ _ _ eq
+coproductCong f g (DoneR eq)       = g.func.homomorphic _ _ _ eq
+coproductCong f g (Call op eqs)    = z.algebra.semCong op $ coproductsCong f g eqs
+coproductCong f g (InjectL op ts)  = CalcWith (index z.setoid _) $
+  |~ f.func.H _ (x.raw.sem op ts)
+  ~~ z.raw.sem op (map f.func.H ts)                                                ...(f.semHomo op ts)
+  ~~ z.raw.sem op (map (coproduct f.func.H g.func.H) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+  ~~ z.raw.sem op (coproducts f.func.H g.func.H _ (map (\_ => Done . Left) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g (InjectR op ts)  = CalcWith (index z.setoid _) $
+  |~ g.func.H _ (y.raw.sem op ts)
+  ~~ z.raw.sem op (map g.func.H ts)                                                 ...(g.semHomo op ts)
+  ~~ z.raw.sem op (map (coproduct f.func.H g.func.H) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+  ~~ z.raw.sem op (coproducts f.func.H g.func.H _ (map (\_ => Done . Right) ts))    .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g (Sym eq)         = z.algebra.equivalence.symmetric _ _ _ $ coproductCong f g eq
+coproductCong f g (Trans eq eq')   = z.algebra.equivalence.transitive _ _ _ _
+  (coproductCong f g eq)
+  (coproductCong f g eq')
+
+coproductsCong f g []          = []
+coproductsCong f g (eq :: eqs) = coproductCong f g eq :: coproductsCong f g eqs
 
 public export
 coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
   -> CoproductAlgebra x y ~> z
 coproductHomo f g = MkHomomorphism
-  { func = coproduct {z = z.raw} f.func g.func
-  , cong = coproductCong f g
+  { func = MkIndexedSetoidHomomorphism
+    { H           = coproduct {z = z.raw} f.func.H g.func.H
+    , homomorphic = \_, _, _ => coproductCong f g
+    }
   , semHomo = \op, tms =>
-    (z.algebra.equivalence _).equalImpliesEq $
+    reflect (index z.setoid _) $
     cong (z.raw.sem op) $
     bindTermsIsMap {a = z.raw} _ tms
   }
 
 public export
 termToCoproduct : (x, y : Algebra sig)
-  -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
+  -> FreeAlgebra (bundle (\t => Either (index x.setoid t) (index y.setoid t))) ~>
      CoproductAlgebra x y
 termToCoproduct x y = MkHomomorphism
-  { func    = \_ => id
-  , cong    = \t => tmRelImpliesCoprodRel
+  { func    = MkIndexedSetoidHomomorphism (\_ => id) (\t, _, _ => tmRelImpliesCoprodRel)
   , semHomo = \op, tms =>
     Call op $
-    coprodsRelReflexive
-      (\i => (x.algebra.equivalence i).refl)
-      (\i => (y.algebra.equivalence i).refl) $
+    reflect (index (pwSetoid (CoproductAlgebra x y).setoid) _) $
     sym $
     mapId tms
   }
@@ -188,13 +184,13 @@ coproductUnique' : {x, y, z : Algebra sig}
   -> (f : CoproductAlgebra x y ~> z)
   -> (g : CoproductAlgebra x y ~> z)
   -> (congL : {t : sig.T} -> (i : x.raw.U t)
-        -> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i))))
+        -> z.relation t (f.func.H t (Done (Left i))) (g.func.H t (Done (Left i))))
   -> (congR : {t : sig.T} -> (i : y.raw.U t)
-        -> z.relation t (f.func t (Done (Right i))) (g.func t (Done (Right i))))
+        -> z.relation t (f.func.H t (Done (Right i))) (g.func.H t (Done (Right i))))
   -> {t : sig.T} -> (tm : _)
-  -> z.relation t (f.func t tm) (g.func t tm)
+  -> z.relation t (f.func.H t tm) (g.func.H t tm)
 coproductUnique' f g congL congR tm = bindUnique'
-  { v = fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))
+  { v = bundle (\t => Either (index x.setoid t) (index y.setoid t))
   , f = f . termToCoproduct x y
   , g = g . termToCoproduct x y
   , cong = \x => case x of
@@ -207,9 +203,9 @@ public export
 coproductUnique : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
   -> (h : CoproductAlgebra x y ~> z)
   -> (congL : {t : sig.T} -> (i : x.raw.U t)
-        -> z.relation t (h.func t (Done (Left i))) (f.func t i))
+        -> z.relation t (h.func.H t (Done (Left i))) (f.func.H t i))
   -> (congR : {t : sig.T} -> (i : y.raw.U t)
-        -> z.relation t (h.func t (Done (Right i))) (g.func t i))
+        -> z.relation t (h.func.H t (Done (Right i))) (g.func.H t i))
   -> {t : sig.T} -> (tm : _)
-  -> z.relation t (h.func t tm) (coproduct {z = z.raw} f.func g.func t tm)
+  -> z.relation t (h.func.H t tm) (coproduct {z = z.raw} f.func.H g.func.H t tm)
 coproductUnique f g h = coproductUnique' h (coproductHomo f g)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index f9f0879..69bdcfc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,11 +1,11 @@
 module Soat.FirstOrder.Term
 
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 
 import Soat.Data.Product
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Signature
+
 import Syntax.PreorderReasoning.Setoid
 
 %default total
@@ -16,10 +16,12 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
   Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
 
 public export
-bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t
+bindTerm : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+  -> {t : _} -> Term sig v t -> a.U t
 
 public export
-bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
+bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+  -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
 
 bindTerm         env (Done i)     = env _ i
 bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
@@ -29,197 +31,178 @@ bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
 
 public export
 bindTermsIsMap : {auto a : RawAlgebra sig}
-  -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
+  -> (env : (t : sig.T) -> v t -> a.U t) -> {ts : _} -> (tms : Term sig v ^ ts)
   -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
 bindTermsIsMap env []        = Refl
 bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
 
--- FIXME: these names shouldn't be public. Indication of bad API design
 namespace Rel
   public export
-  data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
+  data (~=~) : forall v . (0 r : (t : sig.T) -> Rel (v t)) -> (t : sig.T) -> Rel (Term sig v t)
     where
-    Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+    Done : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
       -> {t : sig.T} -> {i, j : v t}
       -> r t i j
       -> (~=~) {sig} {v} r t (Done i) (Done j)
-    Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+    Call : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
       -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity}
       -> Pointwise ((~=~) {sig} {v} r) tms tms'
       -> (~=~) {sig} {v} r t (Call op tms) (Call op tms')
 
-  public export
-  tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm'
-
-  public export
-  tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms'
-
-  tmRelEqualIsEqual (Done' eq)     = cong Done eq
-  tmRelEqualIsEqual (Call' op eqs) = cong (Call op) $ tmsRelEqualIsEqual eqs
-
-  tmsRelEqualIsEqual []          = Refl
-  tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs)
-
-  public export
-  tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+  tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
     -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
 
-  public export
-  tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+  tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
     -> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
 
-  tmRelRefl refl (Done i)     = Done' reflexive
-  tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
+  tmRelRefl refl (Done i)     = Done (refl _ i)
+  tmRelRefl refl (Call op ts) = Call op (tmsRelRefl refl ts)
 
   tmsRelRefl refl []        = []
   tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
 
-  public export
-  tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-    -> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm'
-  tmRelReflexive refl Refl = tmRelRefl refl _
-
-  public export
-  tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-    -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-    -> tms = tms' -> Pointwise ((~=~) rel) tms tms'
-  tmsRelReflexive refl Refl = tmsRelRefl refl _
-
-  public export
-  tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+  tmRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
     -> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
 
-  public export
-  tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+  tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
     -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
     -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
 
-  tmRelSym sym (Done' i)     = Done' (symmetric i)
-  tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)
+  tmRelSym sym (Done i)     = Done (sym _ _ _ i)
+  tmRelSym sym (Call op ts) = Call op (tmsRelSym sym ts)
 
   tmsRelSym sym []        = []
   tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
 
-  public export
-  tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+  tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
     -> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
     -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
 
-  public export
-  tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+  tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+    -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
     -> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
     -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
     -> Pointwise ((~=~) rel) tms tms''
 
-  tmRelTrans trans (Done' i)     (Done' j)     = Done' (transitive i j)
-  tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')
+  tmRelTrans trans (Done i)     (Done j)     = Done (trans _ _ _ _ i j)
+  tmRelTrans trans (Call op ts) (Call _ ts') = Call op (tmsRelTrans trans ts ts')
 
   tmsRelTrans trans []        []          = []
   tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
 
-  export
-  tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
-    -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
-  tmRelEq eq t = MkEquivalence
-    (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
-    (MkSymmetric $ tmRelSym (\t => (eq t).sym))
-    (MkTransitive $ tmRelTrans (\t => (eq t).trans))
+  public export
+  tmRelEq : IndexedEquivalence sig.T v -> IndexedEquivalence sig.T (Term sig v)
+  tmRelEq eq = MkIndexedEquivalence
+    { relation   = (~=~) eq.relation
+    , reflexive  = \t => tmRelRefl eq.reflexive
+    , symmetric  = \t, x, y => tmRelSym eq.symmetric
+    , transitive = \t, x, y, z => tmRelTrans eq.transitive
+    }
 
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
 Free v = MkRawAlgebra (Term sig v) Call
 
 public export
-FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U)
-FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call'
+FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U)
+FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call
 
 public export
-FreeAlgebra : ISetoid sig.T -> Algebra sig
+FreeAlgebra : IndexedSetoid sig.T -> Algebra sig
 FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
 
 public export
-bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+  -> {0 rel : (t : sig.T) -> Rel (v t)}
   -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-  -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
+  -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (eq : (~=~) rel t tm tm')
   -> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
 
 public export
-bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermsCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+  -> {0 rel : (t : sig.T) -> Rel (v t)}
   -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-  -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
+  -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> (eqs : Pointwise ((~=~) rel) tms tms')
   -> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
 
-bindTermCong'         cong (Done' i)     = cong _ i
-bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
+bindTermCong'         cong (Done i)     = cong _ i
+bindTermCong' {a = a} cong (Call op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
 
 bindTermsCong' cong []        = []
 bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
 
 public export
-bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
-  -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
-bindTermCong env = bindTermCong' env.cong
+bindTermCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+  -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (eq : (~=~) v.equivalence.relation t tm tm')
+  -> a.relation t (bindTerm {a = a.raw} env.H tm) (bindTerm {a = a.raw} env.H tm')
+bindTermCong env = bindTermCong' env.homomorphic
 
 public export
-bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-  -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
-  -> Pointwise a.relation
-       (bindTerms {a = a.raw} env.func tms)
-       (bindTerms {a = a.raw} env.func tms')
-bindTermsCong env = bindTermsCong' env.cong
+bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+  -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts}
+  -> (eqs : Pointwise ((~=~) v.equivalence.relation) tms tms')
+  -> Pointwise a.relation (bindTerms {a = a.raw} env.H tms) (bindTerms {a = a.raw} env.H tms')
+bindTermsCong env = bindTermsCong' env.homomorphic
 
 public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
+bindHomo : {a : Algebra sig} -> (env : v ~> a.setoid) -> FreeAlgebra v ~> a
 bindHomo env = MkHomomorphism
-  { func    = \_ => bindTerm {a = a.raw} env.func
-  , cong    = \_ => bindTermCong env
+  { func    = MkIndexedSetoidHomomorphism
+    { H           = \_ => bindTerm {a = a.raw} env.H
+    , homomorphic = \_, _, _ => bindTermCong env
+    }
   , semHomo = \op, tms =>
     a.algebra.semCong op $
-    map (\t => (a.algebra.equivalence t).equalImpliesEq) $
-    equalImpliesPwEq $
-    bindTermsIsMap {a = a.raw} env.func tms
+    reflect (index (pwSetoid a.setoid) _) $
+    bindTermsIsMap {a = a.raw} env.H tms
   }
 
 public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
   -> (f, g : FreeAlgebra v ~> a)
-  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+  -> (cong : {t : sig.T} -> (i : v.U t)
+        -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
   -> {t : sig.T} -> (tm : Term sig v.U t)
-  -> a.relation t (f.func t tm) (g.func t tm)
+  -> a.relation t (f.func.H t tm) (g.func.H t tm)
 
 public export
-bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindsUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
   -> (f, g : FreeAlgebra v ~> a)
-  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+  -> (cong : {t : sig.T} -> (i : v.U t)
+        -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-  -> Pointwise a.relation (map f.func tms) (map g.func tms)
+  -> Pointwise a.relation (map f.func.H tms) (map g.func.H tms)
 
 bindUnique' f g cong (Done i)     = cong i
-bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
-  |~ f.func _ (Call op ts)
-  ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
-  ~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
-  ~~ g.func _ (Call op ts)        ..<( g.semHomo op ts )
+bindUnique' f g cong (Call op ts) = CalcWith (index a.setoid _) $
+  |~ f.func.H _ (Call op ts)
+  ~~ a.raw.sem op (map f.func.H ts) ...( f.semHomo op ts )
+  ~~ a.raw.sem op (map g.func.H ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
+  ~~ g.func.H _ (Call op ts)        ..<( g.semHomo op ts )
 
 bindsUnique' f g cong []        = []
 bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
 
 public export
-bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
   -> (f : FreeAlgebra v ~> a)
-  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i))
   -> {t : sig.T} -> (tm : Term sig v.U t)
-  -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
+  -> a.relation t (f.func.H t tm) (bindTerm {a = a.raw} env.H tm)
 bindUnique env f = bindUnique' f (bindHomo env)
 
 public export
-bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
   -> (f : FreeAlgebra v ~> a)
-  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+  -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-  -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
-bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $
-  |~ map f.func ts
-  ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
-  ~~ bindTerms {a = a.raw} env.func ts            .=<( bindTermsIsMap {a = a.raw} env.func ts )
+  -> Pointwise a.relation (map f.func.H tms) (bindTerms {a = a.raw} env.H tms)
+bindsUnique env f cong ts = CalcWith (index (pwSetoid a.setoid) _) $
+  |~ map f.func.H ts
+  ~~ map (\_ => bindTerm {a = a.raw} env.H) ts ...( bindsUnique' f (bindHomo env) cong ts )
+  ~~ bindTerms {a = a.raw} env.H ts            .=<( bindTermsIsMap {a = a.raw} env.H ts )