Witnessing that there is a natural transformation between two HLists

gistfile1.scala

object WitnessNatT {
  import shapeless._
  import TypeOperators._

  trait NatTRel[L1 <: HList, F[_], L2 <: HList, G[_]]

  object NatTRel {
    type ~??>[F[_], G[_]] = {
      type λ[L1 <: HList, L2 <: HList] = NatTRel[L1, F, L2, G]
    }

    implicit def hnilUnaryTC[F[_], G[_]] = new NatTRel[HNil, F, HNil, G] {}

    implicit def hlistUnaryTC0[H1, T1 <: HList, H2, T2 <: HList, G[_]](implicit e : NatTRel[T1, Id, T2, G]) =
      new NatTRel[H1 :: T1, Id, G[H2] :: T2, G] {}

    implicit def hlistUnaryTC1[H1, T1 <: HList, F[_], H2, T2 <: HList](implicit e : NatTRel[T1, F, T2, Id]) =
      new NatTRel[F[H1] :: T1, F, H2 :: T2, Id] {}

    implicit def hlistUnaryTC2[H1, T1 <: HList, F[_], H2, T2 <: HList, G[_]](implicit e : NatTRel[T1, F, T2, G]) =
      new NatTRel[F[H1] :: T1, F, G[H2] :: T2, G] {}
  }

  import NatTRel._

  def f[L1 <: HList, L2 <: HList](l1: L1)(l2: L2)(implicit e: (Option ~??> Id)#λ[L1, L2]) = l2

  def usage = { 
    implicitly[NatTRel[Option[String] :: HNil, Option, Set[String] :: HNil, Set]]
    implicitly[NatTRel[Option[String] :: HNil, Option, String :: HNil, Id]]
    implicitly[NatTRel[String :: HNil, Id, Option[String] :: HNil, Option]]

    f((None : Option[Int]) :: Option("a") :: HNil)(1 :: "b" :: HNil)
  }
}