summaryrefslogtreecommitdiff
path: root/src/Soat/SecondOrder/Algebra/Lift.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr553
1 files changed, 336 insertions, 217 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index b08eb0e..61852f2 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -6,11 +6,17 @@ import Data.Setoid.Indexed
import Soat.Data.Product
import Soat.Data.Sublist
+
import Soat.FirstOrder.Algebra
+import Soat.FirstOrder.Algebra.Coproduct
+import Soat.FirstOrder.Algebra.FreeExtension
import Soat.FirstOrder.Term
+
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift
+import Syntax.PreorderReasoning.Setoid
+
%default total
public export
@@ -35,17 +41,17 @@ projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx)
public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
- -> (ctx : _)
+ -> (ctx : List sig.T)
-> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx)
-projectIsHomo {b = b} f ctx = MkIsHomomorphism
- (\t => f.cong t ctx)
- (\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)
+projectIsHomo {b = b} homo ctx = MkIsHomomorphism
+ { cong = \t => homo.cong t ctx
+ , semHomo = \op, tms => CalcWith (b.setoid.index _) $
+ |~ f _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f ctx) (wrap (MkPair []) tms))
+ ...(homo.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f t ctx) tms))
+ .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f ctx} tms)
+ }
public export
projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b
@@ -57,88 +63,77 @@ public export
-> (f : ctx `Sublist` ctx')
-> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra 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
+ , homo = MkIsHomomorphism
+ { cong = \t => a.algebra.renameCong t f
+ , semHomo = \op, tms => CalcWith (a.setoid.index _) $
+ |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms))
+ ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
+ ...(a.algebra.semCong _ (MkOp (Op op.op)) $
+ CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ _))) _) $
+ |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
+ ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
+ .=.(mapWrap (MkPair []) tms)
+ ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms)
+ .=.(cong (wrap (MkPair [])) $
+ pwEqImpliesEqual $
+ mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $
+ equalImpliesPwEq Refl))
+ }
+ }
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)
(.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')))
-
-renameBodyFunc : (f : ctx `Sublist` ctx')
- -> IFunction
- (isetoid (flip Elem ctx))
- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid
-renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f))
+ { func = \t, tm => a.raw.subst t ctx tm tms
+ , homo = MkIsHomomorphism
+ { cong = \t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl)
+ , semHomo = \op, tms' => CalcWith (a.setoid.index _) $
+ |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
+ ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms'))
+ ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
+ ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
+ ...(a.algebra.semCong ctx (MkOp (Op op.op)) $
+ CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $
+ |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
+ ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
+ .=.(mapWrap (MkPair []) tms')
+ ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')
+ ...(wrapIntro $
+ mapIntro' (\t, eq =>
+ a.algebra.substCong t ctx eq $
+ CalcWith (pwSetoid (a.setoidAt _) _) $
+ |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
+ ~~ map (\t => a.raw.rename t reflexive) tms
+ .=.(pwEqImpliesEqual $
+ mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $
+ equalImpliesPwEq Refl)
+ ~~ map (\t => id) tms
+ ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $
+ equalImpliesPwEq Refl)
+ ~~ tms
+ .=.(mapId tms)) $
+ pwRefl (\t => (a.algebra.equivalence _).refl)))
+ }
+ }
-indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
- -> IFunction
- (isetoid (flip Elem ts))
- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid
+indexFunc : {x : ISetoid a} -> (tms : x.U ^ ts) -> IFunction (isetoid (flip Elem ts)) x
indexFunc tms = MkIFunction
(\_ => index tms)
- (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms))
-
--- renameFunc : (f : ctx `Sublist` ctx')
--- -> IFunction
--- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid
--- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid
--- renameFunc f = MkIFunction
--- (\_ => bindTerm {a = Free _} (renameBodyFunc f).func)
--- (\t => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f))
+ (\_ => (x.equivalence _).equalImpliesEq . cong (index tms))
public export
Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
Initial sig = MakeRawAlgebra
(\t, ctx => Term sig (flip Elem ctx) t)
- (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
+ (\t, f => free (\_ => curry f) t)
(\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
Done
- (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
+ (\t, _, tm, tms => bindTerm {a = Free _} (\_ => index tms) t tm)
public export
InitialIsAlgebra : (0 sig : _)
@@ -147,91 +142,80 @@ InitialIsAlgebra : (0 sig : _)
(Initial sig)
(\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t)
InitialIsAlgebra sig = MkIsAlgebra
- (\(t, ctx) => tmRelEq (\_ => equiv) t)
- (\t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f))
- (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
- (\_, _, eq, eqs => bindTermCong'
+ { equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t
+ , renameCong = \t, f => freeCong (ifunc (\_ => curry f)) t
+ , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
+ , substCong = \_, _, eq, eqs => bindTermCong'
{a = FreeAlgebra (isetoid (flip Elem _))}
(\t, Refl => index eqs _)
- eq)
- (\t, ctx, tm =>
+ _
+ eq
+ , renameId = \t, ctx, tm =>
tmRelSym (\_ => MkSymmetric symmetric) $
- bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
- tm)
- (\t, f, g, tm =>
+ freeUnique (ifunc (\_ => curry reflexive)) idHomo (\i => Done' $ sym $ curryUncurry id i) $
+ tm
+ , renameComp = \t, f, g, tm =>
tmRelSym (\_ => MkSymmetric symmetric) $
- bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (renameBodyFunc (transitive g f))
- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
+ freeUnique
+ (ifunc (\_ => curry (transitive g f)))
+ (compHomo (freeHomo (ifunc (\_ => curry f))) (freeHomo (ifunc (\_ => curry g))))
(\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
- tm)
- (\f, (MkOp (Op op)), tms =>
+ tm
+ , semNat = \f, (MkOp (Op op)), tms =>
Call' (MkOp op) $
- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
- pwTrans (\_ => MkTransitive transitive) (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ _) $
- pwTrans (\_ => MkTransitive transitive)
- (mapIntro' (\t, eq =>
- tmRelEqualIsEqual $
- bindTermCong'
- {rel = \_ => Equal}
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
- tmRelReflexive (\_ => MkReflexive reflexive) $
- eq) $
- equalImpliesPwEq Refl) $
- equalImpliesPwEq $
- mapUnwrap _ _)
- -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
- -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $
- -- transitive
- -- (mapIntro
- -- (\t, eq =>
- -- bindTermCong'
- -- {v = isetoid (flip Elem _)}
- -- {a = FreeAlgebra (isetoid (flip Elem _))}
- -- (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
- -- tmRelReflexive (\_ => MkReflexive reflexive) $
- -- eq) $
- -- equalImpliesPwEq Refl) $
- -- equalImpliesPwEq $
- -- mapUnwrap
- -- (MkPair [])
- -- (\ty => (renameFunc (reflexive ++ f)).func (snd ty))
- -- tms)
- (\_, _ => Done' Refl)
- (\t, f, tm, tms =>
+ CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+ |~ bindTerms {a = Free _} (\_ => Done . curry f) _ (unwrap (MkPair []) tms)
+ ~~ map (free (\_ => curry f)) (unwrap (MkPair []) tms)
+ .=.(bindTermsIsMap {a = Free _} _ _)
+ ~~ map (free (\_ => curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms)
+ ..<(mapIntro' (\t =>
+ freeCong'
+ {rel = \_ => Equal}
+ {u = isetoid (flip Elem _)}
+ (\_, Refl => curryUncurry (curry f) _)
+ _) $
+ tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms))
+ ~~ unwrap (MkPair []) (map (\ty => free (\_ => curry (reflexive {x = fst ty} ++ f)) (snd ty)) tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ , varNat = \_, _ => Done' Refl
+ , substNat = \t, f, tm, tms =>
bindUnique
{a = FreeAlgebra (isetoid (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
+ (compHomo
+ (freeHomo (ifunc (\_ => curry f)))
+ (bindHomo (indexFunc tms)))
(\i =>
tmRelReflexive (\_ => MkReflexive reflexive) $
sym $
indexMap tms i)
- tm)
- (\t, ctx, f, tm, tms =>
+ tm
+ , substExnat = \t, ctx, f, tm, tms =>
bindUnique
{a = FreeAlgebra (isetoid (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
+ (compHomo
+ (bindHomo (indexFunc tms))
+ (freeHomo (ifunc (\_ => curry f))))
(\i =>
tmRelReflexive (\_ => MkReflexive reflexive) $
sym $
indexShuffle f i)
- tm)
- (\t, ctx, tm, tms, tms' =>
+ tm
+ , substComm = \t, ctx, tm, tms, tms' =>
bindUnique
{a = FreeAlgebra (isetoid (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
+ (compHomo
+ (bindHomo (indexFunc tms'))
+ (bindHomo (indexFunc tms)))
(\i =>
tmRelReflexive (\_ => MkReflexive reflexive) $
sym $
indexMap tms i)
- tm)
- (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
- (\t, ctx, tm =>
+ tm
+ , substVarL = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
+ , substVarR = \t, ctx, tm =>
tmRelSym (\_ => MkSymmetric symmetric) $
bindUnique
{a = FreeAlgebra (isetoid (flip Elem _))}
@@ -241,108 +225,113 @@ InitialIsAlgebra sig = MkIsAlgebra
tmRelReflexive (\_ => MkReflexive reflexive) $
sym $
indexTabulate Done i)
- tm)
- (\ctx, (MkOp (Op op)), tms, tms' =>
+ tm
+ , substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
Call' (MkOp op) $
- tmsRelTrans (\_ => MkTransitive transitive)
- (tmsRelSym (\_ => MkSymmetric symmetric) $
- bindsUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (indexFunc tms')
- (bindHomo (indexFunc _))
- (\i =>
- (tmRelTrans (\_ => MkTransitive transitive)
- (tmRelReflexive (\_ => MkReflexive reflexive) $
- indexMap
- {f = (\_ => bindTerm {a = Free _} (\_ => Done . curry (uncurry (curry reflexive))))}
- tms'
- i) $
- tmRelSym (\_ => MkSymmetric symmetric) $
- (bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (renameBodyFunc _)
- idHomo
- (\i =>
- Done' $
- sym $
- transitive (curryUncurry (curry reflexive) i) (curryUncurry id i))
- (index tms' i))))
- (unwrap (MkPair []) tms)) $
- tmsRelReflexive (\_ => MkReflexive reflexive) $
- mapUnwrap _ _)
+ CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+ |~ bindTerms {a = Free _} (\_ => index tms') _ (unwrap (MkPair []) tms)
+ ~~ map (bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms)
+ .=.(bindTermsIsMap {a = Free _} _ _)
+ ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms)
+ ..<(mapIntro' (\t => bindTermCong'
+ {rel = \_ => Equal}
+ {a = FreeAlgebra (isetoid (flip Elem _))}
+ (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $
+ |~ index (map (free (\_ => curry ([] {ys = []} ++ reflexive))) tms') _
+ ~~ free (\_ => curry ([] {ys = []} ++ reflexive)) _ (index tms' _)
+ .=.(indexMap tms' _)
+ ~~ index tms' _
+ ..<(freeUnique
+ (ifunc (\_ => curry ([] {ys = []} ++ reflexive)))
+ idHomo
+ (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
+ (index tms' _)))
+ _) $
+ tmsRelRefl (\_ => MkReflexive reflexive) $
+ unwrap (MkPair []) tms)
+ ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ }
public export
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 (InitialAlgebra sig) ctx)
- (\_ => Basics.id)
-freeToInitialIsHomo sig ctx = MkIsHomomorphism
- (\_ => id)
- (\(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)
- -> Homomorphism {sig = sig}
+ProjectInitialIsFree : (0 sig : _) -> (ctx : List sig.T)
+ -> Isomorphism {sig = sig}
(FreeAlgebra (isetoid (flip Elem ctx)))
(projectAlgebra (InitialAlgebra sig) ctx)
-freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
+ProjectInitialIsFree sig ctx = MkIsomorphism
+ { to = MkHomomorphism
+ { func = \_ => id
+ , homo = MkIsHomomorphism
+ { cong = \_ => id
+ , semHomo = \(MkOp op), ts =>
+ Call' (MkOp op) $
+ tmsRelReflexive (\_ => MkReflexive Refl) $
+ sym $
+ trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId ts)
+ }
+ }
+ , from = MkHomomorphism
+ { func = \_ => id
+ , homo = MkIsHomomorphism
+ { cong = \_ => id
+ , semHomo = \(MkOp op), ts =>
+ Call' (MkOp op) $
+ tmsRelReflexive (\_ => MkReflexive Refl) $
+ trans (unwrapWrap (extend (Initial sig).U ctx) ts) (sym $ mapId ts)
+ }
+ }
+ , fromTo = \tm => tmRelRefl (\_ => MkReflexive Refl) tm
+ , toFrom = \tm => tmRelRefl (\_ => MkReflexive Refl) tm
+ }
public export
-fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T)
- -> (Initial sig).U t ctx -> a.U t ctx
-fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
+fromInitial : (a : RawAlgebra (lift sig))
+ -> (t : _) -> (ctx : _) -> (Initial sig).U t ctx -> a.U t ctx
+fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) t
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, f => bindUnique'
+ { cong = \t, ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx) t
+ , renameHomo = \t, f => bindUnique'
{v = isetoid (flip Elem _)}
{a = projectAlgebra a _}
- (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
+ (compHomo (bindHomo (a.varFunc _)) (freeHomo (ifunc (\_ => curry f))))
(compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
- (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
- (\ctx, (MkOp (Op op)), tms =>
+ (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)
+ , semHomo = \ctx, (MkOp (Op op)), tms =>
a.algebra.semCong ctx (MkOp (Op op)) $
- map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
- equalImpliesPwEq $
- transitive
- (cong (wrap _) $ bindTermsIsMap {a = project a.raw _} (\_ => a.raw.var) $ unwrap _ tms) $
- transitive
- (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $
- cong (map _) $
- wrapUnwrap tms)
- (\_ => (a.algebra.equivalence _).reflexive)
- (\t, ctx, tm, tms => bindUnique'
- {v = isetoid (flip Elem _)}
- {a = projectAlgebra 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.varFunc _)
- (bindHomo (a.varFunc _))
- (\i => (a.algebra.equivalence _).reflexive)
- (index tms i)) $
- (a.algebra.equivalence _).symmetric $
- (a.algebra.equivalence _).transitive
- (a.algebra.substVarL ctx i _) $
- (a.algebra.equivalence _).equalImpliesEq $
- indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms i)
- tm)
+ CalcWith (pwSetoid (a.setoid.reindex (\ty => (snd ty, fst ty ++ ctx))) _) $
+ |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) _ (unwrap (MkPair []) tms))
+ ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms))
+ .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _)
+ ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms))
+ .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms)
+ ~~ map (extendFunc (fromInitial a.raw) ctx) tms
+ .=.(wrapUnwrap _)
+ , varHomo = \_ => (a.algebra.equivalence _).reflexive
+ , substHomo = \t, ctx, tm, tms =>
+ bindUnique'
+ {v = isetoid (flip Elem _)}
+ {a = projectAlgebra a _}
+ (compHomo
+ (bindHomo (a.varFunc _))
+ (bindHomo (indexFunc tms)))
+ (compHomo
+ (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
+ (\i => CalcWith (a.setoid.index _) $
+ |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) _ (index tms i)
+ ~~ index (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i
+ .=<(indexMap {f = bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i)
+ ~~ a.raw.subst _ ctx (a.raw.var i) (map (bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms)
+ ..<(a.algebra.substVarL ctx i _))
+ tm
+ }
public export
fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
@@ -358,5 +347,135 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
{v = isetoid (flip Elem _)}
{a = projectAlgebra a ctx}
(a.varFunc ctx)
- (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
+ (compHomo (projectHomo f ctx) (ProjectInitialIsFree sig ctx).to)
f.homo.varHomo
+
+public export
+FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig)
+FreeExtension a = MakeRawAlgebra
+ { U = \t, ctx => (FreeExtension a (flip Elem ctx)).U t
+ , rename = \t, f => extend (\_ => curry f) t
+ , sem = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])
+ , var = Done . Right . Done
+ , subst = \t, ctx, tm, tms =>
+ coproduct
+ {z = FreeExtension a (flip Elem _)}
+ (\_ => Done . Left)
+ (bindTerm {a = FreeExtension a (flip Elem _)} (\_ => index tms))
+ t
+ tm
+ }
+
+public export
+FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig)
+FreeExtensionAlgebra a = MkAlgebra
+ { raw = FreeExtension a.raw
+ , relation = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).relation t
+ , algebra = MkIsAlgebra
+ { equivalence = \(t, ctx) => (FreeExtensionAlgebra a (isetoid (flip Elem ctx))).algebra.equivalence t
+ , renameCong = \t, f => extendCong (ifunc (\_ => curry f)) t
+ , semCong = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
+ , substCong = \t, ctx, eq, eqs => coproductCong' {z = FreeExtensionAlgebra a (isetoid (flip Elem ctx))}
+ (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))})
+ (injectLHomo {y = FreeAlgebra (isetoid (flip Elem ctx))})
+ (bindHomo (indexFunc _))
+ (bindHomo (indexFunc _))
+ (\_ => DoneL)
+ (bindTermCong' {a = FreeExtensionAlgebra a (isetoid (flip Elem _))} (\_, Refl => index eqs _))
+ t
+ eq
+ , renameId = \t, ctx, tm =>
+ (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).symmetric $
+ extendUnique
+ { v = isetoid (flip Elem _)
+ , u = isetoid (flip Elem _)
+ , f = ifunc ?f -- (\_ => curry reflexive)
+ , g = idHomo
+ , congL = ?congL
+ , congR = ?congR
+ , tm = ?tm
+ }
+ -- extendUnique (ifunc (\_ => curry reflexive)) idHomo ?congL ?congR tm
+ , renameComp = \t, f, g, tm => ?renameComp
+ , semNat = \f, (MkOp (Op op)), tms => Call (MkOp op) $ ?semNat
+ , varNat = \f, i => (((FreeExtensionAlgebra a (isetoid (flip Elem _)))).algebra.equivalence _).reflexive
+ , substNat = \t, f, tm, tms => ?substNat
+ , substExnat = \t, ctx, f, tm, tms => ?substExnat
+ , substComm = \t, ctx, tm, tms, tms' => ?substComm
+ , substVarL = \ctx, i, tms => ?substVarL
+ , substVarR = \t, ctx, tm => ?substVarR
+ , substCompat = \ctx, (MkOp (Op op)), tms, tms' => Call (MkOp op) $ ?substCompat
+ }
+ }
+
+public export
+ProjectFreeExtensionIsOriginal : (a : FirstOrder.Algebra.Algebra sig)
+ -> Isomorphism (projectAlgebra (FreeExtensionAlgebra a) []) a
+
+public export
+FreeExtensionIsFree : (a : Algebra sig) -> (b : Algebra (lift sig))
+ -> Isomorphism (projectAlgebra b []) a
+ -> Homomorphism (FreeExtensionAlgebra a) b
+
+-- -- public export
+-- -- FreeExtension : RawAlgebra sig -> RawAlgebra (lift sig)
+-- -- FreeExtension a = MakeRawAlgebra
+-- -- { U = \t, ctx => (Coproduct a (Free (flip Elem ctx))).U t
+-- -- , rename = \t, f => coproduct
+-- -- {z = Coproduct a (Free (flip Elem _))}
+-- -- (\_ => Done . Left)
+-- -- (\t => Done . Right . (Initial sig).rename t f)
+-- -- t
+-- -- , sem = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])
+-- -- , var = Done . Right . Done
+-- -- , subst = \t, ctx, tm, tms => coproduct
+-- -- {z = Coproduct a (Free (flip Elem _))}
+-- -- (\_ => Done . Left)
+-- -- (\_ => bindTerm {a = Coproduct a (Free (flip Elem ctx))} (\_ => index tms))
+-- -- t
+-- -- tm
+-- -- }
+
+-- -- public export 0
+-- -- FreeExtensionRelation : (algebra : FirstOrder.Algebra.IsAlgebra sig a rel)
+-- -- -> IRel (uncurry (FreeExtension a).U)
+-- -- FreeExtensionRelation algebra (t, ctx) =
+-- -- (CoproductAlgebra (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem ctx)))).relation t
+
+-- -- public export
+-- -- FreeExtensionIsAlgebra : {a : RawAlgebra sig} -> forall rel . (algebra : IsAlgebra sig a rel)
+-- -- -> IsAlgebra (lift sig) (FreeExtension a) (FreeExtensionRelation algebra)
+-- -- FreeExtensionIsAlgebra algebra = MkIsAlgebra
+-- -- { equivalence = \(t, ctx) => ?equivalence
+-- -- , renameCong = \t, f => coproductCong
+-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
+-- -- (compHomo (injectRHomo a ?y) ?g)
+-- -- -- (compHomo
+-- -- -- (injectRHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
+-- -- -- ((InitialAlgebra sig).renameHomo f))
+-- -- t
+-- -- , semCong = \ctx, (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
+-- -- , substCong = \t, ctx, eq, eqs => coproductCong'
+-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
+-- -- (injectLHomo (MkAlgebra _ _ algebra) (FreeAlgebra (isetoid (flip Elem _))))
+-- -- (bindHomo (indexFunc _ _))
+-- -- (bindHomo (indexFunc _ _))
+-- -- (\_ => DoneL)
+-- -- ?rhs -- (bindTermCong' (\_ => index ?eqseqs))
+-- -- _
+-- -- ?eq
+-- -- , renameId = ?renameId
+-- -- , renameComp = ?renameComp
+-- -- , semNat = ?semNat
+-- -- , varNat = ?varNat
+-- -- , substNat = ?substNat
+-- -- , substExnat = ?substExnat
+-- -- , substComm = ?substComm
+-- -- , substVarL = ?substVarL
+-- -- , substVarR = ?substVarR
+-- -- , substCompat = ?substCompat
+-- -- }
+
+-- -- public export
+-- -- FreeExtensionAlgebra : Algebra sig -> Algebra (lift sig)
+-- -- FreeExtensionAlgebra a = MkAlgebra _ _ $ FreeExtensionIsAlgebra a.algebra
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:34:15 +0000