From 99ff1476aa42e01e1accae2ab8361c50032c3fe1 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Wed, 8 Mar 2023 13:30:55 -0500
Subject: [PATCH] Implement Corepresentable for Morphism

---
 Data/Profunctor/Cayley.idr        |  2 +-
 Data/Profunctor/Representable.idr | 12 ++++++++++--
 Data/Profunctor/Sieve.idr         |  1 -
 Data/Profunctor/Types.idr         |  2 +-
 4 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/Data/Profunctor/Cayley.idr b/Data/Profunctor/Cayley.idr
index 714baea..4c61f4b 100644
--- a/Data/Profunctor/Cayley.idr
+++ b/Data/Profunctor/Cayley.idr
@@ -63,5 +63,5 @@ Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where
 
 
 export
-mapCayley : (forall x. f x -> g x) -> Cayley f p a b -> Cayley g p a b
+mapCayley : (forall x. f x -> g x) -> Cayley f p :-> Cayley g p
 mapCayley f (MkCayley p) = MkCayley (f p)
diff --git a/Data/Profunctor/Representable.idr b/Data/Profunctor/Representable.idr
index d51366e..63059aa 100644
--- a/Data/Profunctor/Representable.idr
+++ b/Data/Profunctor/Representable.idr
@@ -61,9 +61,17 @@ export
 Functor f => Representable (Star f) f where
   tabulate = MkStar
 
+export
+Corepresentable Morphism Identity where
+  cotabulate f = Mor (f . Id)
+
+namespace Corepresentable
+  ||| A named implementation of `Corepresentable` for function types.
+  ||| Use this to avoid having to use a type wrapper like `Morphism`.
+  export
+  [Function] Corepresentable (\a,b => a -> b) Identity using Cosieve.Function where
+    cotabulate = (. Id)
 
 export
 Functor f => Corepresentable (Costar f) f where
   cotabulate = MkCostar
-
-
diff --git a/Data/Profunctor/Sieve.idr b/Data/Profunctor/Sieve.idr
index 7308062..693646b 100644
--- a/Data/Profunctor/Sieve.idr
+++ b/Data/Profunctor/Sieve.idr
@@ -48,7 +48,6 @@ Functor f => Sieve (Star f) f where
   sieve = applyStar
 
 
-
 export
 Cosieve Morphism Identity where
   cosieve (Mor f) = f . runIdentity
diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr
index 3211308..8648e23 100644
--- a/Data/Profunctor/Types.idr
+++ b/Data/Profunctor/Types.idr
@@ -82,7 +82,7 @@ Functor f => Profunctor (Kleislimorphism f) where
 
 
 ------------------------------------------------------------------------------
--- Implementations for existing types
+-- New profunctor types
 ------------------------------------------------------------------------------