blob: 982e54e13d3d9264a8a9fb976b1e3bf182686528 (
plain)
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
|
module Soat.FirstOrder.Algebra
import Data.Product
import Data.Setoid.Indexed
import Data.Setoid.Product
import Soat.FirstOrder.Signature
import Syntax.PreorderReasoning.Setoid
%default total
infix 5 ~>
public export 0
algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
public export
record RawAlgebra (0 sig : Signature) where
constructor MkRawAlgebra
0 U : sig.T -> Type
sem : sig `algebraOver` U
public export
record RawSetoidAlgebra (0 sig : Signature) where
constructor MkRawSetoidAlgebra
raw : RawAlgebra sig
0 relation : (t : sig.T) -> Rel (raw.U t)
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
equivalence : IndexedEquivalence sig.T a.U
semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-> Pointwise equivalence.relation tms tms'
-> equivalence.relation t (a.sem op tms) (a.sem op 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) -> (t : sig.T) -> Rel (a.raw.U t)
(.relation) a = a.algebra.equivalence.relation
public export
(.setoid) : Algebra sig -> IndexedSetoid sig.T
(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence
public export
(.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
(.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
public export
(.semFunc) : (a : Algebra sig) -> {t : sig.T} -> (op : Op sig t)
-> index (Product a.setoid) op.arity ~> index a.setoid t
a .semFunc op = MkSetoidHomomorphism (a.raw.sem op) (\_, _ => a.algebra.semCong op)
public export
record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
func : a.setoid ~> b.setoid
semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-> b.relation t (func.H t (a.raw.sem op tms)) (b.raw.sem op (map func.H tms))
public export
id : {a : Algebra sig} -> a ~> a
id = MkHomomorphism
{ func = id a.setoid
, semHomo = \op, tms =>
reflect (index a.setoid _) $
sym $
cong (a.raw.sem op) $
mapId tms
}
public export
(.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
(.) f g = MkHomomorphism
{ func = f.func . g.func
, semHomo = \op, tms =>
CalcWith (index c.setoid _) $
|~ f.func.H _ (g.func.H _ (a.raw.sem op tms))
~~ f.func.H _ (b.raw.sem op (map g.func.H tms)) ...(f.func.homomorphic _ _ _ $ g.semHomo op tms)
~~ c.raw.sem op (map f.func.H (map g.func.H tms)) ...(f.semHomo op $ map g.func.H tms)
~~ c.raw.sem op (map ((f.func . g.func).H) tms) .=<(cong (c.raw.sem op) $ mapComp tms)
}
|
