Migrate to use idris-setoid library.

2 files changed, 217 insertions, 195 deletions

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)