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.idr319
1 files changed, 174 insertions, 145 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 30bcd91..bb3d24b 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
@@ -14,37 +13,40 @@ import Soat.SecondOrder.Signature.Lift
import Syntax.PreorderReasoning.Setoid
%default total
+%ambiguity_depth 4
public export
project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
-> FirstOrder.Algebra.RawAlgebra sig
project a ctx = MkRawAlgebra
- (flip a.U ctx)
+ (\t => a.U t ctx)
(\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
public export
-projectIsAlgebra : IsAlgebra (lift sig) a -> (ctx : List sig.T) -> IsAlgebra sig (project a ctx)
-projectIsAlgebra a ctx = MkIsAlgebra
- (\t => a.relation (t, ctx))
- (\t => a.equivalence (t, ctx))
- (\op => a.semCong ctx _ . wrapIntro)
-
-public export
projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
-projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx)
+projectAlgebra sig a ctx = MkAlgebra
+ { raw = project a.raw ctx
+ , algebra = MkIsAlgebra
+ { equivalence = (reindex (flip MkPair ctx) a.setoid).equivalence
+ , semCong = \op => a.algebra.semCong ctx (MkOp (Op op.op)) . wrapIntro
+ }
+ }
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
- { func = \t => f.func t ctx
- , cong = \t => f.cong t ctx
- , semHomo = \op, tms => CalcWith (b.setoid.index _) $
- |~ f.func _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
- ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f.func ctx) (wrap (MkPair []) tms))
+ { func = MkIndexedSetoidHomomorphism
+ { H = \t => f.func.H (t, ctx)
+ , homomorphic = \t => f.func.homomorphic (t, ctx)
+ }
+ , semHomo = \op, tms => CalcWith (index b.setoid _) $
+ |~ f.func.H (_, ctx) (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
+ ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (\ty => f.func.H (snd ty, fst ty ++ ctx)) (wrap (MkPair []) tms))
...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
- ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func t ctx) tms))
- .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f.func ctx} tms)
+ ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func.H (t, ctx)) tms))
+ .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $
+ mapWrap (MkPair []) {f = \ty => f.func.H (snd ty, fst ty ++ ctx)} tms)
}
public export
@@ -52,23 +54,30 @@ public export
-> (f : ctx `Sublist` ctx')
-> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
(.renameHomo) a f = MkHomomorphism
- { func = \t => a.raw.rename t f
- , cong = \t => a.algebra.renameCong t f
- , semHomo = \op, tms => CalcWith (a.setoid.index _) $
+ { func = MkIndexedSetoidHomomorphism
+ { H = \t => a.raw.rename t f
+ , homomorphic = \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) _) $
+ CalcWith (index (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))
+ ...(wrapIntro $
+ mapIntro'' (\t, tm, tm', eq =>
+ CalcWith (index a.setoid (t, _)) $
+ |~ a.raw.rename t (reflexive {x = []} ++ f) tm
+ ~~ a.raw.rename t f tm
+ .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f)
+ ~~ a.raw.rename t f tm'
+ ...(a.algebra.renameCong t f eq)) $
+ (pwSetoid (a.setoidAt ctx)).equivalence.reflexive _ tms))
}
public export
@@ -76,17 +85,19 @@ public export
-> {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
- { 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' => CalcWith (a.setoid.index _) $
+ { func = MkIndexedSetoidHomomorphism
+ { H = \t, tm => a.raw.subst t ctx tm tms
+ , homomorphic = \t, _, _, eq =>
+ a.algebra.substCong t ctx eq $
+ (pwSetoid (a.setoidAt _)).equivalence.reflexive _ tms
+ }
+ , 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) _) $
+ CalcWith (index (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')
@@ -94,39 +105,42 @@ public export
...(wrapIntro $
mapIntro' (\t, eq =>
a.algebra.substCong t ctx eq $
- CalcWith (pwSetoid (a.setoidAt _) _) $
+ CalcWith (index (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)
+ ...(mapIntro'' (\t, tm, tm', eq =>
+ CalcWith (index a.setoid (t, ctx)) $
+ |~ a.raw.rename t ([] {ys = []} ++ reflexive) tm
+ ~~ a.raw.rename t reflexive tm
+ .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry reflexive)
+ ~~ tm
+ ...(a.algebra.renameId t ctx tm)
+ ~~ tm'
+ ...(eq)) $
+ (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _)
~~ tms
.=.(mapId tms)) $
- pwRefl (\t => (a.algebra.equivalence _).refl)))
+ (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))
+-- renameBodyFunc : (f : ctx `Sublist` ctx')
+-- -> irrelevantCast (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))
+-- indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
+-- -> irrelevantCast (flip Elem ts) ~>
+-- (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid
+-- indexFunc tms = mate (\_ => index tms)
+
+freeAlg : List sig.T -> FirstOrder.Algebra.Algebra sig
+freeAlg ctx = FreeAlgebra (irrelevantCast (flip Elem ctx))
public export
Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
Initial sig = MkRawAlgebra
- (\t, ctx => Term sig (flip Elem ctx) t)
- (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
+ (\t, ctx => (freeAlg ctx).raw.U t)
+ (\t, f => bindTerm {a = Free _} (\_ => Done . curry f))
(\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
Done
(\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)
@@ -134,29 +148,37 @@ Initial sig = MkRawAlgebra
public export
InitialIsAlgebra : (0 sig : _) -> SecondOrder.Algebra.IsAlgebra (lift sig) (Initial sig)
InitialIsAlgebra sig = MkIsAlgebra
- { relation = \(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t
- , equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t
- , renameCong = \t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)
- , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro
+ { equivalence = MkIndexedEquivalence
+ { relation = \(t, ctx) => (freeAlg ctx).relation t
+ , reflexive = \(t, ctx) => (freeAlg ctx).algebra.equivalence.reflexive t
+ , symmetric = \(t, ctx) => (freeAlg ctx).algebra.equivalence.symmetric t
+ , transitive = \(t, ctx) => (freeAlg ctx).algebra.equivalence.transitive t
+ }
+ , renameCong = \t, f => bindTermCong
+ { a = freeAlg _
+ , env = mate (\_ => Done . curry f)
+ }
+ , semCong = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro
, substCong = \_, _, eq, eqs => bindTermCong'
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (\t, Refl => index eqs _)
- eq
+ { a = freeAlg _
+ , cong = \_, Refl => index eqs _
+ , eq
+ }
, renameId = \t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
- bindUnique (renameBodyFunc reflexive) id (\i => Done' $ sym $ curryUncurry id i) $
- tm
+ (freeAlg _).setoid.equivalence.symmetric t _ _ $
+ bindUnique (mate (\_ => Done . curry reflexive)) id (\i => Done $ sym $ curryUncurry id i) tm
, renameComp = \t, f, g, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
+ (freeAlg _).setoid.equivalence.symmetric t _ _ $
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (renameBodyFunc (transitive g f))
- (bindHomo (renameBodyFunc f) . bindHomo (renameBodyFunc g))
- (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
- tm
+ { a = freeAlg _
+ , env = mate (\_ => Done . curry (transitive g f))
+ , f = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => Done . curry g))
+ , cong = \i => Done $ sym $ curryUncurry (curry f . curry g) i
+ , tm
+ }
, semNat = \f, (MkOp (Op op)), tms =>
- Call' (MkOp op) $
- CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+ Call (MkOp op) $
+ CalcWith (index (pwSetoid (freeAlg _).setoid) _) $
|~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms)
~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms)
.=.(bindTermsIsMap {a = Free _} _ _)
@@ -164,76 +186,78 @@ InitialIsAlgebra sig = MkIsAlgebra
..<(mapIntro' (\t =>
bindTermCong'
{rel = \_ => Equal}
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (\_, Refl => Done' $ curryUncurry (curry f) _)) $
- tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms))
+ {a = freeAlg _}
+ (\_, Refl => Done $ curryUncurry (curry f) _)) $
+ (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
~~ 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 _))}
- (indexFunc _)
- (bindHomo (renameBodyFunc f) . bindHomo (indexFunc tms))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm
- , substExnat = \t, ctx, f, tm, tms =>
- bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (indexFunc _)
- (bindHomo (indexFunc tms) . bindHomo (renameBodyFunc f))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexShuffle f i)
- tm
- , substComm = \t, ctx, tm, tms, tms' =>
- bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (indexFunc _)
- (bindHomo (indexFunc tms') . bindHomo (indexFunc tms))
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
- sym $
- indexMap tms i)
- tm
- , substVarL = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _
+ , varNat = \_, _ => Done Refl
+ , substNat = \t, f, tm, tms => bindUnique
+ { a = freeAlg _
+ , env = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) tms)
+ , f = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => index tms))
+ , cong = \i =>
+ reflect (index (freeAlg _).setoid _) $
+ sym $
+ indexMap tms i
+ , tm
+ }
+ , substExnat = \t, ctx, f, tm, tms => bindUnique
+ { a = freeAlg _
+ , env = mate (\_ => index $ shuffle f tms)
+ , f = bindHomo (mate (\_ => index tms)) . bindHomo (mate (\_ => Done . curry f))
+ , cong = \i =>
+ reflect (index (freeAlg _).setoid _) $
+ sym $
+ indexShuffle f i
+ , tm
+ }
+ , substComm = \t, ctx, tm, tms, tms' => bindUnique
+ { a = freeAlg _
+ , env = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => index tms')) tms)
+ , f = bindHomo (mate (\_ => index tms')) . bindHomo (mate (\_ => index tms))
+ , cong = \i =>
+ reflect (index (freeAlg _).setoid _) $
+ sym $
+ indexMap tms i
+ , tm
+ }
+ , substVarL = \_, _, _ => (freeAlg _).setoid.equivalence.reflexive _ _
, substVarR = \t, ctx, tm =>
- tmRelSym (\_ => MkSymmetric symmetric) $
+ (freeAlg _).setoid.equivalence.symmetric t _ _ $
bindUnique
- {a = FreeAlgebra (isetoid (flip Elem _))}
- (indexFunc _)
- id
- (\i =>
- tmRelReflexive (\_ => MkReflexive reflexive) $
+ { v = irrelevantCast (flip Elem ctx)
+ , a = freeAlg ctx
+ , env = mate (\_ => index $ tabulate (Done {sig = sig, v = flip Elem ctx}))
+ , f = id
+ , cong = \i =>
+ reflect (index (freeAlg ctx).setoid _) $
sym $
- indexTabulate Done i)
- tm
+ indexTabulate Done i
+ , tm
+ }
, substCompat = \ctx, (MkOp (Op op)), tms, tms' =>
- Call' (MkOp op) $
- CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $
+ Call (MkOp op) $
+ CalcWith (index (pwSetoid (freeAlg _).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 _) $
+ {a = freeAlg _}
+ (\t, Refl => CalcWith (index (freeAlg _).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
- (renameBodyFunc ([] {ys = []} ++ reflexive))
- id
- (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i))
- (index tms' _)))) $
- tmsRelRefl (\_ => MkReflexive reflexive) $
- unwrap (MkPair []) tms)
+ { env = mate (\_ => Done . curry ([] {ys = []} ++ reflexive))
+ , f = id
+ , cong = \i => Done $ sym $ trans (curryUncurry _ i) (curryUncurry id i)
+ , tm = index tms' _
+ }))) $
+ (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms))
~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms)
.=.(mapUnwrap (MkPair []) tms)
}
@@ -244,15 +268,18 @@ InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig)
public export
freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
- -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx
+ -> FreeAlgebra (irrelevantCast (flip Elem ctx)) ~>
+ projectAlgebra sig (InitialAlgebra sig) ctx
freeToInitialHomo sig ctx = MkHomomorphism
- { func = \_ => id
- , cong = \_ => id
+ { func = MkIndexedSetoidHomomorphism
+ { H = \_ => id
+ , homomorphic = \_, _, _ => id
+ }
, semHomo = \(MkOp op), tms =>
- Call' (MkOp op) $
- tmsRelSym (\_ => MkSymmetric symmetric) $
- tmsRelReflexive (\_ => MkReflexive reflexive) $
- transitive (unwrapWrap _ _) (mapId tms)
+ Call (MkOp op) $
+ reflect (index (pwSetoid ((InitialAlgebra sig).setoidAt ctx)) _) $
+ sym $
+ trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId tms)
}
public export
@@ -263,31 +290,33 @@ fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)
public export
fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a
fromInitialHomo a = MkHomomorphism
- { func = fromInitial a.raw
- , cong = \t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)
+ { func = MkIndexedSetoidHomomorphism
+ { H = \(t, ctx) => fromInitial a.raw t ctx
+ , homomorphic = \(t, ctx), _, _ => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)
+ }
, renameHomo = \t, f => bindUnique'
- {v = isetoid (flip Elem _)}
+ {v = irrelevantCast (flip Elem _)}
{a = projectAlgebra sig a _}
- (bindHomo (a.varFunc _) . bindHomo (renameBodyFunc f))
+ (bindHomo (a.varFunc _) . bindHomo (mate (\_ => Done . curry f)))
(a.renameHomo f . bindHomo (a.varFunc _))
- (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)
+ (\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i)
, semHomo = \ctx, (MkOp (Op op)), tms =>
a.algebra.semCong ctx (MkOp (Op op)) $
- CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $
+ CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
|~ 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))
+ ~~ wrap (MkPair []) (unwrap (MkPair []) (map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms))
.=.(cong (wrap _) $ mapUnwrap (MkPair []) tms)
- ~~ map (extendFunc (fromInitial a.raw) ctx) tms
+ ~~ map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms
.=.(wrapUnwrap _)
- , varHomo = \_ => (a.algebra.equivalence _).reflexive
+ , varHomo = \i => a.algebra.equivalence.reflexive _ $ a.raw.var i
, substHomo = \t, ctx, tm, tms => bindUnique'
- {v = isetoid (flip Elem _)}
+ {v = irrelevantCast (flip Elem _)}
{a = projectAlgebra sig a _}
- (bindHomo (a.varFunc _) . bindHomo (indexFunc tms))
+ (bindHomo (a.varFunc _) . bindHomo (mate (\_ => index tms)))
(a.substHomo1 ctx _ . bindHomo (a.varFunc _))
- (\i => CalcWith (a.setoid.index _) $
+ (\i => CalcWith (index a.setoid _) $
|~ 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)
@@ -300,9 +329,9 @@ 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)
- -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
+ -> a.relation (t, ctx) (f.func.H (t, ctx) tm) (fromInitial a.raw t ctx tm)
fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
- {v = isetoid (flip Elem _)}
+ {v = irrelevantCast (flip Elem _)}
{a = projectAlgebra sig a ctx}
(a.varFunc ctx)
(projectHomo f ctx . freeToInitialHomo sig ctx)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:12:58 +0000