diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 35 |
1 files changed, 16 insertions, 19 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 5f52f82..831b884 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -28,14 +28,13 @@ projectIsAlgebra a ctx = MkIsAlgebra (\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 : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig +projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx) 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) + -> IsHomomorphism (projectAlgebra sig a ctx) (projectAlgebra sig b ctx) (\t => f t ctx) projectIsHomo {b = b} f ctx = MkIsHomomorphism (\t => f.cong t ctx) (\op, tms => @@ -47,14 +46,14 @@ projectIsHomo {b = b} f ctx = MkIsHomomorphism mapWrap (MkPair []) tms) public export -projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b - -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) +projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b + -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx) public export (.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') - -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx') + -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx' (.renameHomo) a f = MkHomomorphism (\t => a.raw.rename t f) (MkIsHomomorphism @@ -78,7 +77,7 @@ public export 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) + -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx (.substHomo1) a ctx tms = MkHomomorphism (\t, tm => a.raw.subst t ctx tm tms) (MkIsHomomorphism @@ -275,7 +274,7 @@ public export freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T) -> IsHomomorphism {sig = sig} (FreeAlgebra (isetoid (flip Elem ctx))) - (projectAlgebra (InitialAlgebra sig) ctx) + (projectAlgebra sig (InitialAlgebra sig) ctx) (\_ => Basics.id) freeToInitialIsHomo sig ctx = MkIsHomomorphism (\_ => id) @@ -287,9 +286,7 @@ freeToInitialIsHomo sig ctx = MkIsHomomorphism public export freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T) - -> Homomorphism {sig = sig} - (FreeAlgebra (isetoid (flip Elem ctx))) - (projectAlgebra (InitialAlgebra sig) ctx) + -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx) public export @@ -301,10 +298,10 @@ 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 , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx)) (\t, f => bindUnique' {v = isetoid (flip Elem _)} - {a = projectAlgebra a _} + {a = projectAlgebra sig 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)) @@ -321,14 +318,14 @@ fromInitialIsHomo a = MkIsHomomorphism (\_ => (a.algebra.equivalence _).reflexive) (\t, ctx, tm, tms => bindUnique' {v = isetoid (flip Elem _)} - {a = projectAlgebra a _} + {a = projectAlgebra sig 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 = projectAlgebra sig a _} (a.varFunc _) (bindHomo (a.varFunc _)) (\i => (a.algebra.equivalence _).reflexive) @@ -342,17 +339,17 @@ fromInitialIsHomo a = MkIsHomomorphism public export fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) - -> Homomorphism (InitialAlgebra sig) a + -> 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) + -> (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) fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique {v = isetoid (flip Elem _)} - {a = projectAlgebra a ctx} + {a = projectAlgebra sig a ctx} (a.varFunc ctx) (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx)) f.homo.varHomo |