Leibniz.md

// addCompilerPlugin("org.spire-math" %% "kind-projector" % "0.9.3")

import scala.language.higherKinds

trait Leibniz[A, B] {
  def subst[F[_]](fa: F[A]): F[B]
}

object Leibniz {
  implicit def ref1[A] = new Leibniz[A, A] { def subst[F[_]](fa: F[A]): F[A] = fa }

  implicit def lift[F[_], A, B](implicit AB : Leibniz[A, B]): Leibniz[F[A], F[B]] =
    AB.subst[Lambda[X => Leibniz[F[A], F[X]]]](ref1)

  implicit def swap[A, B](implicit AB : Leibniz[A, B]): Leibniz[B, A] =
    AB.subst[Leibniz[?, A]](ref1[A])

  implicit def compose[A, B, C](implicit AB : Leibniz[A, B], BC : Leibniz[B, C]): Leibniz[A, C] =
    BC.subst[Leibniz[A, ?]](AB)
}