diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 116b5e4..d80eeb1 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -65,7 +65,7 @@ public export ...(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 (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $ + CalcWith (index (Product (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) @@ -78,7 +78,7 @@ public export .=.(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)) + (Product (a.setoidAt ctx)).equivalence.reflexive _ tms)) } public export @@ -90,7 +90,7 @@ public export { 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 + (Product (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 @@ -98,7 +98,7 @@ public export ...(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 (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $ + CalcWith (index (Product (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') @@ -106,7 +106,7 @@ public export ...(wrapIntro $ mapIntro' (\t, eq => a.algebra.substCong t ctx eq $ - CalcWith (index (pwSetoid (a.setoidAt _)) _) $ + CalcWith (index (Product (a.setoidAt _)) _) $ |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms ~~ map (\t => id) tms ...(mapIntro'' (\t, tm, tm', eq => @@ -118,10 +118,10 @@ public export ...(a.algebra.renameId t ctx tm) ~~ tm' ...(eq)) $ - (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _) + (Product (a.setoidAt _)).equivalence.reflexive _ _) ~~ tms .=.(mapId tms)) $ - (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _)) + (Product (a.setoidAt _)).equivalence.reflexive _ _)) } -- renameBodyFunc : (f : ctx `Sublist` ctx') @@ -179,7 +179,7 @@ InitialIsAlgebra sig = MkIsAlgebra } , semNat = \f, (MkOp (Op op)), tms => Call (MkOp op) $ - CalcWith (index (pwSetoid (freeAlg _).setoid) _) $ + CalcWith (index (Product (freeAlg _).setoid) _) $ |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms) ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms) .=.(bindTermsIsMap {a = Free _} _ _) @@ -189,7 +189,7 @@ InitialIsAlgebra sig = MkIsAlgebra {rel = \_ => Equal} {a = freeAlg _} (\_, Refl => Done $ curryUncurry (curry f) _)) $ - (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms)) + (Product (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 @@ -239,7 +239,7 @@ InitialIsAlgebra sig = MkIsAlgebra } , substCompat = \ctx, (MkOp (Op op)), tms, tms' => Call (MkOp op) $ - CalcWith (index (pwSetoid (freeAlg _).setoid) _) $ + CalcWith (index (Product (freeAlg _).setoid) _) $ |~ bindTerms {a = Free _} (\_ => index tms') (unwrap (MkPair []) tms) ~~ map (\_ => bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms) .=.(bindTermsIsMap {a = Free _} _ _) @@ -258,7 +258,7 @@ InitialIsAlgebra sig = MkIsAlgebra , cong = \i => Done $ sym $ trans (curryUncurry _ i) (curryUncurry id i) , tm = index tms' _ }))) $ - (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms)) + (Product (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms)) ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms) .=.(mapUnwrap (MkPair []) tms) } @@ -278,7 +278,7 @@ freeToInitialHomo sig ctx = MkHomomorphism } , semHomo = \(MkOp op), tms => Call (MkOp op) $ - reflect (index (pwSetoid ((InitialAlgebra sig).setoidAt ctx)) _) $ + reflect (index (Product ((InitialAlgebra sig).setoidAt ctx)) _) $ sym $ trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId tms) } @@ -303,7 +303,7 @@ fromInitialHomo a = MkHomomorphism (\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i) , semHomo = \ctx, (MkOp (Op op)), tms => a.algebra.semCong ctx (MkOp (Op op)) $ - CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $ + CalcWith (index (Product (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} _ _) |