Migrate to use idris-setoid library.

12 files changed, 433 insertions, 659 deletions

diff --git a/soat.ipkg b/soat.ipkg
index d5cdcd9..e5b4f05 100644
--- a/soat.ipkg
+++ b/soat.ipkg
@@ -2,11 +2,9 @@ package soat
 authors = "Greg Brown"
 sourcedir = "src"
 
-modules = Data.Morphism.Indexed
-        , Data.Setoid
-        , Data.Setoid.Either
-        , Data.Setoid.Indexed
-        , Soat.Data.Product
+depends = setoid
+
+modules = Soat.Data.Product
         , Soat.Data.Sublist
         , Soat.FirstOrder.Algebra
         , Soat.FirstOrder.Algebra.Coproduct
@@ -16,4 +14,3 @@ modules = Data.Morphism.Indexed
         , Soat.SecondOrder.Algebra.Lift
         , Soat.SecondOrder.Signature
         , Soat.SecondOrder.Signature.Lift
-        , Syntax.PreorderReasoning.Setoid
diff --git a/src/Data/Morphism/Indexed.idr b/src/Data/Morphism/Indexed.idr
deleted file mode 100644
index c271c90..0000000
--- a/src/Data/Morphism/Indexed.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-module Data.Morphism.Indexed
-
-import Data.Setoid.Indexed
-
-public export
-IFunc : {a : Type} -> (x, y : a -> Type) -> Type
-IFunc {a} x y = (i : a) -> x i -> y i
-
-public export
-record IFunction {a : Type} (x, y : ISetoid a) where
-  constructor MkIFunction
-  func : IFunc x.U y.U
-  cong : (i : a) -> {u, v : x.U i} -> x.relation i u v -> y.relation i (func i u) (func i v)
diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr
deleted file mode 100644
index 8014bac..0000000
--- a/src/Data/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-module Data.Setoid
-
-import public Control.Relation
-
-%default total
-
-public export
-record Equivalence a (rel : Rel a) where
-  constructor MkEquivalence
-  refl  : Reflexive a rel
-  sym   : Symmetric a rel
-  trans : Transitive a rel
-
-public export
-record Setoid where
-  constructor MkSetoid
-  0 U         : Type
-  0 relation  : Rel U
-  equivalence : Data.Setoid.Equivalence U relation
-
-public export
-equiv : Control.Relation.Equivalence a rel => Data.Setoid.Equivalence a rel
-equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive)
-
-public export
-[refl'] (eq : Data.Setoid.Equivalence a rel) => Reflexive a rel where
-  reflexive = reflexive @{eq.refl}
-
-public export
-[sym'] (eq : Data.Setoid.Equivalence a rel) => Symmetric a rel where
-  symmetric = symmetric @{eq.sym}
-
-public export
-[trans'] (eq : Data.Setoid.Equivalence a rel) => Transitive a rel where
-  transitive = transitive @{eq.trans}
-
-public export
-[equiv'] Data.Setoid.Equivalence a rel => Control.Relation.Equivalence a rel
-  using refl' sym' trans' where
-
-public export
-(.reflexive) : Data.Setoid.Equivalence a rel -> {x : a} -> rel x x
-(.reflexive) eq = reflexive @{eq.refl}
-
-public export
-(.symmetric) : Data.Setoid.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x
-(.symmetric) eq = symmetric @{eq.sym}
-
-public export
-(.transitive) : Data.Setoid.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z
-(.transitive) eq = transitive @{eq.trans}
-
-public export
-(.equalImpliesEq) : Data.Setoid.Equivalence a rel -> {x, y : a} -> x = y -> rel x y
-(.equalImpliesEq) eq Refl = eq.reflexive
diff --git a/src/Data/Setoid/Either.idr b/src/Data/Setoid/Either.idr
deleted file mode 100644
index 682ac5a..0000000
--- a/src/Data/Setoid/Either.idr
+++ /dev/null
@@ -1,37 +0,0 @@
-module Data.Setoid.Either
-
-import public Data.Setoid
-
-public export
-data Either : (0 r : Rel a) -> (0 s : Rel b) -> Rel (Either a b) where
-  Left  : forall r, s . r x y -> Either r s (Left x) (Left y)
-  Right : forall r, s . s x y -> Either r s (Right x) (Right y)
-
-public export
-[eitherRefl] Reflexive a rel => Reflexive b rel' => Reflexive (Either a b) (Either rel rel') where
-  reflexive {x = (Left x)}  = Left reflexive
-  reflexive {x = (Right x)} = Right reflexive
-
-public export
-[eitherSym] Symmetric a rel => Symmetric b rel' => Symmetric (Either a b) (Either rel rel') where
-  symmetric (Left eq)  = Left $ symmetric eq
-  symmetric (Right eq) = Right $ symmetric eq
-
-public export
-[eitherTrans] Transitive a rel => Transitive b rel'
-  => Transitive (Either a b) (Either rel rel') where
-  transitive (Left eq)  (Left eq')  = Left $ transitive eq eq'
-  transitive (Right eq) (Right eq') = Right $ transitive eq eq'
-
-public export
-EitherEquivalence : Setoid.Equivalence a rel -> Setoid.Equivalence b rel'
-  -> Setoid.Equivalence (Either a b) (Either rel rel')
-EitherEquivalence eq eq' = MkEquivalence
-  { refl  = MkReflexive $ reflexive @{eitherRefl @{eq.refl} @{eq'.refl}}
-  , sym   = MkSymmetric $ symmetric @{eitherSym @{eq.sym} @{eq'.sym}}
-  , trans = MkTransitive $ transitive @{eitherTrans @{eq.trans} @{eq'.trans}}
-  }
-
-public export
-EitherSetoid : Setoid -> Setoid -> Setoid
-EitherSetoid x y = MkSetoid _ _ $ EitherEquivalence x.equivalence y.equivalence
diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr
deleted file mode 100644
index a04b647..0000000
--- a/src/Data/Setoid/Indexed.idr
+++ /dev/null
@@ -1,48 +0,0 @@
-module Data.Setoid.Indexed
-
-import public Data.Setoid
-
-%default total
-
-public export
-IRel : {a : Type} -> (a -> Type) -> Type
-IRel {a = a} x = (i : a) -> x i -> x i -> Type
-
-public export
-IReflexive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-IReflexive x rel = (i : a) -> Reflexive (x i) (rel i)
-
-public export
-ISymmetric : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-ISymmetric x rel = (i : a) -> Symmetric (x i) (rel i)
-
-public export
-ITransitive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-ITransitive x rel = (i : a) -> Transitive (x i) (rel i)
-
-public export
-IEquivalence : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-IEquivalence x rel = (i : a) -> Setoid.Equivalence (x i) (rel i)
-
-public export
-record ISetoid (a : Type) where
-  constructor MkISetoid
-  0 U         : a -> Type
-  0 relation  : IRel U
-  equivalence : IEquivalence U relation
-
-public export
-fromIndexed : (a -> Setoid) -> ISetoid a
-fromIndexed x = MkISetoid (\i => (x i).U) (\i => (x i).relation) (\i => (x i).equivalence)
-
-public export
-(.index) : ISetoid a -> a -> Setoid
-(.index) x i = MkSetoid (x.U i) (x.relation i) (x.equivalence i)
-
-public export
-reindex : (a -> b) -> ISetoid b -> ISetoid a
-reindex f x = MkISetoid (x.U . f) (\i => x.relation $ f i) (\i => x.equivalence $ f i)
-
-public export
-isetoid : (a -> Type) -> ISetoid a
-isetoid u = MkISetoid u (\_ => Equal) (\_ => equiv)
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index 0cb5dda..1532d4b 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -1,7 +1,6 @@
 module Soat.Data.Product
 
 import Data.List.Elem
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 
 %default total
@@ -68,7 +67,7 @@ map f []        = []
 map f (x :: xs) = f _ x :: map f xs
 
 public export
-indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is)
+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
@@ -79,8 +78,8 @@ mapId []        = Refl
 mapId (x :: xs) = cong ((::) x) $ mapId xs
 
 public export
-mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is)
-  -> map (\i => f i . g i) xs = map f (map g xs)
+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
 
@@ -95,7 +94,7 @@ wrap f []        = []
 wrap f (x :: xs) = x :: wrap f xs
 
 public export
-mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is)
+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
@@ -106,7 +105,8 @@ unwrap f {is = []}        []        = []
 unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
 
 public export
-mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is)
+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
@@ -148,89 +148,80 @@ namespace Pointwise
 
   -- Relational Properties
 
-  public export
   pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
   pwEqImpliesEqual []        = Refl
   pwEqImpliesEqual (r :: rs) = trans
     (sym $ consHeadTail _)
     (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
 
-  public export
   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)
 
-  -- FIXME: work out how to expose interfaces
-
-  public export
   pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> Reflexive (x i) (rel i))
-    -> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs
-  pwRefl f {xs = []}        = []
-  pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
-
+    -> ((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
 
-  public export
-  pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> Reflexive (x i) (rel i))
-    -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys
-  pwReflexive refl Refl = pwRefl refl
-
-  public export
   pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> Symmetric (x i) (rel 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 f []        = []
-  pwSym f (r :: rs) = symmetric r :: pwSym f rs
+  pwSym sym []        = []
+  pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs
 
-  public export
   pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
-    -> ((i : a) -> Transitive (x i) (rel 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 f []        []        = []
-  pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss
+  pwTrans trans []        []        = []
+  pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss
 
   public export
-  pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel)
-  pwEquivalence eq = MkEquivalence
-    (MkReflexive $ pwRefl (\i => (eq i).refl))
-    (MkSymmetric $ pwSym (\i => (eq i).sym))
-    (MkTransitive $ pwTrans (\i => (eq i).trans))
+  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 : ISetoid a -> List a -> Setoid
-  pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence)
+  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 : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+  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 : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+  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 : IFunction x y) -> {is : _} -> {xs, ys : x.U ^ is}
-    -> Pointwise x.relation xs ys -> Pointwise y.relation (map f.func xs) (map f.func ys)
-  mapIntro f = mapIntro' f.cong
+  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 : IRel x} -> {0 xs, ys : (x . f) ^ is}
+  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 : {0 f : a -> b} -> {0 rel : IRel x} -> {is : List a} -> {0 xs, ys : x ^ map f is}
+  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 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 )
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 6f7cb4a..06d8674 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -1,6 +1,5 @@
 module Soat.SecondOrder.Algebra
 
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 import Data.List.Elem
 
@@ -15,15 +14,10 @@ extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type
 extend x ctx ty = x (snd ty) (fst ty ++ ctx)
 
 public export
-extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U))
-  -> (ctx : List a) -> IRel (extend U ctx)
+extendRel : {U : a -> List a -> Type} -> (rel : (ty : _) -> Rel (uncurry U ty))
+  -> (ctx : List a) -> (ty : _) -> Rel (extend U ctx ty)
 extendRel rel ctx ty = rel (snd ty, fst ty ++ ctx)
 
-public export
-extendFunc : {0 U, V : a -> List a -> Type} -> (f : (t : a) -> IFunc (U t) (V t)) -> (ctx : List a)
-  -> IFunc (extend U ctx) (extend V ctx)
-extendFunc f ctx ty = f (snd ty) (fst ty ++ ctx)
-
 public export 0
 algebraOver : (sig : Signature) -> (U : sig.T -> List sig.T -> Type) -> Type
 algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
@@ -41,7 +35,7 @@ record RawAlgebra (0 sig : Signature) where
 
 public export
 (.extendSubst) : (a : RawAlgebra sig) -> (ctx : List sig.T) -> {ctx' : List sig.T}
-  -> (tms : (\t => a.U t ctx) ^ ctx') -> IFunc (extend a.U ctx') (extend a.U ctx)
+  -> (tms : (\t => a.U t ctx) ^ ctx') -> (ty : _) -> extend a.U ctx' ty -> extend a.U ctx ty
 a .extendSubst ctx tms ty tm = a.subst
   (snd ty)
   (fst ty ++ ctx)
@@ -52,65 +46,69 @@ a .extendSubst ctx tms ty tm = a.subst
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  0 relation  : IRel (uncurry a.U)
-  equivalence : IEquivalence (uncurry a.U) relation
+  equivalence : IndexedEquivalence _ (uncurry a.U)
   -- Congruences
   renameCong  : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-    -> {tm, tm' : a.U t ctx} -> relation (t, ctx) tm tm'
-    -> relation (t, ctx') (a.rename t f tm) (a.rename t f tm')
+    -> {tm, tm' : a.U t ctx} -> equivalence.relation (t, ctx) tm tm'
+    -> equivalence.relation (t, ctx') (a.rename t f tm) (a.rename t f tm')
   semCong     : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> {tms, tms' : extend a.U ctx ^ op.arity}
-    -> Pointwise (extendRel {U = a.U} relation ctx) tms tms'
-    -> relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
+    -> Pointwise (extendRel {U = a.U} equivalence.relation ctx) tms tms'
+    -> equivalence.relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
   substCong   : (t : sig.T) -> (ctx : List sig.T)
-    -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> relation (t, ctx') tm tm'
-    -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} -> Pointwise (\t => relation (t, ctx)) tms tms'
-    -> relation (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
+    -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> equivalence.relation (t, ctx') tm tm'
+    -> {tms, tms' : (\t => a.U t ctx) ^ ctx'}
+    -> Pointwise (\t => equivalence.relation (t, ctx)) tms tms'
+    -> equivalence.relation (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
   -- rename is functorial
   renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
-    -> relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
+    -> equivalence.relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
   renameComp  : (t : sig.T) -> {ctx, ctx', ctx'' : _}
     -> (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
     -> (tm : a.U t ctx)
-    -> relation (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
+    -> equivalence.relation (t, ctx'')
+         (a.rename t (transitive g f) tm)
+         (a.rename t f $ a.rename t g tm)
   -- sem are natural transformation
   semNat      : {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.U ctx ^ op.arity)
-    -> relation (t, ctx')
+    -> equivalence.relation (t, ctx')
          (a.rename t f $ a.sem ctx op tms)
          (a.sem ctx' op $
           map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
           tms)
   -- var is natural transformation
   varNat      : {t : _} -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
-    -> relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
+    -> equivalence.relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
   -- subst is natural transformation
   substNat    : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
     -> {ctx'' : _} -> (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'')
-    -> relation (t, ctx')
+    -> equivalence.relation (t, ctx')
          (a.rename t f $ a.subst t ctx tm tms)
          (a.subst t ctx' tm $ map (\t => a.rename t f) tms)
   -- subst is extranatural transformation
   substExnat  : (t : sig.T) -> (ctx : List sig.T)
     -> {ctx', ctx'' : _} -> (f : ctx' `Sublist` ctx'')
     -> (tm : a.U t ctx') -> (tms : (\t => a.U t ctx) ^ ctx'')
-    -> relation (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
+    -> equivalence.relation (t, ctx)
+         (a.subst t ctx (a.rename t f tm) tms)
+         (a.subst t ctx tm (shuffle f tms))
   -- var, subst is a monoid
   substComm   : (t : sig.T) -> (ctx : List sig.T)
     -> {ctx', ctx'' : _} -> (tm : a.U t ctx'')
     -> (tms : (\t => a.U t ctx') ^ ctx'') -> (tms' : (\t => a.U t ctx) ^ ctx')
-    -> relation (t, ctx)
+    -> equivalence.relation (t, ctx)
          (a.subst t ctx (a.subst t ctx' tm tms) tms')
          (a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms)
   substVarL   : {t : _} -> (ctx : List sig.T) -> {ctx' : _} -> (i : Elem t ctx')
     -> (tms : (\t => a.U t ctx) ^ ctx')
-    -> relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
+    -> equivalence.relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
   substVarR   : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
-    -> relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
+    -> equivalence.relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
   -- sem, var and subst are compatible
   substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
-    -> relation (t, ctx)
+    -> equivalence.relation (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
          (a.sem ctx op $
           map (\ty, tm =>
@@ -126,44 +124,39 @@ record Algebra (0 sig : Signature) where
   algebra    : IsAlgebra sig raw
 
 public export 0
-(.relation) : (0 a : Algebra sig) -> IRel (uncurry a.raw.U)
-(.relation) a = a.algebra.relation
+(.relation) : (0 a : Algebra sig) -> (ty : _) -> Rel (uncurry a.raw.U ty)
+(.relation) a = a.algebra.equivalence.relation
 
 public export
-(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T))
-(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid (Pair sig.T (List sig.T))
+(.setoid) a = MkIndexedSetoid (uncurry a.raw.U) a.algebra.equivalence
 
 public export
-(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> ISetoid sig.T
-(.setoidAt) a ctx = MkISetoid
-  (flip a.raw.U ctx)
-  (\t => a.relation (t, ctx))
-  (\_ => a.algebra.equivalence _)
+(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> IndexedSetoid sig.T
+(.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
 
 public export
-(.varFunc) : (a : Algebra sig) -> (ctx : _) -> IFunction (isetoid (flip Elem ctx)) (a.setoidAt ctx)
-(.varFunc) a ctx = MkIFunction
-  (\_ => a.raw.var)
-  (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
+(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
+(.varFunc) a ctx = mate (\_ => a.raw.var)
 
 public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func       : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
-  cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
-    -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm')
+  func       : a.setoid ~> b.setoid
   renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
-    -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm)
+    -> b.relation (t, ctx')
+         (func.H (t, ctx') $ a.raw.rename t g tm)
+         (b.raw.rename t g $ func.H (t, ctx) tm)
   semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.relation (t, ctx)
-         (func t ctx $ a.raw.sem ctx op tms)
-         (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms)
+         (func.H (t, ctx) $ a.raw.sem ctx op tms)
+         (b.raw.sem ctx op $ map (\ty => func.H (snd ty, fst ty ++ ctx)) tms)
   varHomo    : {t : _} -> {ctx : _} -> (i : Elem t ctx)
-    -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i)
+    -> b.relation (t, ctx) (func.H (t, ctx) $ a.raw.var i) (b.raw.var i)
   substHomo  : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
     -> (tms : (\t => a.raw.U t ctx) ^ ctx')
     -> b.relation (t, ctx)
-         (func t ctx $ a.raw.subst t ctx tm tms)
-         (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms)
+         (func.H (t, ctx) $ a.raw.subst t ctx tm tms)
+         (b.raw.subst t ctx (func.H (t, ctx') tm) $ map (\t => func.H (t, ctx)) tms)
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 30bcd91..bb3d24b 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -1,7 +1,6 @@
 module Soat.SecondOrder.Algebra.Lift
 
 import Data.List.Elem
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 
 import Soat.Data.Product
@@ -14,37 +13,40 @@ import Soat.SecondOrder.Signature.Lift
 import Syntax.PreorderReasoning.Setoid
 
 %default total
+%ambiguity_depth 4
 
 public export
 project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
   -> FirstOrder.Algebra.RawAlgebra sig
 project a ctx = MkRawAlgebra
-  (flip a.U ctx)
+  (\t => a.U t ctx)
   (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
 
 public export
-projectIsAlgebra : IsAlgebra (lift sig) a -> (ctx : List sig.T) -> IsAlgebra sig (project a ctx)
-projectIsAlgebra a ctx = MkIsAlgebra
-  (\t => a.relation (t, ctx))
-  (\t => a.equivalence (t, ctx))
-  (\op => a.semCong ctx _ . wrapIntro)
-
-public export
 projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
-projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra sig a ctx = MkAlgebra
+  { raw = project a.raw ctx
+  , algebra = MkIsAlgebra
+    { equivalence = (reindex (flip MkPair ctx) a.setoid).equivalence
+    , semCong     = \op => a.algebra.semCong ctx (MkOp (Op op.op)) . wrapIntro
+    }
+  }
 
 public export
 projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b
   -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
 projectHomo f ctx = MkHomomorphism
-  { func    = \t => f.func t ctx
-  , cong    = \t => f.cong t ctx
-  , semHomo = \op, tms => CalcWith (b.setoid.index _) $
-    |~ f.func _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
-    ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f.func ctx) (wrap (MkPair []) tms))
+  { func    = MkIndexedSetoidHomomorphism
+    { H           = \t => f.func.H (t, ctx)
+    , homomorphic = \t => f.func.homomorphic (t, ctx)
+    }
+  , semHomo = \op, tms => CalcWith (index b.setoid _) $
+    |~ f.func.H (_, ctx) (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
+    ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (\ty => f.func.H (snd ty, fst ty ++ ctx)) (wrap (MkPair []) tms))
       ...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
-    ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func t ctx) tms))
-      .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f.func ctx} tms)
+    ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func.H (t, ctx)) tms))
+      .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $
+          mapWrap (MkPair []) {f = \ty => f.func.H (snd ty, fst ty ++ ctx)} tms)
   }
 
 public export
@@ -52,23 +54,30 @@ public export
   -> (f : ctx `Sublist` ctx')
   -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
 (.renameHomo) a f = MkHomomorphism
-  { func    = \t => a.raw.rename t f
-  , cong    = \t => a.algebra.renameCong t f
-  , semHomo = \op, tms => CalcWith (a.setoid.index _) $
+  { func    = MkIndexedSetoidHomomorphism
+    { H           = \t => a.raw.rename t f
+    , homomorphic = \t, _, _ => a.algebra.renameCong t f
+    }
+  , semHomo = \op, tms => CalcWith (index a.setoid _) $
     |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms))
     ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms))
       ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
     ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
       ...(a.algebra.semCong _ (MkOp (Op op.op)) $
-          CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $
+          CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $
           |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
           ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
             .=.(mapWrap (MkPair []) tms)
           ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms)
-            .=.(cong (wrap (MkPair [])) $
-                pwEqImpliesEqual $
-                mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $
-                equalImpliesPwEq Refl))
+            ...(wrapIntro $
+                mapIntro'' (\t, tm, tm', eq =>
+                  CalcWith (index a.setoid (t, _)) $
+                  |~ a.raw.rename t (reflexive {x = []} ++ f) tm
+                  ~~ a.raw.rename t f tm
+                    .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f)
+                  ~~ a.raw.rename t f tm'
+                    ...(a.algebra.renameCong t f eq)) $
+                (pwSetoid (a.setoidAt ctx)).equivalence.reflexive _ tms))
   }
 
 public export
@@ -76,17 +85,19 @@ public export
   -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
   -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
 (.substHomo1) a ctx tms = MkHomomorphism
-  { func    = \t, tm => a.raw.subst t ctx tm tms
-  , cong    = \t, eq =>
-    a.algebra.substCong t ctx eq $
-    pwRefl (\_ => (a.algebra.equivalence _).refl)
-  , semHomo = \op, tms' => CalcWith (a.setoid.index _) $
+  { func    = MkIndexedSetoidHomomorphism
+    { H           = \t, tm => a.raw.subst t ctx tm tms
+    , homomorphic = \t, _, _, eq =>
+      a.algebra.substCong t ctx eq $
+      (pwSetoid (a.setoidAt _)).equivalence.reflexive _ tms
+    }
+  , semHomo = \op, tms' => CalcWith (index a.setoid _) $
     |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
     ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms'))
       ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
     ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
       ...(a.algebra.semCong ctx (MkOp (Op op.op)) $
-          CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
+          CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
           |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
           ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
             .=.(mapWrap (MkPair []) tms')
@@ -94,39 +105,42 @@ public export
             ...(wrapIntro $
                 mapIntro' (\t, eq =>
                   a.algebra.substCong t ctx eq $
-                  CalcWith (pwSetoid (a.setoidAt _) _) $
+                  CalcWith (index (pwSetoid (a.setoidAt _)) _) $
                   |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
-                  ~~ map (\t => a.raw.rename t reflexive) tms
-                    .=.(pwEqImpliesEqual $
-                        mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $
-                        equalImpliesPwEq Refl)
                   ~~ map (\t => id) tms
-                    ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $
-                        equalImpliesPwEq Refl)
+                    ...(mapIntro'' (\t, tm, tm', eq =>
+                          CalcWith (index a.setoid (t, ctx)) $
+                          |~ a.raw.rename t ([] {ys = []} ++ reflexive) tm
+                          ~~ a.raw.rename t reflexive tm
+                            .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry reflexive)
+                          ~~ tm
+                            ...(a.algebra.renameId t ctx tm)
+                          ~~ tm'
+                            ...(eq)) $
+                        (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _)
                   ~~ tms
                     .=.(mapId tms)) $
-                pwRefl (\t => (a.algebra.equivalence _).refl)))
+                (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _))
   }
 
-renameBodyFunc : (f : ctx `Sublist` ctx')
-  -> IFunction
-       (isetoid (flip Elem ctx))
-       (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid
-renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f))
+-- renameBodyFunc : (f : ctx `Sublist` ctx')
+--   -> irrelevantCast (flip Elem ctx) ~>
+--      (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx'))).setoid
+-- renameBodyFunc f = mate (\_ => Done . curry f)
 
-indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
-  -> IFunction
-       (isetoid (flip Elem ts))
-       (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid
-indexFunc tms = MkIFunction
-  (\_ => index tms)
-  (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms))
+-- indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
+--   -> irrelevantCast (flip Elem ts) ~>
+--      (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
+-- indexFunc tms = mate (\_ => index tms)
+
+freeAlg : List sig.T -> FirstOrder.Algebra.Algebra sig
+freeAlg ctx = FreeAlgebra (irrelevantCast (flip Elem ctx))
 
 public export
 Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
 Initial sig = MkRawAlgebra
-  (\t, ctx => Term sig (flip Elem ctx) t)
-  (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
+  (\t, ctx => (freeAlg ctx).raw.U t)
+  (\t, f => bindTerm {a = Free _} (\_ => Done . curry f))
   (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
   Done
   (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
@@ -134,29 +148,37 @@ Initial sig = MkRawAlgebra
 public export
 InitialIsAlgebra : (0 sig : _) -> SecondOrder.Algebra.IsAlgebra (lift sig) (Initial sig)
 InitialIsAlgebra sig = MkIsAlgebra
-  { relation    = \(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t
-  , equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t
-  , renameCong  = \t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)
-  , semCong     = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
+  { equivalence = MkIndexedEquivalence
+    { relation   = \(t, ctx) => (freeAlg ctx).relation t
+    , reflexive  = \(t, ctx) => (freeAlg ctx).algebra.equivalence.reflexive t
+    , symmetric  = \(t, ctx) => (freeAlg ctx).algebra.equivalence.symmetric t
+    , transitive = \(t, ctx) => (freeAlg ctx).algebra.equivalence.transitive t
+    }
+  , renameCong  = \t, f => bindTermCong
+    { a   = freeAlg _
+    , env = mate (\_ => Done . curry f)
+    }
+  , semCong     = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
   , substCong   = \_, _, eq, eqs => bindTermCong'
-    {a = FreeAlgebra (isetoid (flip Elem _))}
-    (\t, Refl => index eqs _)
-    eq
+    { a    = freeAlg _
+    , cong = \_, Refl => index eqs _
+    , eq
+    }
   , renameId    = \t, ctx, tm =>
-    tmRelSym (\_ => MkSymmetric symmetric) $
-    bindUnique (renameBodyFunc reflexive) id (\i => Done' $ sym $ curryUncurry id i) $
-    tm
+    (freeAlg _).setoid.equivalence.symmetric t _ _ $
+    bindUnique (mate (\_ => Done . curry reflexive)) id (\i => Done $ sym $ curryUncurry id i) tm
   , renameComp  = \t, f, g, tm =>
-    tmRelSym (\_ => MkSymmetric symmetric) $
+    (freeAlg _).setoid.equivalence.symmetric t _ _ $
     bindUnique
-      {a = FreeAlgebra (isetoid (flip Elem _))}
-      (renameBodyFunc (transitive g f))
-      (bindHomo (renameBodyFunc f) . bindHomo (renameBodyFunc g))
-      (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
-    tm
+      { a    = freeAlg _
+      , env  = mate (\_ => Done . curry (transitive g f))
+      , f    = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => Done . curry g))
+      , cong = \i => Done $ sym $ curryUncurry (curry f . curry g) i
+      , tm
+      }
   , semNat      = \f, (MkOp (Op op)), tms =>
-    Call' (MkOp op) $
-    CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+    Call (MkOp op) $
+    CalcWith (index (pwSetoid (freeAlg _).setoid) _) $
     |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
     ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
       .=.(bindTermsIsMap {a = Free _} _ _)
@@ -164,76 +186,78 @@ InitialIsAlgebra sig = MkIsAlgebra
       ..<(mapIntro' (\t =>
             bindTermCong'
               {rel = \_ => Equal}
-              {a = FreeAlgebra (isetoid (flip Elem _))}
-              (\_, Refl => Done' $ curryUncurry (curry f) _)) $
-          tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms))
+              {a = freeAlg _}
+              (\_, Refl => Done $ curryUncurry (curry f) _)) $
+          (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
     ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms)
       .=.(mapUnwrap (MkPair []) tms)
-  , varNat      = \_, _ => Done' Refl
-  , substNat    = \t, f, tm, tms =>
-    bindUnique
-      {a = FreeAlgebra (isetoid (flip Elem _))}
-      (indexFunc _)
-      (bindHomo (renameBodyFunc f) . bindHomo (indexFunc tms))
-      (\i =>
-        tmRelReflexive (\_ => MkReflexive reflexive) $
-        sym $
-        indexMap tms i)
-      tm
-  , substExnat  = \t, ctx, f, tm, tms =>
-    bindUnique
-      {a = FreeAlgebra (isetoid (flip Elem _))}
-      (indexFunc _)
-      (bindHomo (indexFunc tms) . bindHomo (renameBodyFunc f))
-      (\i =>
-        tmRelReflexive (\_ => MkReflexive reflexive) $
-        sym $
-        indexShuffle f i)
-      tm
-  , substComm   = \t, ctx, tm, tms, tms' =>
-    bindUnique
-      {a = FreeAlgebra (isetoid (flip Elem _))}
-      (indexFunc _)
-      (bindHomo (indexFunc tms') . bindHomo (indexFunc tms))
-      (\i =>
-        tmRelReflexive (\_ => MkReflexive reflexive) $
-        sym $
-        indexMap tms i)
-      tm
-  , substVarL   = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
+  , varNat      = \_, _ => Done Refl
+  , substNat    = \t, f, tm, tms => bindUnique
+    { a = freeAlg _
+    , env = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) tms)
+    , f   = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => index tms))
+    , cong = \i =>
+      reflect (index (freeAlg _).setoid _) $
+      sym $
+      indexMap tms i
+    , tm
+    }
+  , substExnat  = \t, ctx, f, tm, tms => bindUnique
+    { a    = freeAlg _
+    , env  = mate (\_ => index $ shuffle f tms)
+    , f    = bindHomo (mate (\_ => index tms)) . bindHomo (mate (\_ => Done . curry f))
+    , cong = \i =>
+      reflect (index (freeAlg _).setoid _) $
+      sym $
+      indexShuffle f i
+    , tm
+    }
+  , substComm   = \t, ctx, tm, tms, tms' => bindUnique
+    { a    = freeAlg _
+    , env  = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => index tms')) tms)
+    , f    = bindHomo (mate (\_ => index tms')) . bindHomo (mate (\_ => index tms))
+    , cong = \i =>
+      reflect (index (freeAlg _).setoid _) $
+      sym $
+      indexMap tms i
+    , tm
+    }
+  , substVarL   = \_, _, _ => (freeAlg _).setoid.equivalence.reflexive _ _
   , substVarR   = \t, ctx, tm =>
-    tmRelSym (\_ => MkSymmetric symmetric) $
+    (freeAlg _).setoid.equivalence.symmetric t _ _ $
     bindUnique
-      {a = FreeAlgebra (isetoid (flip Elem _))}
-      (indexFunc _)
-      id
-      (\i =>
-        tmRelReflexive (\_ => MkReflexive reflexive) $
+      { v    = irrelevantCast (flip Elem ctx)
+      , a    = freeAlg ctx
+      , env  = mate (\_ => index $ tabulate (Done {sig = sig, v = flip Elem ctx}))
+      , f    = id
+      , cong = \i =>
+        reflect (index (freeAlg ctx).setoid _) $
         sym $
-        indexTabulate Done i)
-      tm
+        indexTabulate Done i
+      , tm
+      }
   , substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
-    Call' (MkOp op) $
-    CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+    Call (MkOp op) $
+    CalcWith (index (pwSetoid (freeAlg _).setoid) _) $
     |~ bindTerms {a = Free _} (\_ => index tms') (unwrap (MkPair []) tms)
     ~~ map (\_ => bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms)
       .=.(bindTermsIsMap {a = Free _} _ _)
     ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms)
       ..<(mapIntro' (\t => bindTermCong'
             {rel = \_ => Equal}
-            {a = FreeAlgebra (isetoid (flip Elem _))}
-            (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $
+            {a = freeAlg _}
+            (\t, Refl => CalcWith (index (freeAlg _).setoid _) $
               |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _
               ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _)
                 .=.(indexMap tms' _)
               ~~ index tms' _
                 ..<(bindUnique
-                      (renameBodyFunc ([] {ys = []} ++ reflexive))
-                      id
-                      (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
-                      (index tms' _)))) $
-          tmsRelRefl (\_ => MkReflexive reflexive) $
-          unwrap (MkPair []) tms)
+                      { env  = mate (\_ => Done . curry ([] {ys = []} ++ reflexive))
+                      , f    = id
+                      , cong = \i => Done $ sym $ trans (curryUncurry _ i) (curryUncurry id i)
+                      , tm   = index tms' _
+                      }))) $
+          (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
     ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
       .=.(mapUnwrap (MkPair []) tms)
   }
@@ -244,15 +268,18 @@ InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig)
 
 public export
 freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
-  -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
+  -> FreeAlgebra (irrelevantCast (flip Elem ctx)) ~>
+     projectAlgebra sig (InitialAlgebra sig) ctx
 freeToInitialHomo sig ctx = MkHomomorphism
-  { func    = \_ => id
-  , cong    = \_ => id
+  { func    = MkIndexedSetoidHomomorphism
+    { H           = \_ => id
+    , homomorphic = \_, _, _ => id
+    }
   , semHomo = \(MkOp op), tms =>
-    Call' (MkOp op) $
-    tmsRelSym (\_ => MkSymmetric symmetric) $
-    tmsRelReflexive (\_ => MkReflexive reflexive) $
-    transitive (unwrapWrap _ _) (mapId tms)
+    Call (MkOp op) $
+    reflect (index (pwSetoid ((InitialAlgebra sig).setoidAt ctx)) _) $
+    sym $
+    trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId tms)
   }
 
 public export
@@ -263,31 +290,33 @@ fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
 public export
 fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a
 fromInitialHomo a = MkHomomorphism
-  { func       = fromInitial a.raw
-  , cong       = \t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)
+  { func       = MkIndexedSetoidHomomorphism
+    { H           = \(t, ctx) => fromInitial a.raw t ctx
+    , homomorphic = \(t, ctx), _, _ => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)
+    }
   , renameHomo = \t, f => bindUnique'
-    {v = isetoid (flip Elem _)}
+    {v = irrelevantCast (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (bindHomo (a.varFunc _) . bindHomo (renameBodyFunc f))
+    (bindHomo (a.varFunc _) . bindHomo (mate (\_ => Done . curry f)))
     (a.renameHomo f . bindHomo (a.varFunc _))
-    (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)
+    (\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i)
   , semHomo    = \ctx, (MkOp (Op op)), tms =>
     a.algebra.semCong ctx (MkOp (Op op)) $
-    CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
+    CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
     |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) (unwrap (MkPair []) tms))
     ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms))
       .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _)
-    ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms))
+    ~~ wrap (MkPair []) (unwrap (MkPair []) (map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms))
       .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms)
-    ~~ map (extendFunc (fromInitial a.raw) ctx) tms
+    ~~ map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms
       .=.(wrapUnwrap _)
-  , varHomo    = \_ => (a.algebra.equivalence _).reflexive
+  , varHomo    = \i => a.algebra.equivalence.reflexive _ $ a.raw.var i
   , substHomo  = \t, ctx, tm, tms => bindUnique'
-    {v = isetoid (flip Elem _)}
+    {v = irrelevantCast (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (bindHomo (a.varFunc _) . bindHomo (indexFunc tms))
+    (bindHomo (a.varFunc _) . bindHomo (mate (\_ => index tms)))
     (a.substHomo1 ctx _ . bindHomo (a.varFunc _))
-    (\i => CalcWith (a.setoid.index _) $
+    (\i => CalcWith (index a.setoid _) $
         |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) (index tms i)
         ~~ index (map (\_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i
           .=<(indexMap {f = \_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i)
@@ -300,9 +329,9 @@ public export
 fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
   -> (f : InitialAlgebra sig ~> a)
   -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
-  -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
+  -> a.relation (t, ctx) (f.func.H (t, ctx) tm) (fromInitial a.raw t ctx tm)
 fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
-  {v = isetoid (flip Elem _)}
+  {v = irrelevantCast (flip Elem _)}
   {a = projectAlgebra sig a ctx}
   (a.varFunc ctx)
   (projectHomo f ctx . freeToInitialHomo sig ctx)
diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
deleted file mode 100644
index f0480b2..0000000
--- a/src/Syntax/PreorderReasoning/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-{- Taken from https://github.com/ohad/idris-setoid -}
-
-||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
-module Syntax.PreorderReasoning.Setoid
-
-import public Data.Setoid
-
-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.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.relation x y
-CalcWith a (|~ x) = a.equivalence.reflexive
-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.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.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))
-
-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))