diff options
Diffstat (limited to 'src/Soat/Data/Product.idr')
| -rw-r--r-- | src/Soat/Data/Product.idr | 54 |
1 files changed, 30 insertions, 24 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index 0cb5dda..3a5d96c 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -1,8 +1,7 @@ module Soat.Data.Product import Data.List.Elem -import Data.Morphism.Indexed -import Data.Setoid.Indexed +import Data.Setoid.Indexed.Definition %default total @@ -68,7 +67,7 @@ map f [] = [] map f (x :: xs) = f _ x :: map f xs public export -indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is) +indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is) -> index (map f xs) elem = f i (index xs elem) indexMap (x :: xs) Here = Refl indexMap (x :: xs) (There elem) = indexMap xs elem @@ -79,8 +78,8 @@ mapId [] = Refl mapId (x :: xs) = cong ((::) x) $ mapId xs public export -mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is) - -> map (\i => f i . g i) xs = map f (map g xs) +mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i} + -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs) mapComp [] = Refl mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs @@ -95,7 +94,7 @@ wrap f [] = [] wrap f (x :: xs) = x :: wrap f xs public export -mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is) +mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is) -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs) mapWrap g [] = Refl mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs @@ -106,7 +105,8 @@ unwrap f {is = []} [] = [] unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs public export -mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is) +mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) + -> {is : _} -> (xs : x ^ map g is) -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs) mapUnwrap g {is = []} [] = Refl mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs @@ -166,16 +166,16 @@ namespace Pointwise public export pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} -> ((i : a) -> Reflexive (x i) (rel i)) - -> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs - pwRefl f {xs = []} = [] - pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f + -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs + pwRefl f [] = [] + pwRefl f (x :: xs) = reflexive :: pwRefl f xs public export pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} -> ((i : a) -> Reflexive (x i) (rel i)) -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys - pwReflexive refl Refl = pwRefl refl + pwReflexive refl Refl = pwRefl refl _ public export pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} @@ -193,44 +193,50 @@ namespace Pointwise pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss public export - pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel) + pwEquivalence : IndexedEquivalence a x -> {is : _} -> Equivalence (x ^ is) pwEquivalence eq = MkEquivalence - (MkReflexive $ pwRefl (\i => (eq i).refl)) - (MkSymmetric $ pwSym (\i => (eq i).sym)) - (MkTransitive $ pwTrans (\i => (eq i).trans)) + { relation = Pointwise eq.relation + , reflexive = pwRefl (\i => MkReflexive $ eq.reflexive i _) + , symmetric = \_, _ => pwSym (\i => MkSymmetric $ eq.symmetric i _ _) + , transitive = \_, _, _ => pwTrans (\i => MkTransitive $ eq.transitive i _ _ _) + } public export - pwSetoid : ISetoid a -> List a -> Setoid - pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence) + pwSetoid : IndexedSetoid a -> List a -> Setoid + pwSetoid x is = MkSetoid (x.U ^ is) (pwEquivalence x.equivalence) -- Introductors and Eliminators public export - mapIntro'' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y} + mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} + -> {0 f, g : (i : a) -> x i -> y i} -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v)) -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys) mapIntro'' cong [] = [] mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs public export - mapIntro' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y} + mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} + -> {0 f, g : (i : a) -> x i -> y i} -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v)) -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys) mapIntro' cong = mapIntro'' (\t, _, _ => cong t) public export - mapIntro : (f : IFunction x y) -> {is : _} -> {xs, ys : x.U ^ is} - -> Pointwise x.relation xs ys -> Pointwise y.relation (map f.func xs) (map f.func ys) - mapIntro f = mapIntro' f.cong + mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is} + -> Pointwise x.equivalence.relation xs ys + -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys) + mapIntro f = mapIntro' f.homomorphic public export - wrapIntro : forall f . {0 rel : IRel x} -> {0 xs, ys : (x . f) ^ is} + wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {0 xs, ys : (x . f) ^ is} -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys) wrapIntro [] = [] wrapIntro (r :: rs) = r :: wrapIntro rs public export - unwrapIntro : {0 f : a -> b} -> {0 rel : IRel x} -> {is : List a} -> {0 xs, ys : x ^ map f is} + unwrapIntro : {0 f : a -> b} -> {0 rel : (i : b) -> Rel (x i)} -> {is : List a} + -> {0 xs, ys : x ^ map f is} -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys) unwrapIntro {is = []} [] = [] unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs |