diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
| commit | 580970d11a4e754c0c8e6f42c8312bffb1edc2db (patch) | |
| tree | 47e85bfd18a33ed6fd87e1c82181e5cdb5f6d43b /src/Soat/SecondOrder/Algebra/Lift.idr | |
| parent | 242197f40bb7957625be1e5f0bfd325af6e06be4 (diff) | |
Move IsAlgebra relation from type to body.
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 5be7dd1..5f52f82 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -21,17 +21,16 @@ project a ctx = MkRawAlgebra (\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 : 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 : 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 _ (projectIsAlgebra a.algebra ctx) public export projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f @@ -141,12 +140,9 @@ Initial sig = MkRawAlgebra (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t) public export -InitialIsAlgebra : (0 sig : _) - -> SecondOrder.Algebra.IsAlgebra - (lift sig) - (Initial sig) - (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t) +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) @@ -273,7 +269,7 @@ InitialIsAlgebra sig = MkIsAlgebra public export InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig) -InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig) +InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig) public export freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T) |