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
156
157
158
159
160
161
162
|
module Soat.SecondOrder.Algebra
import Data.Setoid.Indexed
import Data.List.Elem
import Soat.Data.Product
import Soat.Data.Sublist
import Soat.SecondOrder.Signature
infix 5 ~>
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 : (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 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)
-> extend x ctx ^ op.arity -> x t ctx
public export
record RawAlgebra (0 sig : Signature) where
constructor MkRawAlgebra
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
(.extendSubst) : (a : RawAlgebra sig) -> (ctx : List sig.T) -> {ctx' : List sig.T}
-> (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 . Sublist.elemJoinL {ys = ctx}) ++
map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms)
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
equivalence : IndexedEquivalence _ (uncurry a.U)
-- Congruences
renameCong : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-> {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} 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'} -> 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)
-> 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)
-> 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)
-> 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)
-> 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'')
-> 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'')
-> 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')
-> 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')
-> 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)
-> 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')
-> 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)
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
raw : RawAlgebra sig
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 -> 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) -> IndexedSetoid sig.T
(.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
public export
(.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 : 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.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.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.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.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)
|
