diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index 3e5d4a7..b204dca 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -81,10 +81,33 @@ export ungentambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q ungentambara f x = dimap unitr.bwd unitr.fwd $ getTambara $ f x + public export -Tambara : (p : Type -> Type -> Type) -> Type +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 + + -- Pastro public export @@ -142,3 +165,28 @@ export ungenpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q ungenpastro f x = f (MkPastro unitr.fwd x unitr.bwd) + +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