summaryrefslogtreecommitdiff
path: root/src/Soat/SecondOrder
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/SecondOrder')
-rw-r--r--src/Soat/SecondOrder/Algebra.idr28
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr147
2 files changed, 77 insertions, 98 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 0ab235b..d3e1f4c 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -132,31 +132,23 @@ public export
(\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
public export
-record IsHomomorphism
- {0 sig : Signature} (a, b : Algebra sig)
- (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
- constructor MkIsHomomorphism
+ constructor MkHomomorphism
+ func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
- -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm')
+ -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm')
renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
- -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
+ -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm)
semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.raw.U ctx ^ op.arity)
-> b.relation (t, ctx)
- (f t ctx $ a.raw.sem ctx op tms)
- (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
+ (func t ctx $ a.raw.sem ctx op tms)
+ (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms)
varHomo : {t : _} -> {ctx : _} -> (i : Elem t ctx)
- -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
+ -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i)
substHomo : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
-> (tms : (\t => a.raw.U t ctx) ^ ctx')
-> b.relation (t, ctx)
- (f t ctx $ a.raw.subst t ctx tm tms)
- (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)
-
-public export
-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
- homo : IsHomomorphism a b func
+ (func t ctx $ a.raw.subst t ctx tm tms)
+ (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms)
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 831b884..4ed29cf 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -32,80 +32,78 @@ projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Alge
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 (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 =>
+projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b
+ -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
+projectHomo f ctx = MkHomomorphism
+ { func = \t => f.func t ctx
+ , cong = \t => f.cong t ctx
+ , semHomo = \op, tms =>
(b.algebra.equivalence _).transitive
(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) $
b.algebra.semCong ctx (MkOp (Op op.op)) $
map (\(_,_) => (b.algebra.equivalence _).equalImpliesEq) $
equalImpliesPwEq $
- mapWrap (MkPair []) tms)
-
-public export
-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)
+ mapWrap (MkPair []) tms
+ }
public export
(.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
-> (f : ctx `Sublist` ctx')
-> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
(.renameHomo) a f = MkHomomorphism
- (\t => a.raw.rename t f)
- (MkIsHomomorphism
- (\t => a.algebra.renameCong t f)
- (\op, tms => (a.algebra.equivalence _).transitive
- (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
- (a.algebra.semCong _ (MkOp (Op op.op)) $
- map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
- pwSym (\_ => MkSymmetric symmetric) $
- pwTrans (\_ => MkTransitive transitive)
- (wrapIntro $
- mapIntro'' (\t, tm, _, Refl =>
- cong (\f => a.raw.rename t f tm) $
- sym $
- uncurryCurry f) $
- equalImpliesPwEq Refl) $
- equalImpliesPwEq $
- sym $
- mapWrap (MkPair []) tms)))
+ { func = \t => a.raw.rename t f
+ , cong = \t => a.algebra.renameCong t f
+ , semHomo = \op, tms => (a.algebra.equivalence _).transitive
+ (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ (a.algebra.semCong _ (MkOp (Op op.op)) $
+ map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
+ pwSym (\_ => MkSymmetric symmetric) $
+ pwTrans (\_ => MkTransitive transitive)
+ (wrapIntro $
+ mapIntro'' (\t, tm, _, Refl =>
+ cong (\f => a.raw.rename t f tm) $
+ sym $
+ uncurryCurry f) $
+ equalImpliesPwEq Refl) $
+ equalImpliesPwEq $
+ sym $
+ mapWrap (MkPair []) tms)
+ }
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')
-> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
(.substHomo1) a ctx tms = MkHomomorphism
- (\t, tm => a.raw.subst t ctx tm tms)
- (MkIsHomomorphism
- (\t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl))
- (\op, tms' => (a.algebra.equivalence _).transitive
- (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
- (a.algebra.semCong ctx (MkOp (Op op.op)) $
- pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
- pwTrans (\(_,_) => (a.algebra.equivalence _).trans)
- (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
- wrapIntro $
- mapIntro'' (\t, tm, _, Refl =>
- a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $
- pwTrans (\_ => (a.algebra.equivalence _).trans)
- (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive
- ((a.algebra.equivalence _).equalImpliesEq $
- cong (\f => a.raw.rename t f tm) $
- uncurryCurry reflexive)
- (a.algebra.renameId _ _ tm)) $
- equalImpliesPwEq Refl) $
- map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
- equalImpliesPwEq $
- mapId tms) $
- equalImpliesPwEq Refl) $
- map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
- equalImpliesPwEq $
- sym $
- mapWrap (MkPair []) tms')))
+ { func = \t, tm => a.raw.subst t ctx tm tms
+ , cong = \t, eq =>
+ a.algebra.substCong t ctx eq $
+ pwRefl (\_ => (a.algebra.equivalence _).refl)
+ , semHomo = \op, tms' => (a.algebra.equivalence _).transitive
+ (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
+ (a.algebra.semCong ctx (MkOp (Op op.op)) $
+ pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
+ pwTrans (\(_,_) => (a.algebra.equivalence _).trans)
+ (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
+ wrapIntro $
+ mapIntro'' (\t, tm, _, Refl =>
+ a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $
+ pwTrans (\_ => (a.algebra.equivalence _).trans)
+ (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive
+ ((a.algebra.equivalence _).equalImpliesEq $
+ cong (\f => a.raw.rename t f tm) $
+ uncurryCurry reflexive)
+ (a.algebra.renameId _ _ tm)) $
+ equalImpliesPwEq Refl) $
+ map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
+ equalImpliesPwEq $
+ mapId tms) $
+ equalImpliesPwEq Refl) $
+ map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
+ equalImpliesPwEq $
+ sym $
+ mapWrap (MkPair []) tms')
+ }
renameBodyFunc : (f : ctx `Sublist` ctx')
-> IFunction
@@ -271,23 +269,17 @@ InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig)
public export
-freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
- -> IsHomomorphism {sig = sig}
- (FreeAlgebra (isetoid (flip Elem ctx)))
- (projectAlgebra sig (InitialAlgebra sig) ctx)
- (\_ => Basics.id)
-freeToInitialIsHomo sig ctx = MkIsHomomorphism
- (\_ => id)
- (\(MkOp op), tms =>
+freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
+ -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
+freeToInitialHomo sig ctx = MkHomomorphism
+ { func = \_ => id
+ , cong = \_ => id
+ , semHomo = \(MkOp op), tms =>
Call' (MkOp op) $
tmsRelSym (\_ => MkSymmetric symmetric) $
tmsRelReflexive (\_ => MkReflexive reflexive) $
- transitive (unwrapWrap _ _) (mapId tms))
-
-public export
-freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
- -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
-freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
+ transitive (unwrapWrap _ _) (mapId tms)
+ }
public export
fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T)
@@ -295,9 +287,9 @@ fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) ->
fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
public export
-fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
- -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
-fromInitialIsHomo a = MkIsHomomorphism
+fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a
+fromInitialHomo a = MkHomomorphism
+ (fromInitial a.raw)
(\t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx))
(\t, f => bindUnique'
{v = isetoid (flip Elem _)}
@@ -338,11 +330,6 @@ fromInitialIsHomo a = MkIsHomomorphism
tm)
public export
-fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
- -> InitialAlgebra sig ~> a
-fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
-
-public export
fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
-> (f : InitialAlgebra sig ~> a)
-> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
@@ -352,4 +339,4 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
{a = projectAlgebra sig a ctx}
(a.varFunc ctx)
(compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
- f.homo.varHomo
+ f.varHomo
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 23:10:23 +0000