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
|
module Soat.SecondOrder.Algebra
import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Data.List.Elem
import Soat.Data.Product
import Soat.Data.Sublist
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) -> {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)
-> {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) -> {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 : {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 : {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) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-> {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)
-> {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)
-> {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 : {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)
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)
-> {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) -> {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 : {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')
-> (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
|
