I'm toying with functor pairs a la
https://blog.functorial.com/posts/2017-12-10-Co-Finds-A-Pairing.html
and
https://hackage.haskell.org/package/kan-extensions-5.2.1/docs/Control-Monad-Co.html#t:CoT
I am not very practiced with universe levels, however, and I've run into an issue that I don't see how to overcome. Here is my implementation so far:
data Co (W : Set o → Set l) (A : Set o) : Set (suc o ⊔ l) where
co : ( {R : Set o} → W (A → R) → R ) → Co W A
open import Category.Functor using (RawFunctor)
co-functor : {W : Set o → Set l} → RawFunctor W → RawFunctor (Co W)
co-functor rfw =
record
{ _<$>_ = λ f → λ where (co warr) → co λ wbr → warr (fmap (λ g → g ∘ f) wbr)
}
where
open import Function using (_∘_)
open RawFunctor rfw renaming (_<$>_ to fmap)
So the functor instance seems alright, but when I try to implement
co-monad : {W : Set o → Set l} → RawComonad W → RawMonad (Co W)
co-monad rcmw = ?
I quickly run into the issue that RawMonad in the stdlib operates on functors of shape Set f -> Set f. I believe this is not possible for Co since it contains (essentially) a forall {R}, which means it must be Set f -> Set (suc f).
At least that is my current understanding. I would appreciate any pointers; it's possible (or likely) I just haven't grasped the universes well enough to make this work on my own. I'd prefer not turning off universe levels, but I'm willing to do it if it's the only option that a beginner can handle.
