refactor: expand flip in most places.

1 files changed, 8 insertions, 8 deletions

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 9f9719e..9e1ef91 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -29,7 +29,7 @@ record RawAlgebra (0 sig : Signature) where
   sem    : sig `algebraOver` U
   var    : forall t, ctx . (i : Elem t ctx) -> U t ctx
   subst  : (t : sig.T) -> (ctx : List sig.T)
-    -> forall ctx' . U t ctx' -> flip U ctx ^ ctx' -> U t ctx
+    -> 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
@@ -45,7 +45,7 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
     -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
   substCong   : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx' . {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
-    -> {tms, tms' : flip a.U ctx ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
+    -> {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')
   -- rename is functorial
   renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
@@ -67,30 +67,30 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
     -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
   -- subst is natural transformation
   substNat    : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
-    -> forall ctx'' . (tm : a.U t ctx'') -> (tms : flip a.U ctx ^ ctx'')
+    -> forall ctx'' . (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'')
     -> rel (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)
     -> forall ctx', ctx'' . (f : ctx' `Sublist` ctx'')
-    -> (tm : a.U t ctx') -> (tms : flip a.U ctx ^ 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))
   -- var, subst is a monoid
   substComm   : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx', ctx'' . (tm : a.U t ctx'')
-    -> (tms : flip a.U ctx' ^ ctx'') -> (tms' : flip a.U ctx ^ ctx')
+    -> (tms : (\t => a.U t ctx') ^ ctx'') -> (tms' : (\t => a.U t ctx) ^ ctx')
     -> rel (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   : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
-    -> (tms : flip a.U ctx ^ ctx')
+    -> (tms : (\t => a.U t ctx) ^ ctx')
     -> rel (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
   -- sem, var and subst are compatible
   substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-    -> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : flip a.U ctx ^ ctx')
+    -> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
          (a.sem ctx op $
@@ -142,7 +142,7 @@ record IsHomomorphism
   varHomo    : forall t, ctx . (i : Elem t ctx)
     -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
   substHomo  : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
-    -> (tms : flip a.raw.U ctx ^ ctx')
+    -> (tms : (\t => a.raw.U t ctx) ^ ctx')
     -> b.relation (t, ctx)
          (f t ctx $ a.raw.subst t ctx tm tms)
          (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)