blob: 675c65b2390d62bdeb5a17927db2573d9ef5cb6b (
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
|
module Soat.FirstOrder.Algebra.FreeExtension
import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Algebra.Coproduct
import Soat.FirstOrder.Signature
import Soat.FirstOrder.Term
%default total
public export
FreeExtension : (a : RawAlgebra sig) -> (v : sig.T -> Type) -> RawAlgebra sig
FreeExtension a v = Coproduct a (Free v)
public export
FreeExtensionAlgebra : (a : Algebra sig) -> (v : ISetoid sig.T) -> Algebra sig
FreeExtensionAlgebra a v = CoproductAlgebra a (FreeAlgebra v)
public export
extend : {a : RawAlgebra sig} -> {u : sig.T -> Type} -> (f : IFunc v u)
-> IFunc (FreeExtension a v).U (FreeExtension a u).U
extend f = coproduct {z = FreeExtension a u}
(\_ => Done . Left)
(\t => Done . Right . free f t)
public export
extendHomo : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
-> Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u)
extendHomo f = coproductHomo {z = FreeExtensionAlgebra a u}
(injectLHomo {y = FreeAlgebra u})
(compHomo injectRHomo (freeHomo f))
public export
extendCong : {a : Algebra sig} -> {v, u : ISetoid sig.T} -> (f : IFunction v u)
-> (t : sig.T) -> {tm, tm' : (FreeExtension a.raw v.U).U t}
-> (FreeExtensionAlgebra a v).relation t tm tm'
-> ((FreeExtensionAlgebra a u).relation t `on` extend {a = a.raw} f.func t) tm tm'
extendCong f = coproductCong {z = FreeExtensionAlgebra a u}
(injectLHomo {y = FreeAlgebra u})
(compHomo injectRHomo (freeHomo f))
public export
extendUnique : {a : Algebra sig} -> {v, u : ISetoid sig.T}
-> (f : IFunction v u)
-> (g : Homomorphism (FreeExtensionAlgebra a v) (FreeExtensionAlgebra a u))
-> (congL : {t : sig.T} -> (i : a.raw.U t)
-> (FreeExtensionAlgebra a u).relation t (g.func t (Done (Left i))) (Done (Left i)))
-> (congR : {t : sig.T} -> (i : Term sig v.U t)
-> (FreeExtensionAlgebra a u).relation t
(g.func t (Done (Right i)))
(Done (Right (free f.func t i))))
-> {t : sig.T} -> (tm : _)
-> (FreeExtensionAlgebra a u).relation t (g.func t tm) (extend {a = a.raw} f.func t tm)
extendUnique f = coproductUnique {z = FreeExtensionAlgebra a u}
(injectLHomo {y = FreeAlgebra u})
(compHomo injectRHomo (freeHomo f))
|
