From 2e4fa7ff874075cb60fc646b0e5a1aad31be8ed1 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 6 Mar 2023 10:51:23 -0500 Subject: [PATCH] Define Choice as special case of GenStrong --- Data/Profunctor/Strong.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index 649c121..da0aba5 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -24,6 +24,18 @@ public export second : Strong p => p a b -> p (c, a) (c, b) 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