diff options
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 16 |
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) |