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.idr99
1 files changed, 56 insertions, 43 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index c506c85..5dd53c5 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
@@ -13,11 +12,17 @@ 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 : {0 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) -> (ctx : List a) -> U t ctx -> V t ctx)
+ -> (ctx : List a) -> (ty : Pair (List a) a) -> extend U ctx ty -> extend V ctx ty
+extendFunc f ctx ty = f (snd ty) (fst ty ++ ctx)
+
+public export
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)
-> extend x ctx ^ op.arity -> x t ctx
@@ -30,100 +35,108 @@ 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' -> (\t => U t ctx) ^ ctx' -> U t ctx
+ -> forall ctx' . (tm : U t ctx') -> (tms : (\t => U t ctx) ^ ctx') -> U t ctx
+
+public export
+(.extendSubst) : (a : RawAlgebra sig) -> (ctx : _) -> {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)
+ tm
+ (tabulate {is = fst ty} (a.var . elemJoinL {ys = ctx}) ++
+ map (\t => a.rename t ([] {ys = fst ty} ++ reflexive {x = ctx})) tms)
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
+ equivalence : IndexedEquivalence (Pair sig.T (List sig.T)) (uncurry a.U)
-- 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} -> 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} rel ctx) tms tms'
- -> rel (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'} -> 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'} -> 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)
- -> rel (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)
- -> rel (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)
- -> rel (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)
- -> rel (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'')
- -> rel (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'')
- -> rel (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')
- -> rel (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')
- -> rel (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)
- -> rel (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')
- -> rel (t, ctx)
+ -> equivalence.relation (t, ctx)
(a.subst t ctx (a.sem ctx' op tms) tms')
- (a.sem ctx op $
- map (\ty, tm =>
- a.subst (snd ty) (fst ty ++ ctx) tm
- (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++
- map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms')) $
- tms)
+ (a.sem ctx op $ map (a.extendSubst ctx tms') tms)
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) -> (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 : _) -> cast (flip Elem ctx) ~> a.setoidAt ctx
+(.varFunc) a ctx = mate (\_ => a.raw.var)
public export
record IsHomomorphism
@@ -139,7 +152,7 @@ record IsHomomorphism
-> (tms : extend a.raw.U ctx ^ op.arity)
-> b.relation (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)
+ (b.raw.sem ctx op $ map (extendFunc f ctx) tms)
varHomo : {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) -> {ctx' : _} -> (tm : a.raw.U t ctx')
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:34:14 +0000