If we look at the forgetful functor U from the category LPro of costrong profunctors to the category Pro of profunctors, we can find its adjoints by using the usual Kan extension trick.
Ran U 1 -| U -| Lan U 1
Composing the parts of this adjoint triple yields a "real" Cotambara and Copastro construction.
Using Lan U 1:
data Cotambara q a b where
Cotambara :: Costrong r => (r :-> q) -> r a b -> Cotambara q a b
Using Ran U 1:
newtype Copastro p a b = Copastro { runCopastro :: forall r. Costrong r => (p :-> r) -> r a b }
Copastro -| Cotambara
and now they freely/cofreely generate costrength. They should also have the profunctor comonad/monad structure we find in the usual Pastro and Tambara constructions.
If we look at the forgetful functor U from the category LPro of costrong profunctors to the category Pro of profunctors, we can find its adjoints by using the usual Kan extension trick.
Ran U 1 -| U -| Lan U 1
Composing the parts of this adjoint triple yields a "real" Cotambara and Copastro construction.
Using
Lan U 1
:Using
Ran U 1
:Copastro -| Cotambara
and now they freely/cofreely generate costrength. They should also have the profunctor comonad/monad structure we find in the usual
Pastro
andTambara
constructions.