summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
-rw-r--r--src/Soat/SecondOrder/Algebra.idr4
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr35
5 files changed, 42 insertions, 44 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)
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 475bdc0..0ab235b 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -8,6 +8,8 @@ import Soat.Data.Product
import Soat.Data.Sublist
import Soat.SecondOrder.Signature
+infix 5 ~>
+
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)
@@ -153,7 +155,7 @@ record IsHomomorphism
(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)
+record (~>) {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
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 5f52f82..831b884 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -28,14 +28,13 @@ projectIsAlgebra a ctx = MkIsAlgebra
(\op => a.semCong ctx _ . wrapIntro)
public export
-projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
- -> FirstOrder.Algebra.Algebra sig
-projectAlgebra a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
+projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
-> (ctx : _)
- -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx)
+ -> IsHomomorphism (projectAlgebra sig a ctx) (projectAlgebra sig b ctx) (\t => f t ctx)
projectIsHomo {b = b} f ctx = MkIsHomomorphism
(\t => f.cong t ctx)
(\op, tms =>
@@ -47,14 +46,14 @@ projectIsHomo {b = b} f ctx = MkIsHomomorphism
mapWrap (MkPair []) tms)
public export
-projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b
- -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx)
+projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b
+ -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx)
public export
(.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
-> (f : ctx `Sublist` ctx')
- -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx')
+ -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
(.renameHomo) a f = MkHomomorphism
(\t => a.raw.rename t f)
(MkIsHomomorphism
@@ -78,7 +77,7 @@ public export
public export
(.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T)
-> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
- -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx)
+ -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
(.substHomo1) a ctx tms = MkHomomorphism
(\t, tm => a.raw.subst t ctx tm tms)
(MkIsHomomorphism
@@ -275,7 +274,7 @@ public export
freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
-> IsHomomorphism {sig = sig}
(FreeAlgebra (isetoid (flip Elem ctx)))
- (projectAlgebra (InitialAlgebra sig) ctx)
+ (projectAlgebra sig (InitialAlgebra sig) ctx)
(\_ => Basics.id)
freeToInitialIsHomo sig ctx = MkIsHomomorphism
(\_ => id)
@@ -287,9 +286,7 @@ freeToInitialIsHomo sig ctx = MkIsHomomorphism
public export
freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
- -> Homomorphism {sig = sig}
- (FreeAlgebra (isetoid (flip Elem ctx)))
- (projectAlgebra (InitialAlgebra sig) ctx)
+ -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
public export
@@ -301,10 +298,10 @@ public export
fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
-> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
fromInitialIsHomo a = MkIsHomomorphism
- (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx))
+ (\t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx))
(\t, f => bindUnique'
{v = isetoid (flip Elem _)}
- {a = projectAlgebra a _}
+ {a = projectAlgebra sig a _}
(compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
(compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
(\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
@@ -321,14 +318,14 @@ fromInitialIsHomo a = MkIsHomomorphism
(\_ => (a.algebra.equivalence _).reflexive)
(\t, ctx, tm, tms => bindUnique'
{v = isetoid (flip Elem _)}
- {a = projectAlgebra a _}
+ {a = projectAlgebra sig a _}
(compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms)))
(compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
(\i =>
(a.algebra.equivalence _).transitive
(bindUnique
{v = isetoid (flip Elem _)}
- {a = projectAlgebra a _}
+ {a = projectAlgebra sig a _}
(a.varFunc _)
(bindHomo (a.varFunc _))
(\i => (a.algebra.equivalence _).reflexive)
@@ -342,17 +339,17 @@ fromInitialIsHomo a = MkIsHomomorphism
public export
fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
- -> Homomorphism (InitialAlgebra sig) a
+ -> InitialAlgebra sig ~> a
fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
public export
fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
- -> (f : Homomorphism (InitialAlgebra sig) a)
+ -> (f : InitialAlgebra sig ~> a)
-> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
-> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
{v = isetoid (flip Elem _)}
- {a = projectAlgebra a ctx}
+ {a = projectAlgebra sig a ctx}
(a.varFunc ctx)
(compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
f.homo.varHomo
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 16:55:26 +0000