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.idr658
1 files changed, 383 insertions, 275 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index b08eb0e..e981593 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -1,7 +1,6 @@
module Soat.SecondOrder.Algebra.Lift
import Data.List.Elem
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
@@ -11,6 +10,9 @@ import Soat.FirstOrder.Term
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift
+import Syntax.PreorderReasoning.Setoid
+
+%ambiguity_depth 4
%default total
public export
@@ -21,31 +23,30 @@ project a ctx = MakeRawAlgebra
(\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
public export
-projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel
- -> (ctx : List sig.T)
- -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx))
-projectIsAlgebra a ctx = MkIsAlgebra
- (\t => a.equivalence (t, ctx))
- (\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 a ctx = MkAlgebra
+ { raw = project a.raw ctx
+ , algebra = MkIsAlgebra
+ { equivalence = (a.setoidAt ctx).equivalence
+ , semCong = \op => a.algebra.semCong ctx _ . wrapIntro
+ }
+ }
+
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)
-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 (index b.setoid _) $
+ |~ f _ _ (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,85 +58,79 @@ 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 (index a.setoid _) $
+ |~ 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 (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $
+ |~ 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')))
+ { func = \t, tm => a.raw.subst t ctx tm tms
+ , homo = MkIsHomomorphism
+ { cong = \t, eq =>
+ a.algebra.substCong t ctx eq $
+ (pwSetoid (a.setoidAt _) _).equivalence.reflexive _
+ , semHomo = \op, tms' => CalcWith (index a.setoid _) $
+ |~ 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 (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
+ |~ 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)) $
+ (pwSetoid (a.setoidAt _) _).equivalence.reflexive _))
+ }
+ }
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))
+ -> cast (flip Elem ctx) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx'))).setoid
+renameBodyFunc f = mate (\_ => Done . curry f)
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 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))
+ -> cast (flip Elem ts) ~> (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
+indexFunc tms = mate (\_ => 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 => bindTerm {a = Free _} (renameBodyFunc f).H)
(\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
Done
(\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
@@ -145,218 +140,331 @@ InitialIsAlgebra : (0 sig : _)
-> SecondOrder.Algebra.IsAlgebra
(lift 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'
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ { equivalence = (bundle $ \(t, ctx) => index (FreeAlgebra (irrelevantCast (flip Elem ctx))).setoid t).equivalence
+ , renameCong = \t, f => bindTermCong ?renameCongEnv t
+ , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
+ , substCong = \_, _, eq, eqs => bindTermCong'
+ {rel = \_ => Equal}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(\t, Refl => index eqs _)
- eq)
- (\t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
- bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
- tm)
- (\t, f, g, tm =>
+ eq
+ , renameId = \t, ctx, tm =>
+ (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
+ bindUnique ?renameIdEnv 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)))
+ ?renameCompEnv
+ -- (ifunc (\_ => curry (transitive g f)))
+ (compHomo (bindHomo ?renameCompFunc) (bindHomo ?renameCompFunc'))
(\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 (irrelevantCast (flip Elem _))).setoid _) $
+ |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
+ ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
+ .=.(bindTermsIsMap {a = Free _} _ _)
+ ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms)
+ ..<(mapIntro' (\t =>
+ bindTermCong'
+ {rel = \_ => Equal}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+ (\_, Refl => Done' $ curryUncurry (curry f) _)) $
+ (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive _)
+ ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ , varNat = \_, _ => Done' Refl
+ , substNat = \t, f, tm, tms =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm)
- (\t, ctx, f, tm, tms =>
+ (compHomo
+ (bindHomo ?substNatFunc)
+ (bindHomo (indexFunc tms)))
+ ?substNatCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexMap tms i)
+ tm
+ , substExnat = \t, ctx, f, tm, tms =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexShuffle f i)
- tm)
- (\t, ctx, tm, tms, tms' =>
+ (compHomo
+ (bindHomo (indexFunc tms))
+ (bindHomo ?substExnatFunc))
+ ?substExnatCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexShuffle f i)
+ tm
+ , substComm = \t, ctx, tm, tms, tms' =>
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
- (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm)
- (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
- (\t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
+ (compHomo
+ (bindHomo (indexFunc tms'))
+ (bindHomo (indexFunc tms)))
+ ?substCommCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexMap tms i)
+ tm
+ , substVarL = ?substVarL -- \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
+ , substVarR = \t, ctx, tm =>
+ (FreeAlgebra (irrelevantCast (flip Elem _))).setoid.equivalence.symmetric _ _ _ $
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
+ {a = FreeAlgebra (irrelevantCast (flip Elem _))}
(indexFunc _)
idHomo
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexTabulate Done i)
- tm)
- (\ctx, (MkOp (Op op)), tms, tms' =>
+ ?substVarRCong
+ -- (\i =>
+ -- tmRelReflexive (\_ => MkReflexive reflexive) $
+ -- sym $
+ -- indexTabulate Done i)
+ 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 (irrelevantCast (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 (irrelevantCast (flip Elem _))}
+ (\t, Refl => CalcWith (index (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _) $
+ |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _
+ ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _)
+ .=.(indexMap tms' _)
+ ~~ index tms' _
+ ..<(bindUnique
+ ?substCompatEnv
+ idHomo
+ (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
+ (index tms' _)))) $
+ (pwSetoid (FreeAlgebra (irrelevantCast (flip Elem _))).setoid _).equivalence.reflexive $
+ unwrap (MkPair []) tms)
+ ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
+ .=.(mapUnwrap (MkPair []) tms)
+ }
+-- InitialIsAlgebra sig = MkIsAlgebra
+-- (\(t, ctx) => tmRelEq (\_ => equiv) t)
+-- (\t, f => bindTermCong {a = FreeAlgebra (irrelevantCast (flip Elem _))} (renameBodyFunc f))
+-- (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
+-- (\_, _, eq, eqs => bindTermCong'
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (\t, Refl => index eqs _)
+-- eq)
+-- (\t, ctx, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
+-- tm)
+-- (\t, f, g, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (renameBodyFunc (transitive g f))
+-- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
+-- (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
+-- tm)
+-- (\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 (irrelevantCast (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 = irrelevantCast (flip Elem _)}
+-- -- {a = FreeAlgebra (irrelevantCast (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 =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexMap tms i)
+-- tm)
+-- (\t, ctx, f, tm, tms =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexShuffle f i)
+-- tm)
+-- (\t, ctx, tm, tms, tms' =>
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexMap tms i)
+-- tm)
+-- (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
+-- (\t, ctx, tm =>
+-- tmRelSym (\_ => MkSymmetric symmetric) $
+-- bindUnique
+-- {a = FreeAlgebra (irrelevantCast (flip Elem _))}
+-- (indexFunc _)
+-- idHomo
+-- (\i =>
+-- tmRelReflexive (\_ => MkReflexive reflexive) $
+-- sym $
+-- indexTabulate Done i)
+-- tm)
+-- (\ctx, (MkOp (Op op)), tms, tms' =>
+-- Call' (MkOp op) $
+-- tmsRelTrans (\_ => MkTransitive transitive)
+-- (tmsRelSym (\_ => MkSymmetric symmetric) $
+-- bindsUnique
+-- {a = FreeAlgebra (irrelevantCast (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 (irrelevantCast (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 _ _)
-public export
-InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
-InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig)
+-- 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
+-- freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
+-- -> IsHomomorphism {sig = sig}
+-- (FreeAlgebra (irrelevantCast (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}
- (FreeAlgebra (isetoid (flip Elem ctx)))
- (projectAlgebra (InitialAlgebra sig) ctx)
-freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
+-- public export
+-- freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
+-- -> Homomorphism {sig = sig}
+-- (FreeAlgebra (irrelevantCast (flip Elem ctx)))
+-- (projectAlgebra (InitialAlgebra sig) ctx)
+-- freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)
-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)
+-- 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)
-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'
- {v = isetoid (flip Elem _)}
- {a = projectAlgebra 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))
- (\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)
+-- 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'
+-- {v = irrelevantCast (flip Elem _)}
+-- {a = projectAlgebra 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))
+-- (\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 = irrelevantCast (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 = irrelevantCast (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)
-public export
-fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
- -> Homomorphism (InitialAlgebra sig) a
-fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)
+-- public export
+-- fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
+-- -> Homomorphism (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)
- -> (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.varFunc ctx)
- (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
- f.homo.varHomo
+-- public export
+-- fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
+-- -> (f : Homomorphism (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 = irrelevantCast (flip Elem _)}
+-- {a = projectAlgebra 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 21:41:01 +0000