toki/idris2-profunctors
1
0
Fork 0
Code Issues Pull requests Activity

Add type synonyms for common tensor products

Browse source
This commit is contained in:
Kiana Sheibani 2023-03-06 11:01:17 -05:00
parent 2aa29d4bf5
commit f4dffcfa11
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 49 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
Data/Profunctor/Strong.idr
View file

@ -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