1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
module Soat.SecondOrder.Algebra
import Data.List.Elem
import Soat.Data.Product
import Soat.Data.Sublist
import Soat.Relation
import Soat.SecondOrder.Signature
public export
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 rel ctx ty = rel (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
public export
record RawAlgebra (0 sig : Signature) where
constructor MakeRawAlgebra
0 U : (t : sig.T) -> (ctx : List sig.T) -> Type
rename : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx'
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
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
constructor MkIsAlgebra
equivalence : IEquivalence (uncurry a.U) rel
-- Congruences
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')
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')
substCong : (t : sig.T) -> (ctx : List sig.T)
-> forall 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')
-- 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
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
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)
(a.sem ctx' op $
map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
tms)
-- var is natural transformation
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
substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` 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 : (\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 : (\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 : (\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' : (\t => a.U t ctx) ^ ctx')
-> rel (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)
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
raw : RawAlgebra sig
0 relation : IRel (uncurry raw.U)
algebra : IsAlgebra sig raw 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
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 _)
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)
public export
record IsHomomorphism
{0 sig : Signature} (a, b : Algebra sig)
(f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
where
constructor MkIsHomomorphism
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) (f t ctx tm) (f t ctx tm')
renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
-> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f 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)
(f t ctx $ a.raw.sem ctx op tms)
(b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
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 : (\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)
public export
record Homomorphism {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
homo : IsHomomorphism a b func
|
