diff options
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 68 |
1 files changed, 35 insertions, 33 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 596bb24..463fa84 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -131,27 +131,27 @@ Initial sig = MkRawAlgebra public export InitialIsAlgebra : (0 sig : _) -> SecondOrder.Algebra.IsAlgebra (lift sig) (Initial sig) InitialIsAlgebra sig = MkIsAlgebra - (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t) - (\(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' + { 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 + , 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) id (\i => Done' $ sym $ curryUncurry id i) $ - tm) - (\t, f, g, tm => + tm + , renameComp = \t, f, g, tm => tmRelSym (\_ => MkSymmetric symmetric) $ 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) - (\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 _} _ _) $ @@ -166,9 +166,9 @@ InitialIsAlgebra sig = MkIsAlgebra eq) $ equalImpliesPwEq Refl) $ equalImpliesPwEq $ - mapUnwrap _ _) - (\_, _ => Done' Refl) - (\t, f, tm, tms => + mapUnwrap _ _ + , varNat = \_, _ => Done' Refl + , substNat = \t, f, tm, tms => bindUnique {a = FreeAlgebra (isetoid (flip Elem _))} (indexFunc _) @@ -177,8 +177,8 @@ InitialIsAlgebra sig = MkIsAlgebra 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 _) @@ -187,8 +187,8 @@ InitialIsAlgebra sig = MkIsAlgebra 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 _) @@ -197,9 +197,9 @@ InitialIsAlgebra sig = MkIsAlgebra 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 _))} @@ -209,8 +209,8 @@ 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) $ @@ -237,7 +237,8 @@ InitialIsAlgebra sig = MkIsAlgebra (index tms' i)))) (unwrap (MkPair []) tms)) $ tmsRelReflexive (\_ => MkReflexive reflexive) $ - mapUnwrap _ _) + mapUnwrap _ _ + } public export InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig) @@ -264,15 +265,15 @@ fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) public export 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' + { func = fromInitial a.raw + , cong = \t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx) + , renameHomo = \t, f => bindUnique' {v = isetoid (flip Elem _)} {a = projectAlgebra sig a _} (bindHomo (a.varFunc _) . bindHomo (renameBodyFunc f)) (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 $ @@ -281,9 +282,9 @@ fromInitialHomo a = MkHomomorphism transitive (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $ cong (map _) $ - wrapUnwrap tms) - (\_ => (a.algebra.equivalence _).reflexive) - (\t, ctx, tm, tms => bindUnique' + wrapUnwrap tms + , varHomo = \_ => (a.algebra.equivalence _).reflexive + , substHomo = \t, ctx, tm, tms => bindUnique' {v = isetoid (flip Elem _)} {a = projectAlgebra sig a _} (bindHomo (a.varFunc _) . bindHomo (indexFunc tms)) @@ -302,7 +303,8 @@ fromInitialHomo a = MkHomomorphism (a.algebra.substVarL ctx i _) $ (a.algebra.equivalence _).equalImpliesEq $ indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms i) - tm) + tm + } public export fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)} |