Move IsAlgebra relation from type to body.

5 files changed, 50 insertions, 43 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index f0b23ea..6f9389b 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -25,18 +25,22 @@ record RawSetoidAlgebra (0 sig : Signature) where
   0 relation : IRel raw.U
 
 public export
-record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  equivalence : IEquivalence a.U rel
+  0 relation  : IRel a.U
+  equivalence : IEquivalence a.U relation
   semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-    -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
+    -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms')
 
 public export
 record Algebra (0 sig : Signature) where
   constructor MkAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel raw.U
-  algebra    : IsAlgebra sig raw relation
+  algebra    : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> IRel a.raw.U
+(.relation) a = a.algebra.relation
 
 public export
 (.setoid) : Algebra sig -> ISetoid sig.T
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 736dc75..29a740f 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -73,11 +73,14 @@ Coproduct x y = MkRawAlgebra
   }
 
 public export
-CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
+CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y
   -> IsAlgebra sig (Coproduct x y)
-       ((~=~) (MkRawSetoidAlgebra x rel) (MkRawSetoidAlgebra y rel'))
 CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
-  { equivalence = \t => MkEquivalence
+  { 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)
@@ -90,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
 
 public export
 CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra
+CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
 
 public export
 injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index eaa2da2..45282cc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -130,12 +130,12 @@ 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) ((~=~) v.relation)
-FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
+FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U)
+FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call'
 
 public export
 FreeAlgebra : ISetoid sig.T -> Algebra sig
-FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
+FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
 
 public export
 bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 664a5d7..475bdc0 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -33,66 +33,67 @@ record RawAlgebra (0 sig : Signature) where
     -> forall ctx' . U t ctx' -> (\t => U t ctx) ^ ctx' -> U t ctx
 
 public export
-record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  equivalence : IEquivalence (uncurry a.U) rel
+  0 relation  : IRel (uncurry a.U)
+  equivalence : IEquivalence (uncurry a.U) relation
   -- Congruences
   renameCong  : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-    -> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm'
-    -> rel (t, ctx') (a.rename t f tm) (a.rename t f tm')
+    -> {tm, tm' : a.U t ctx} -> relation (t, ctx) tm tm'
+    -> 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} rel ctx) tms tms'
-    -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
+    -> Pointwise (extendRel {U = a.U} relation ctx) tms tms'
+    -> 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'} -> rel (t, ctx') tm tm'
-    -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
-    -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
+    -> {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')
   -- rename is functorial
   renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
-    -> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
+    -> 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)
-    -> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
+    -> 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)
-    -> rel (t, ctx')
+    -> 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)
-    -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
+    -> 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'')
-    -> rel (t, ctx')
+    -> 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'')
-    -> rel (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
+    -> 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')
-    -> rel (t, ctx)
+    -> 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')
-    -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
+    -> 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)
-    -> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
+    -> 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')
-    -> rel (t, ctx)
+    -> relation (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
          (a.sem ctx op $
           map (\ty, tm =>
@@ -105,8 +106,11 @@ public export
 record Algebra (0 sig : Signature) where
   constructor MkAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel (uncurry raw.U)
-  algebra    : IsAlgebra sig raw relation
+  algebra    : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> IRel (uncurry a.raw.U)
+(.relation) a = a.algebra.relation
 
 public export
 (.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T))
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 5be7dd1..5f52f82 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -21,17 +21,16 @@ project a ctx = MkRawAlgebra
   (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
 
 public export
-projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel
-  -> (ctx : List sig.T)
-  -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx))
+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 : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
   -> FirstOrder.Algebra.Algebra sig
-projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
 
 public export
 projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
@@ -141,12 +140,9 @@ Initial sig = MkRawAlgebra
   (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
 
 public export
-InitialIsAlgebra : (0 sig : _)
-  -> SecondOrder.Algebra.IsAlgebra
-       (lift sig)
-       (Initial sig)
-       (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t)
+InitialIsAlgebra : (0 sig : _) -> SecondOrder.Algebra.IsAlgebra (lift sig) (Initial sig)
 InitialIsAlgebra sig = MkIsAlgebra
+  (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t)
   (\(t, ctx) => tmRelEq (\_ => equiv) t)
   (\t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f))
   (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
@@ -273,7 +269,7 @@ InitialIsAlgebra sig = MkIsAlgebra
 
 public export
 InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
-InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig)
+InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig)
 
 public export
 freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)