diff --git a/Data/Profunctor/Costrong.idr b/Data/Profunctor/Costrong.idr index 24800dd..8b25bcf 100644 --- a/Data/Profunctor/Costrong.idr +++ b/Data/Profunctor/Costrong.idr @@ -30,7 +30,7 @@ import Data.Profunctor.Types ||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`. ||| ||| Laws: -||| * `costrongl = costrongr . dimap swap swap` +||| * `costrongl = costrongr . dimap swap' swap'` ||| * `costrongl . dimap unitr.rightToLeft unitr.leftToRight = id` ||| * `costrongl . lmap (mapSnd f) = costrongl . rmap (mapSnd f)` ||| * `costrongr . costrongr = costrongr . dimap assocl assocr` diff --git a/Data/Profunctor/Mapping.idr b/Data/Profunctor/Mapping.idr index 90f8335..f08b904 100644 --- a/Data/Profunctor/Mapping.idr +++ b/Data/Profunctor/Mapping.idr @@ -141,12 +141,12 @@ Functor (FreeMapping p a) where export GenStrong Pair (FreeMapping p) where strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r) - strongl = dimap Builtin.swap Builtin.swap . strongr {p=FreeMapping p} + strongl = dimap swap' swap' . strongr {p=FreeMapping p} export GenStrong Either (FreeMapping p) where strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r) - strongl = dimap Tensor.swap Tensor.swap . strongr {p=FreeMapping p} + strongl = dimap swap' swap' . strongr {p=FreeMapping p} export Closed (FreeMapping p) where diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index 4197968..d7729f1 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -27,7 +27,7 @@ import Data.Profunctor.Types ||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`. ||| ||| Laws: -||| * `strongl = dimap swap swap . strongr` +||| * `strongl = dimap swap' swap' . strongr` ||| * `dimap unitr.rightToLeft unitr.leftToRight . strongl = id` ||| * `lmap (mapSnd f) . strongl = rmap (mapSnd f) . strongl` ||| * `strongr . strongr = dimap assocr assocl . strongr` @@ -161,8 +161,8 @@ Tensor ten i => ProfunctorComonad (GenTambara ten) where export Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where strongl (MkTambara p) = MkTambara $ dimap assocr assocl p - strongr (MkTambara p) = MkTambara $ dimap (assocr . mapFst swap) - (mapFst swap . assocl) p + strongr (MkTambara p) = MkTambara $ dimap (assocr . mapFst swap') + (mapFst swap' . assocl) p export Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where @@ -223,10 +223,10 @@ export projoin (MkPastro {x=x',y=y',z=z'} l' (MkPastro {x,y,z} l m r) r') = MkPastro ll m rr where ll : y `ten` (z' `ten` z) -> b - ll = l' . mapFst l . assocl . mapSnd swap + ll = l' . mapFst l . assocl . mapSnd swap' rr : a -> x `ten` (z' `ten` z) - rr = mapSnd swap . assocr . mapFst r . r' + rr = mapSnd swap' . assocr . mapFst r . r' export ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where @@ -244,9 +244,9 @@ export strongr (MkPastro {x,y,z} l m r) = MkPastro l' m r' where l' : y `ten` (c `ten` z) -> c `ten` b - l' = swap . mapFst l . assocl . mapSnd swap + l' = swap' . mapFst l . assocl . mapSnd swap' r' : c `ten` a -> x `ten` (c `ten` z) - r' = mapSnd swap . assocr . mapFst r . swap + r' = mapSnd swap' . assocr . mapFst r . swap' ||| The monad generated by the reflective subcategory of profunctors that diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr index d123747..200d678 100644 --- a/Data/Profunctor/Traversing.idr +++ b/Data/Profunctor/Traversing.idr @@ -128,12 +128,12 @@ Profunctor p => Profunctor (CofreeTraversing p) where export Profunctor p => GenStrong Pair (CofreeTraversing p) where strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}}) - strongl = dimap Builtin.swap Builtin.swap . strongr {p=CofreeTraversing p} + strongl = dimap swap' swap' . strongr {p=CofreeTraversing p} export Profunctor p => GenStrong Either (CofreeTraversing p) where strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}}) - strongl = dimap swap swap . strongr {p=CofreeTraversing p} + strongl = dimap swap' swap' . strongr {p=CofreeTraversing p} export Profunctor p => Traversing (CofreeTraversing p) where @@ -182,12 +182,12 @@ Profunctor (FreeTraversing p) where export GenStrong Pair (FreeTraversing p) where strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r) - strongl = dimap Builtin.swap Builtin.swap . strongr {p=FreeTraversing p} + strongl = dimap swap' swap' . strongr {p=FreeTraversing p} export GenStrong Either (FreeTraversing p) where strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r) - strongl = dimap swap swap . strongr {p=FreeTraversing p} + strongl = dimap swap' swap' . strongr {p=FreeTraversing p} export Traversing (FreeTraversing p) where diff --git a/Data/Tensor.idr b/Data/Tensor.idr index 65e3cb9..e90c599 100644 --- a/Data/Tensor.idr +++ b/Data/Tensor.idr @@ -34,11 +34,11 @@ interface Bifunctor ten => Associative ten where ||| The bifunctor `ten` is generally also associative. public export interface Bifunctor ten => Symmetric ten where - swap : a `ten` b -> b `ten` a - swap = symmetric.leftToRight + swap' : a `ten` b -> b `ten` a + swap' = symmetric.leftToRight symmetric : a `ten` b <=> b `ten` a - symmetric = MkEquivalence swap swap + symmetric = MkEquivalence swap' swap' ||| A tensor product is an associative bifunctor that has an identity element @@ -65,7 +65,7 @@ Associative Pair where export Symmetric Pair where - swap = Builtin.swap + swap' = swap export Tensor Pair () where @@ -90,7 +90,7 @@ Associative Either where export Symmetric Either where - swap = either Right Left + swap' = either Right Left export Tensor Either Void where