blob: 26370cc6d596f485cd196dec67d5a60d2394bb27 (
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
module Soat.FirstOrder.Algebra
import Data.Morphism.Indexed
import Data.Setoid.Indexed
import public Soat.Data.Product
import Soat.FirstOrder.Signature
%default total
%hide Control.Relation.Equivalence
public export
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
algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t
public export
record RawAlgebra (0 sig : Signature) where
constructor MakeRawAlgebra
0 U : sig.T -> Type
sem : sig `algebraOver` U
public export
MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
public export
record RawAlgebraWithRelation (0 sig : Signature) where
constructor MkRawAlgebraWithRelation
raw : RawAlgebra sig
0 relation : IRel raw.U
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
constructor MkIsAlgebra
equivalence : IEquivalence a.U rel
semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
raw : RawAlgebra sig
0 relation : IRel raw.U
algebra : IsAlgebra sig raw relation
public export
(.setoid) : Algebra sig -> ISetoid sig.T
(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
public export
(.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig
(.rawWithRelation) a = MkRawAlgebraWithRelation a.raw a.relation
public export
record IsHomomorphism
{0 sig : Signature} (a, b : Algebra sig)
(f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
where
constructor MkIsHomomorphism
cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
-> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
func : IFunc a.raw.U b.raw.U
homo : IsHomomorphism a b func
public export
idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
idIsHomo = MkIsHomomorphism
(\_ => id)
(\op, tms =>
(a.algebra.equivalence _).equalImpliesEq $
sym $
cong (a.raw.sem op) $
mapId tms)
public export
idHomo : {a : Algebra sig} -> Homomorphism a a
idHomo = MkHomomorphism _ idIsHomo
public export
compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
-> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
compIsHomo fHomo gHomo = MkIsHomomorphism
(\t => fHomo.cong t . gHomo.cong t)
(\op, tms =>
(c.algebra.equivalence _).transitive
(fHomo.cong _ $ gHomo.semHomo op tms) $
(c.algebra.equivalence _).transitive
(fHomo.semHomo op (map g tms)) $
(c.algebra.equivalence _).equalImpliesEq $
sym $
cong (c.raw.sem op) $
mapComp tms)
public export
compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
public export
record Isomorphism {0 sig : Signature} (a, b : Algebra sig) where
constructor MkIsomorphism
to : Homomorphism a b
from : Homomorphism b a
fromTo : {t : sig.T} -> (x : a.raw.U t) -> a.relation t (from.func t $ to.func t x) x
toFrom : {t : sig.T} -> (x : b.raw.U t) -> b.relation t (to.func t $ from.func t x) x
|
