Free Arrows are Free Relative Monads

FreeArrow.idr

-- Original: https://gist.github.com/MonoidMusician/6c02a07b366813491143c3ad991753e7

-- Natural transformations between presheaves
(~>) : {k : Type} -> (k -> Type) -> (k -> Type) -> Type  
(~>) f g = {a : k} -> f a -> g a 

-- | First define a left kan extension from Type to Presheaves (k -> Type)

-- Takes two functors (Type -> (k -> Type) to a functor (k -> Type) -> (k -> Type) 
data PshLan  : (j, f : Type -> (k -> Type)) -> ((k -> Type) -> (k -> Type))  where 
  Map : {j, f : Type -> (k -> Type)} -> 
    (j a ~> c) -> f a ~> PshLan j f c

-- | Then take the free relative monad over PshLan
data Freer : (y, p : Type -> (k -> Type)) -> Type -> (k -> Type) where 
  Pure : y a ~> Freer y p a 
  Bind : (y a ~> Freer y p c) -> Freer y p a ~> Freer y p c 

-- Yoneda embedding, action on objects
Yo : Type -> (Type -> Type) 
Yo x y = y -> x

-- Hom Profunctor
Hom : Type -> (Type -> Type) 
Hom x y = x -> y

-- | This free monad should be isomorphic to a free arrow

-- Coyoneda for Profunctors
data CoyoProf : (Type -> Type -> Type) -> Type -> Type -> Type  where
  DiMap : (a -> b) -> p b c -> (c -> d) -> CoyoProf p a d

-- Free arrow over a profunctor
data FreeArr : (p : Type -> Type -> Type) -> Type -> Type -> Type where
  Arr : (a -> b) -> FreeArr p a b
  Comp : p x b -> FreeArr p a x -> FreeArr p a b
  
-- Free arrow over (Type -> Type -> Type)
FreeArr' : (Type -> Type -> Type) -> Type -> Type -> Type
FreeArr' p = FreeArr (CoyoProf p) 

-- | `Freer Yo p` should be isomorphic to `FreeArr' p`