From 038a4c588a463f8d698d9926cabc371889ed7d56 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 6 Mar 2023 22:05:33 -0500 Subject: [PATCH] Define Coyoneda --- Data/Profunctor/Yoneda.idr | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Data/Profunctor/Yoneda.idr b/Data/Profunctor/Yoneda.idr index 0dde348..1809931 100644 --- a/Data/Profunctor/Yoneda.idr +++ b/Data/Profunctor/Yoneda.idr @@ -9,3 +9,8 @@ public export record Yoneda p a b where constructor MkYoneda runYoneda : forall x, y. (x -> a) -> (b -> y) -> p x y + + +public export +data Coyoneda : (p : Type -> Type -> Type) -> Type -> Type -> Type where + MkCoyoneda : (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b