Move IsAlgebra relation from type to body.

1 files changed, 25 insertions, 21 deletions

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))