summaryrefslogtreecommitdiff
path: root/src/Soat/SecondOrder/Algebra.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/SecondOrder/Algebra.idr')
-rw-r--r--src/Soat/SecondOrder/Algebra.idr93
1 files changed, 43 insertions, 50 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 6f7cb4a..06d8674 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -1,6 +1,5 @@
module Soat.SecondOrder.Algebra
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Data.List.Elem
@@ -15,15 +14,10 @@ extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type
extend x ctx ty = x (snd ty) (fst ty ++ ctx)
public export
-extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U))
- -> (ctx : List a) -> IRel (extend U ctx)
+extendRel : {U : a -> List a -> Type} -> (rel : (ty : _) -> Rel (uncurry U ty))
+ -> (ctx : List a) -> (ty : _) -> Rel (extend U ctx ty)
extendRel rel ctx ty = rel (snd ty, fst ty ++ ctx)
-public export
-extendFunc : {0 U, V : a -> List a -> Type} -> (f : (t : a) -> IFunc (U t) (V t)) -> (ctx : List a)
- -> IFunc (extend U ctx) (extend V ctx)
-extendFunc f ctx ty = f (snd ty) (fst ty ++ ctx)
-
public export 0
algebraOver : (sig : Signature) -> (U : sig.T -> List sig.T -> Type) -> Type
algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
@@ -41,7 +35,7 @@ record RawAlgebra (0 sig : Signature) where
public export
(.extendSubst) : (a : RawAlgebra sig) -> (ctx : List sig.T) -> {ctx' : List sig.T}
- -> (tms : (\t => a.U t ctx) ^ ctx') -> IFunc (extend a.U ctx') (extend a.U ctx)
+ -> (tms : (\t => a.U t ctx) ^ ctx') -> (ty : _) -> extend a.U ctx' ty -> extend a.U ctx ty
a .extendSubst ctx tms ty tm = a.subst
(snd ty)
(fst ty ++ ctx)
@@ -52,65 +46,69 @@ a .extendSubst ctx tms ty tm = a.subst
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
- 0 relation : IRel (uncurry a.U)
- equivalence : IEquivalence (uncurry a.U) relation
+ equivalence : IndexedEquivalence _ (uncurry a.U)
-- Congruences
renameCong : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
- -> {tm, tm' : a.U t ctx} -> relation (t, ctx) tm tm'
- -> relation (t, ctx') (a.rename t f tm) (a.rename t f tm')
+ -> {tm, tm' : a.U t ctx} -> equivalence.relation (t, ctx) tm tm'
+ -> equivalence.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} relation ctx) tms tms'
- -> relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
+ -> Pointwise (extendRel {U = a.U} equivalence.relation ctx) tms tms'
+ -> equivalence.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'} -> 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')
+ -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> equivalence.relation (t, ctx') tm tm'
+ -> {tms, tms' : (\t => a.U t ctx) ^ ctx'}
+ -> Pointwise (\t => equivalence.relation (t, ctx)) tms tms'
+ -> equivalence.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)
- -> relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
+ -> equivalence.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)
- -> relation (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
+ -> equivalence.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)
- -> relation (t, ctx')
+ -> equivalence.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)
- -> relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
+ -> equivalence.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'')
- -> relation (t, ctx')
+ -> equivalence.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'')
- -> relation (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
+ -> equivalence.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')
- -> relation (t, ctx)
+ -> equivalence.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')
- -> relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
+ -> equivalence.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)
- -> relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
+ -> equivalence.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')
- -> relation (t, ctx)
+ -> equivalence.relation (t, ctx)
(a.subst t ctx (a.sem ctx' op tms) tms')
(a.sem ctx op $
map (\ty, tm =>
@@ -126,44 +124,39 @@ record Algebra (0 sig : Signature) where
algebra : IsAlgebra sig raw
public export 0
-(.relation) : (0 a : Algebra sig) -> IRel (uncurry a.raw.U)
-(.relation) a = a.algebra.relation
+(.relation) : (0 a : Algebra sig) -> (ty : _) -> Rel (uncurry a.raw.U ty)
+(.relation) a = a.algebra.equivalence.relation
public export
-(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T))
-(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid (Pair sig.T (List sig.T))
+(.setoid) a = MkIndexedSetoid (uncurry a.raw.U) a.algebra.equivalence
public export
-(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> ISetoid sig.T
-(.setoidAt) a ctx = MkISetoid
- (flip a.raw.U ctx)
- (\t => a.relation (t, ctx))
- (\_ => a.algebra.equivalence _)
+(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> IndexedSetoid sig.T
+(.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
public export
-(.varFunc) : (a : Algebra sig) -> (ctx : _) -> IFunction (isetoid (flip Elem ctx)) (a.setoidAt ctx)
-(.varFunc) a ctx = MkIFunction
- (\_ => a.raw.var)
- (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
+(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
+(.varFunc) a ctx = mate (\_ => a.raw.var)
public export
record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
- cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
- -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm')
+ func : a.setoid ~> b.setoid
renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
- -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm)
+ -> b.relation (t, ctx')
+ (func.H (t, ctx') $ a.raw.rename t g tm)
+ (b.raw.rename t g $ func.H (t, ctx) tm)
semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.raw.U ctx ^ op.arity)
-> b.relation (t, ctx)
- (func t ctx $ a.raw.sem ctx op tms)
- (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms)
+ (func.H (t, ctx) $ a.raw.sem ctx op tms)
+ (b.raw.sem ctx op $ map (\ty => func.H (snd ty, fst ty ++ ctx)) tms)
varHomo : {t : _} -> {ctx : _} -> (i : Elem t ctx)
- -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i)
+ -> b.relation (t, ctx) (func.H (t, ctx) $ a.raw.var i) (b.raw.var i)
substHomo : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
-> (tms : (\t => a.raw.U t ctx) ^ ctx')
-> b.relation (t, ctx)
- (func t ctx $ a.raw.subst t ctx tm tms)
- (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms)
+ (func.H (t, ctx) $ a.raw.subst t ctx tm tms)
+ (b.raw.subst t ctx (func.H (t, ctx') tm) $ map (\t => func.H (t, ctx)) tms)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:12:57 +0000