Free relative monads as free monads

A.agda

data Freer (F : Set → Set) (A : Set) : Set₁ where
  pure : A → Freer F A
  bind : (B : Set) → F B → (B → Freer F A) → Freer F A

data Freest {A : Set} (J : A → Set) (F : A → Set) (a : A) : Set where
  pure : J a → Freest J F a
  bind : (b : A) → F b → (J b → Freest J F a) → Freest J F a

data R {A : Set} (J : A → Set) (F : A → Set) : Set → Set where
  mkR : (a : A) → F a → R J F (J a)

st-r : {A : Set} {J F : A → Set} {a : A} → Freest J F a → Freer (R J F) (J a)
st-r (pure x) = pure x
st-r (bind b f k) = bind _ (mkR b f) λ x → st-r (k x)

r-st : {A : Set} {J F : A → Set} {a : A} → Freer (R J F) (J a) → Freest J F a
r-st (pure x) = pure x
r-st (bind _ (mkR b f) k) = bind b f λ x → r-st (k x)