summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr8
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr29
-rw-r--r--src/Soat/FirstOrder/Term.idr10
3 files changed, 23 insertions, 24 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6f9389b..b9c02c5 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -8,6 +8,8 @@ import Soat.FirstOrder.Signature
%default total
%hide Control.Relation.Equivalence
+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
@@ -62,7 +64,7 @@ record IsHomomorphism
-> 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)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
func : IFunc a.raw.U b.raw.U
@@ -79,7 +81,7 @@ idIsHomo = MkIsHomomorphism
mapId tms)
public export
-idHomo : {a : Algebra sig} -> Homomorphism a a
+idHomo : {a : Algebra sig} -> a ~> a
idHomo = MkHomomorphism _ idIsHomo
public export
@@ -98,5 +100,5 @@ compIsHomo fHomo gHomo = MkIsHomomorphism
mapComp tms)
public export
-compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 29a740f..5e6d4ce 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -110,11 +110,11 @@ injectRIsHomo = MkIsHomomorphism
}
public export
-injectLHomo : Homomorphism x (CoproductAlgebra x y)
+injectLHomo : x ~> CoproductAlgebra x y
injectLHomo = MkHomomorphism _ $ injectLIsHomo
public export
-injectRHomo : Homomorphism y (CoproductAlgebra x y)
+injectRHomo : y ~> CoproductAlgebra x y
injectRHomo = MkHomomorphism _ $ injectRIsHomo
public export
@@ -127,14 +127,12 @@ coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
coproducts f g _ = bindTerms (\i => either (f i) (g i))
public export
-coproductCong : {x, y, z : Algebra sig}
- -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
-> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
public export
-coproductsCong : {x, y, z : Algebra sig}
- -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
-> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
-> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
@@ -164,7 +162,7 @@ coproductsCong f g _ (eq :: eqs) =
coproductCong f g _ eq :: coproductsCong f g _ eqs
public export
-coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+coproductIsHomo : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func)
coproductIsHomo f g = MkIsHomomorphism
{ cong = coproductCong f g
@@ -175,15 +173,14 @@ coproductIsHomo f g = MkIsHomomorphism
}
public export
-coproductHomo : {x, y, z : Algebra sig} -> Homomorphism x z -> Homomorphism y z
- -> Homomorphism (CoproductAlgebra x y) z
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+ -> CoproductAlgebra x y ~> z
coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g
public export
termToCoproduct : (x, y : Algebra sig)
- -> Homomorphism
- (FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))))
- (CoproductAlgebra x y)
+ -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
+ CoproductAlgebra x y
termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
{ cong = \t => tmRelImpliesCoprodRel
, semHomo = \op, tms =>
@@ -197,8 +194,8 @@ termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
public export
coproductUnique' : {x, y, z : Algebra sig}
- -> (f : Homomorphism (CoproductAlgebra x y) z)
- -> (g : Homomorphism (CoproductAlgebra x y) z)
+ -> (f : CoproductAlgebra x y ~> z)
+ -> (g : CoproductAlgebra x y ~> z)
-> (congL : {t : sig.T} -> (i : x.raw.U t)
-> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i))))
-> (congR : {t : sig.T} -> (i : y.raw.U t)
@@ -216,8 +213,8 @@ coproductUnique' f g congL congR tm = bindUnique'
}
public export
-coproductUnique : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
- -> (h : Homomorphism (CoproductAlgebra x y) z)
+coproductUnique : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
+ -> (h : CoproductAlgebra x y ~> z)
-> (congL : {t : sig.T} -> (i : x.raw.U t)
-> z.relation t (h.func t (Done (Left i))) (f.func t i))
-> (congR : {t : sig.T} -> (i : y.raw.U t)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 45282cc..bedfe3f 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -181,19 +181,19 @@ bindIsHomo a env = MkIsHomomorphism
bindTermsIsMap {a = a.raw} env.func tms)
public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a
+bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
public export
bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
- -> (f, g : Homomorphism (FreeAlgebra v) a)
+ -> (f, g : FreeAlgebra v ~> a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.relation t (f.func t tm) (g.func t tm)
public export
bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
- -> (f, g : Homomorphism (FreeAlgebra v) a)
+ -> (f, g : FreeAlgebra v ~> a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-> Pointwise a.relation (map f.func tms) (map g.func tms)
@@ -210,7 +210,7 @@ bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g con
public export
bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
- -> (f : Homomorphism (FreeAlgebra v) a)
+ -> (f : FreeAlgebra v ~> a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
@@ -218,7 +218,7 @@ bindUnique env f = bindUnique' f (bindHomo env)
public export
bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
- -> (f : Homomorphism (FreeAlgebra v) a)
+ -> (f : FreeAlgebra v ~> a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 23:44:14 +0000