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

Define Choice as special case of GenStrong

Browse source
This commit is contained in:
Kiana Sheibani 2023-03-06 10:51:23 -05:00
parent c6215d7509
commit 2e4fa7ff87
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
Data/Profunctor/Strong.idr
View file

@ -24,6 +24,18 @@ public export
second : Strong p => p a b -> p (c, a) (c, b) second : Strong p => p a b -> p (c, a) (c, b)
second = strongr {ten=Pair} second = strongr {ten=Pair}
public export
Choice : (p : Type -> Type -> Type) -> Type
Choice = GenStrong Either
public export
left : Choice p => p a b -> p (Either a c) (Either b c)
left = strongl {ten=Either}
public export
right : Choice p => p a b -> p (Either c a) (Either c b)
right = strongr {ten=Either}
export export