diff --git a/Data/Profunctor/Costrong.idr b/Data/Profunctor/Costrong.idr index 3a13354..58d7a98 100644 --- a/Data/Profunctor/Costrong.idr +++ b/Data/Profunctor/Costrong.idr @@ -144,36 +144,19 @@ ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where procounit (MkCopastro h) = proextract (h id) -export -gencopastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q -gencopastro f (MkCopastro h) = h f - -export -ungencopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q -ungencopastro f x = f (MkCopastro ($ x)) - - public export Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type Copastro = GenCopastro Pair -export -copastro : Costrong q => p :-> q -> Copastro p :-> q -copastro = gencopastro - -export -uncopastro : Copastro p :-> q -> p :-> q -uncopastro = ungencopastro - - public export CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type CopastroSum = GenCopastro Either -export -copastroSum : Cochoice q => p :-> q -> CopastroSum p :-> q -copastroSum = gencopastro export -uncopastroSum : CopastroSum p :-> q -> p :-> q -uncopastroSum = ungencopastro +copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q +copastro f (MkCopastro h) = h f + +export +uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q +uncopastro f x = f (MkCopastro ($ x)) diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index 0060047..f481a5f 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -114,39 +114,22 @@ Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where map = rmap -export -gentambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q -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.rightToLeft unitr.leftToRight $ runTambara $ f x - - public export Tambara : (p : Type -> Type -> Type) -> Type -> Type -> Type Tambara = GenTambara Pair -export -tambara : Strong p => p :-> q -> p :-> Tambara q -tambara = gentambara - -export -untambara : Profunctor q => p :-> Tambara q -> p :-> q -untambara = ungentambara - - public export TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type TambaraSum = GenTambara Either -export -tambaraSum : Choice p => p :-> q -> p :-> TambaraSum q -tambaraSum = gentambara export -untambaraSum : Profunctor q => p :-> TambaraSum q -> p :-> q -untambaraSum = ungentambara +tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q +tambara @{gs} f x = MkTambara $ f $ strongl @{gs} x + +export +untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q +untambara f x = dimap unitr.rightToLeft unitr.leftToRight $ runTambara $ f x -- Pastro @@ -198,36 +181,20 @@ export r' = mapSnd swap . assoc.rightToLeft . mapFst r . swap -export -genpastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q -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.leftToRight x unitr.rightToLeft) - - public export Pastro : (p : Type -> Type -> Type) -> Type -> Type -> Type Pastro = GenPastro Pair -export -pastro : Strong q => p :-> q -> Pastro p :-> q -pastro = genpastro - -export -unpastro : Pastro p :-> q -> p :-> q -unpastro = ungenpastro - - public export PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type PastroSum = GenPastro Either -export -pastroSum : Choice q => p :-> q -> PastroSum p :-> q -pastroSum = genpastro export -unpastroSum : PastroSum p :-> q -> p :-> q -unpastroSum = ungenpastro +pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q +pastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m)) + +export +unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q +unpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft) +