summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr55
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr49
-rw-r--r--src/Soat/FirstOrder/Term.idr25
-rw-r--r--src/Soat/SecondOrder/Algebra.idr28
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr147
5 files changed, 129 insertions, 175 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b9c02c5..7bed448 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -53,52 +53,39 @@ public export
(.rawSetoid) a = MkRawSetoidAlgebra 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 (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- func : IFunc a.raw.U b.raw.U
- homo : IsHomomorphism a b func
+ func : (t : sig.T) -> a.raw.U t -> b.raw.U t
+ cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
+ -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+ semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+ -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
public export
-idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
-idIsHomo = MkIsHomomorphism
- (\_ => id)
- (\op, tms =>
+idHomo : {a : Algebra sig} -> a ~> a
+idHomo = MkHomomorphism
+ { func = \_ => id
+ , cong = \_ => id
+ , semHomo = \op, tms =>
(a.algebra.equivalence _).equalImpliesEq $
sym $
cong (a.raw.sem op) $
- mapId tms)
+ mapId tms
+ }
public export
-idHomo : {a : Algebra sig} -> 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 =>
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
+compHomo f g = MkHomomorphism
+ { func = \t => f.func t . g.func t
+ , cong = \t => f.cong t . g.cong t
+ , semHomo = \op, tms =>
(c.algebra.equivalence _).transitive
- (fHomo.cong _ $ gHomo.semHomo op tms) $
+ (f.cong _ $ g.semHomo op tms) $
(c.algebra.equivalence _).transitive
- (fHomo.semHomo op (map g tms)) $
+ (f.semHomo op (map g.func tms)) $
(c.algebra.equivalence _).equalImpliesEq $
sym $
cong (c.raw.sem op) $
- mapComp tms)
-
-public export
-compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
-compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
+ mapComp tms
+ }
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5e6d4ce..a98391b 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -96,28 +96,22 @@ CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
- { cong = \_ => DoneL
+injectLHomo : x ~> CoproductAlgebra x y
+injectLHomo = MkHomomorphism
+ { func = \_ => Done . Left
+ , cong = \_ => DoneL
, semHomo = InjectL
}
public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
- { cong = \_ => DoneR
+injectRHomo : y ~> CoproductAlgebra x y
+injectRHomo = MkHomomorphism
+ { func = \_ => Done . Right
+ , cong = \_ => DoneR
, semHomo = InjectR
}
public export
-injectLHomo : x ~> CoproductAlgebra x y
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
-
-public export
-injectRHomo : y ~> CoproductAlgebra x y
-injectRHomo = MkHomomorphism _ $ injectRIsHomo
-
-public export
coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
coproduct f g _ = bindTerm (\i => either (f i) (g i))
@@ -137,19 +131,19 @@ coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
-> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
-coproductCong f g _ (DoneL eq) = f.homo.cong _ eq
-coproductCong f g _ (DoneR eq) = g.homo.cong _ eq
+coproductCong f g _ (DoneL eq) = f.cong _ eq
+coproductCong f g _ (DoneR eq) = g.cong _ eq
coproductCong f g _ (Call op eqs) =
z.algebra.semCong op $
coproductsCong f g _ eqs
coproductCong f g _ (InjectL op ts) = CalcWith (z.setoid.index _) $
|~ f.func _ (x.raw.sem op ts)
- ~~ z.raw.sem op (map f.func ts) ...(f.homo.semHomo op ts)
+ ~~ z.raw.sem op (map f.func ts) ...(f.semHomo op ts)
~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
coproductCong f g _ (InjectR op ts) = CalcWith (z.setoid.index _) $
|~ g.func _ (y.raw.sem op ts)
- ~~ z.raw.sem op (map g.func ts) ...(g.homo.semHomo op ts)
+ ~~ z.raw.sem op (map g.func ts) ...(g.semHomo op ts)
~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
coproductCong f g _ (Sym eq) = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
@@ -162,10 +156,11 @@ coproductsCong f g _ (eq :: eqs) =
coproductCong f g _ eq :: coproductsCong f g _ eqs
public export
-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
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+ -> CoproductAlgebra x y ~> z
+coproductHomo f g = MkHomomorphism
+ { func = coproduct {z = z.raw} f.func g.func
+ , cong = coproductCong f g
, semHomo = \op, tms =>
(z.algebra.equivalence _).equalImpliesEq $
cong (z.raw.sem op) $
@@ -173,16 +168,12 @@ coproductIsHomo f g = MkIsHomomorphism
}
public export
-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)
-> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
CoproductAlgebra x y
-termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
- { cong = \t => tmRelImpliesCoprodRel
+termToCoproduct x y = MkHomomorphism
+ { func = \_ => id
+ , cong = \t => tmRelImpliesCoprodRel
, semHomo = \op, tms =>
Call op $
coprodsRelReflexive
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index bedfe3f..f9f0879 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -170,19 +170,16 @@ bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
bindTermsCong env = bindTermsCong' env.cong
public export
-bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
- -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
-bindIsHomo a env = MkIsHomomorphism
- (\t, eq => bindTermCong env eq)
- (\op, tms =>
- a.algebra.semCong op $
- map (\t => (a.algebra.equivalence t).equalImpliesEq) $
- equalImpliesPwEq $
- bindTermsIsMap {a = a.raw} env.func tms)
-
-public export
bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
-bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
+bindHomo env = MkHomomorphism
+ { func = \_ => bindTerm {a = a.raw} env.func
+ , cong = \_ => bindTermCong env
+ , semHomo = \op, tms =>
+ a.algebra.semCong op $
+ map (\t => (a.algebra.equivalence t).equalImpliesEq) $
+ equalImpliesPwEq $
+ bindTermsIsMap {a = a.raw} env.func tms
+ }
public export
bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
@@ -201,9 +198,9 @@ bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
bindUnique' f g cong (Done i) = cong i
bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
|~ f.func _ (Call op ts)
- ~~ a.raw.sem op (map f.func ts) ...( f.homo.semHomo op ts )
+ ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
- ~~ g.func _ (Call op ts) ..<( g.homo.semHomo op ts )
+ ~~ g.func _ (Call op ts) ..<( g.semHomo op ts )
bindsUnique' f g cong [] = []
bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
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 16:23:50 +0000