diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 147 |
1 files changed, 67 insertions, 80 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 831b884..4ed29cf 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -32,80 +32,78 @@ projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Alge 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 (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 => +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 => (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) - -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 (\t => f.func t ctx) (projectIsHomo f.homo ctx) + mapWrap (MkPair []) tms + } public export (.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> projectAlgebra sig a ctx ~> projectAlgebra sig 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 + , cong = \t => a.algebra.renameCong t f + , semHomo = \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) + } 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') -> projectAlgebra sig a ctx' ~> projectAlgebra sig 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 + , cong = \t, eq => + a.algebra.substCong t ctx eq $ + pwRefl (\_ => (a.algebra.equivalence _).refl) + , semHomo = \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') + } renameBodyFunc : (f : ctx `Sublist` ctx') -> IFunction @@ -271,23 +269,17 @@ 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 sig (InitialAlgebra sig) ctx) - (\_ => Basics.id) -freeToInitialIsHomo sig ctx = MkIsHomomorphism - (\_ => id) - (\(MkOp op), tms => +freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T) + -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx +freeToInitialHomo sig ctx = MkHomomorphism + { func = \_ => id + , cong = \_ => id + , semHomo = \(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) - -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx -freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx) + transitive (unwrapWrap _ _) (mapId tms) + } public export fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T) @@ -295,9 +287,9 @@ fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> 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 +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' {v = isetoid (flip Elem _)} @@ -338,11 +330,6 @@ fromInitialIsHomo a = MkIsHomomorphism tm) public export -fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) - -> InitialAlgebra sig ~> a -fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a) - -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) @@ -352,4 +339,4 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique {a = projectAlgebra sig a ctx} (a.varFunc ctx) (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx)) - f.homo.varHomo + f.varHomo |