I'm guessing that we get soundness :: a -> p a for free in your notation?

I think you wanted loeb :: Prov p => (p a -> a) -> p a.

Scala implementation, I think:

trait ProofLike[O[_]] {
  def sound[A](a: A): O[A]
  def dup[A](oa: O[A]): O[O[A]] //Isn't this just a special case of soundness?
  def mp[A, B](oab: O[A => B]): O[A] => O[B]
}

/**
 * type-level function. Implementation left as an exercise for the reader
 */
trait MFix[F[_], O[_]] {
    type Psi
    def ->(p: Psi): F[O[Psi]]
    def <-(fop: F[O[Psi]]): Psi
}

def loeb[O[_]: ProofLike, P](l1: O[P] => P, fx: MFix[({type F[A] = (A => P)]})#F, O]) : P = {
  val pl = implicitly[ProofLike[O]]
  type Psi = fx.Psi
  val l3: Psi => (O[Psi] => P) = fx.->
  val l4: O[Psi => (O[Psi] => P)] = pl.sound(l3)
  val l5: O[Psi] => O[O[Psi] => P] = pl.mp(l4)
  val l6: O[O[Psi] => P] => (O[O[Psi]] => O[P]) = pl.mp[O[Psi], P]
  val l7: O[Psi] => (O[O[Psi]] => O[P]) = l5 andThen l6
  val l8: O[Psi] => O[O[Psi]] = pl.dup[Psi]
  val l9: O[Psi] => O[P] = {x: O[Psi] => val y = l8(x); l7(x)(y)}
  val l10: O[Psi] => P = l9 andThen l1
  val l11: (O[Psi] => P) => Psi = fx.<-
  val l12: Psi = l11(l10)
  val l13: O[Psi] = pl.sound(l12)
  fx.->(l12)(l13)
}