diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index 2b7fabc..0060047 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -100,14 +100,14 @@ ProfunctorFunctor (GenTambara ten) where export Tensor ten i => ProfunctorComonad (GenTambara ten) where - proextract (MkTambara p) = dimap unitr.bwd unitr.fwd p - produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assoc.bwd assoc.fwd p + proextract (MkTambara p) = dimap unitr.rightToLeft unitr.leftToRight p + produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assoc.rightToLeft assoc.leftToRight p export Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where - strongl (MkTambara p) = MkTambara $ dimap assoc.bwd assoc.fwd p - strongr (MkTambara p) = MkTambara $ dimap (assoc.bwd . mapFst swap) - (mapFst swap . assoc.fwd) p + strongl (MkTambara p) = MkTambara $ dimap assoc.rightToLeft assoc.leftToRight p + strongr (MkTambara p) = MkTambara $ dimap (assoc.rightToLeft . mapFst swap) + (mapFst swap . assoc.leftToRight) p export Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where @@ -120,7 +120,7 @@ gentambara @{gs} f x = MkTambara $ f $ strongl @{gs} x export ungentambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q -ungentambara f x = dimap unitr.bwd unitr.fwd $ runTambara $ f x +ungentambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x public export @@ -168,14 +168,14 @@ ProfunctorFunctor (GenPastro ten) where export (Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten) where - propure x = MkPastro unitr.fwd x unitr.bwd + propure x = MkPastro unitr.leftToRight x unitr.rightToLeft 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 . assoc.fwd . mapSnd swap + ll = l' . mapFst l . assoc.leftToRight . mapSnd swap rr : a -> x `ten` (z' `ten` z) - rr = mapSnd swap . assoc.bwd . mapFst r . r' + rr = mapSnd swap . assoc.rightToLeft . mapFst r . r' export ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where @@ -187,15 +187,15 @@ export strongl (MkPastro {x,y,z} l m r) = MkPastro l' m r' where l' : y `ten` (z `ten` c) -> b `ten` c - l' = mapFst l . assoc.fwd + l' = mapFst l . assoc.leftToRight r' : a `ten` c -> x `ten` (z `ten` c) - r' = assoc.bwd . mapFst r + r' = assoc.rightToLeft . mapFst r 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 . assoc.fwd . mapSnd swap + l' = swap . mapFst l . assoc.leftToRight . mapSnd swap r' : c `ten` a -> x `ten` (c `ten` z) - r' = mapSnd swap . assoc.bwd . mapFst r . swap + r' = mapSnd swap . assoc.rightToLeft . mapFst r . swap export @@ -204,7 +204,7 @@ genpastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m)) export ungenpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q -ungenpastro f x = f (MkPastro unitr.fwd x unitr.bwd) +ungenpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft) public export diff --git a/Data/Tensor.idr b/Data/Tensor.idr index df8b03f..4d12017 100644 --- a/Data/Tensor.idr +++ b/Data/Tensor.idr @@ -3,31 +3,29 @@ module Data.Tensor %default total -public export -record Isomorphism a b where - constructor MkIso - fwd : a -> b - bwd : b -> a - - public export interface Bifunctor ten => Associative ten where - assoc : Isomorphism (a `ten` (b `ten` c)) ((a `ten` b) `ten` c) + assoc : a `ten` (b `ten` c) <=> (a `ten` b) `ten` c public export interface Bifunctor ten => Symmetric ten where swap : a `ten` b -> b `ten` a + swap = symmetric.leftToRight + + symmetric : a `ten` b <=> b `ten` a + symmetric = MkEquivalence swap swap + public export interface Associative ten => Tensor ten i | ten where - unitl : Isomorphism (i `ten` a) a - unitr : Isomorphism (a `ten` i) a + unitl : i `ten` a <=> a + unitr : a `ten` i <=> a export Associative Pair where - assoc = MkIso (\(x,(y,z)) => ((x,y),z)) (\((x,y),z) => (x,(y,z))) + assoc = MkEquivalence (\(x,(y,z)) => ((x,y),z)) (\((x,y),z) => (x,(y,z))) export Symmetric Pair where @@ -35,13 +33,13 @@ Symmetric Pair where export Tensor Pair () where - unitl = MkIso snd ((),) - unitr = MkIso fst (,()) + unitl = MkEquivalence snd ((),) + unitr = MkEquivalence fst (,()) export Associative Either where - assoc = MkIso f b + assoc = MkEquivalence f b where f : forall a,b,c. Either a (Either b c) -> Either (Either a b) c f (Left x) = Left (Left x) @@ -59,5 +57,5 @@ Symmetric Either where export Tensor Either Void where - unitl = MkIso (either absurd id) Right - unitr = MkIso (either id absurd) Left + unitl = MkEquivalence (either absurd id) Right + unitr = MkEquivalence (either id absurd) Left