Lift index of varFunc.

2 files changed, 24 insertions, 42 deletions

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index e52c945..038e065 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -155,8 +155,8 @@ public export
   }
 
 public export
-(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
-(.varFunc) a ctx = mate (\_ => a.raw.var)
+(.varFunc) : (a : Algebra sig) -> irrelevantCast (uncurry Elem) ~> a.setoid
+(.varFunc) a = mate (\(_, _) => a.raw.var)
 
 public export
 (.substFunc) : (a : Algebra sig) -> (t : _) -> (ctx, ctx' : _)
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 8bbcf9e..4053748 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -4,6 +4,7 @@ import Data.List.Elem
 import Data.List.Sublist
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Pair
 import Data.Setoid.Product
 
 import Soat.FirstOrder.Algebra
@@ -36,10 +37,7 @@ 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    = MkIndexedSetoidHomomorphism
-    { H           = \t => f.func.H (t, ctx)
-    , homomorphic = \t => f.func.homomorphic (t, ctx)
-    }
+  { func    = reindex (flip MkPair ctx) f.func
   , 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))
@@ -54,10 +52,7 @@ public export
   -> (f : ctx `Sublist` ctx')
   -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
 (.renameHomo) a f = MkHomomorphism
-  { func    = MkIndexedSetoidHomomorphism
-    { H           = \t => a.raw.rename t f
-    , homomorphic = \t, _, _ => a.algebra.renameCong t f
-    }
+  { func    = a.renameFunc 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))
@@ -85,12 +80,11 @@ 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    = MkIndexedSetoidHomomorphism
-    { H           = \t, tm => a.raw.subst t ctx tm tms
-    , homomorphic = \t, _, _, eq =>
-      a.algebra.substCong t ctx eq $
-      (Product (a.setoidAt _)).equivalence.reflexive _ tms
-    }
+  { func    = bundle (\t =>
+    a.substFunc t ctx ctx' .
+    tuple
+      (id (index a.setoid (t, ctx')))
+      (const {b = index (Product (a.setoidAt ctx)) ctx'} 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'))
@@ -123,16 +117,7 @@ public export
                 (Product (a.setoidAt _)).equivalence.reflexive _ _))
   }
 
--- 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)
---   -> irrelevantCast (flip Elem ts) ~>
---      (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
--- indexFunc tms = mate (\_ => index tms)
-
+public export
 freeAlg : List sig.T -> FirstOrder.Algebra.Algebra sig
 freeAlg ctx = FreeAlgebra (irrelevantCast (flip Elem ctx))
 
@@ -283,39 +268,36 @@ freeToInitialHomo sig ctx = MkHomomorphism
   }
 
 public export
-fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T)
-  -> (Initial sig).U t ctx -> a.U t ctx
-fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
+fromInitial : (a : Algebra (lift sig)) -> (InitialAlgebra sig).setoid ~> a.setoid
+fromInitial a = bundle (\(t, ctx) =>
+  index (bindFunc {a = projectAlgebra sig a ctx} (reindex (flip MkPair ctx) a.varFunc)) t)
 
 public export
 fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a
 fromInitialHomo a = MkHomomorphism
-  { func       = MkIndexedSetoidHomomorphism
-    { H           = \(t, ctx) => fromInitial a.raw t ctx
-    , homomorphic = \(t, ctx), _, _ => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)
-    }
+  { func       = fromInitial a
   , renameHomo = \t, f => bindUnique'
     {v = irrelevantCast (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (bindHomo (a.varFunc _) . bindHomo (mate (\_ => Done . curry f)))
-    (a.renameHomo f . bindHomo (a.varFunc _))
+    (bindHomo (reindex (flip MkPair _) a.varFunc) . bindHomo (mate (\_ => Done . curry f)))
+    (a.renameHomo f . bindHomo (reindex (flip MkPair _) a.varFunc))
     (\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i)
   , semHomo    = \ctx, (MkOp (Op op)), tms =>
     a.algebra.semCong ctx (MkOp (Op op)) $
     CalcWith (index (Product (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))
+    ~~ wrap (MkPair []) (map (\t => (fromInitial a).H (t, ctx)) (unwrap (MkPair []) tms))
       .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _)
-    ~~ wrap (MkPair []) (unwrap (MkPair []) (map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms))
+    ~~ wrap (MkPair []) (unwrap (MkPair []) (map (\ty => (fromInitial a).H (snd ty, fst ty ++ ctx)) tms))
       .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms)
-    ~~ map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms
+    ~~ map (\ty => (fromInitial a).H (snd ty, fst ty ++ ctx)) tms
       .=.(wrapUnwrap _)
   , varHomo    = \i => a.algebra.equivalence.reflexive _ $ a.raw.var i
   , substHomo  = \t, ctx, tm, tms => bindUnique'
     {v = irrelevantCast (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (bindHomo (a.varFunc _) . bindHomo (mate (\_ => index tms)))
-    (a.substHomo1 ctx _ . bindHomo (a.varFunc _))
+    (bindHomo (reindex (flip MkPair _) a.varFunc) . bindHomo (mate (\_ => index tms)))
+    (a.substHomo1 ctx _ . bindHomo (reindex (flip MkPair _) a.varFunc))
     (\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
@@ -329,10 +311,10 @@ 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.H (t, ctx) tm) (fromInitial a.raw t ctx tm)
+  -> a.relation (t, ctx) (f.func.H (t, ctx) tm) ((fromInitial a).H (t, ctx) tm)
 fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
   {v = irrelevantCast (flip Elem _)}
   {a = projectAlgebra sig a ctx}
-  (a.varFunc ctx)
+  (reindex (flip MkPair ctx) a.varFunc)
   (projectHomo f ctx . freeToInitialHomo sig ctx)
   f.varHomo