diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index 3ce1726..bc3defb 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -34,28 +34,28 @@ record RawAlgebra (0 sig : Signature) where public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where constructor MkIsAlgebra - 0 equivalence : IEquivalence (uncurry a.U) rel + equivalence : IEquivalence (uncurry a.U) rel -- Congruences - 0 renameCong : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') + renameCong : (t : sig.T) -> forall 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') - 0 semCong : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + 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') - 0 substCong : (t : sig.T) -> (ctx : List sig.T) + 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' -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms') -- rename is functorial - 0 renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) + 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 - 0 renameComp : (t : sig.T) + renameComp : (t : sig.T) -> forall 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) -- sem are natural transformation - 0 semNat : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t) + semNat : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t) -> (tms : extend a.U ctx ^ op.arity) -> rel (t, ctx') (a.rename t f $ a.sem ctx op tms) @@ -63,33 +63,33 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $ tms) -- var is natural transformation - 0 varNat : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx) + varNat : forall 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) -- subst is natural transformation - 0 substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') + substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') -> forall ctx'' . (tm : a.U t ctx'') -> (tms : flip a.U 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 - 0 substExnat : (t : sig.T) -> (ctx : List sig.T) + 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'') -> 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 - 0 substComm : (t : sig.T) -> (ctx : List sig.T) + 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') -> 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) - 0 substVarL : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx') + substVarL : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx') -> (tms : flip a.U ctx ^ ctx') -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i) - 0 substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) + 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 - 0 substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + 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') -> rel (t, ctx) (a.subst t ctx (a.sem ctx' op tms) tms') @@ -117,18 +117,18 @@ record IsHomomorphism (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx) where constructor MkIsHomomorphism - 0 cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx} + cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx} -> a.rel (t, ctx) tm tm' -> b.rel (t, ctx) (f t ctx tm) (f t ctx tm') - 0 renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx) + renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx) -> b.rel (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm) - 0 semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) + semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> (tms : extend a.raw.U ctx ^ op.arity) -> b.rel (t, ctx) (f t ctx $ a.raw.sem ctx op tms) (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms) - 0 varHomo : forall t, ctx . (i : Elem t ctx) + varHomo : forall t, ctx . (i : Elem t ctx) -> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i) - 0 substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx') + substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx') -> (tms : flip a.raw.U ctx ^ ctx') -> b.rel (t, ctx) (f t ctx $ a.raw.subst t ctx tm tms) |