Add Leibniz equality

[tel]

This might fall a bit outside the standard "only the things you need" toolkit, but having a notion of Leibniz equality makes handling type equalities much easier and is useful for some pure functional idioms. Scalaz's implementation is more powerful to account for subtyping, but a simpler version might be the following

I also propose calling it something less scary than "Leibniz equality", so Teq seems reasonable.

import scala.language.higherKinds
import scala.language.implicitConversions

/**
  * `Teq[A, B]` is a witness that the types `A` and `B` are equal. It is more
  * powerful than the standard `A =:= B` since it offers the ability to
  * convert types appearing within other structures.
  */
sealed abstract class Teq[A, B] {
  def subst[F[_]](fa: F[A]): F[B]

  final def apply(a: A): B =
    Teq.witness(this)(a)

  final def andThen[C](next: B Teq C): A Teq C =
    next.subst[A Teq ?](this)

  final def compose[C](prev: C Teq A): C Teq B =
    prev andThen this

  final def from: B Teq A =
    this.subst[? Teq A](Teq.refl)

  final def lift[F[_]]: F[A] Teq F[B] =
    subst[Lambda[X => F[A] Teq F[X]]](Teq.refl)
}

object Teq {

  /**
    * The only real value of `Teq` is the statement `A Teq A`.
    */
  implicit def refl[A]: A Teq A = new Teq[A, A] {
    def subst[F[_]](fa: F[A]): F[A] = fa
  }

  /**
    * A `Teq` immediately furnishes a coercion function.
    */
  implicit def witness[A, B](t: A Teq B): A => B =
    t.subst[A => ?](identity)

  /**
    * We can convert `A Teq B` to a `A =:= B` witness via substitution.
    */
  implicit def scalaEq[A, B](t: A Teq B): A =:= B =
    t.subst[A =:= ?](implicitly[A =:= A])

}

[tpolecat]

I think both Leibniz and Lizkov from scalaz end up being useful, although maybe more for library authors than for end users. In any case 👍 from me.

[tel]

I'm a little curious about Lizkov and the subtyping parameters around Leibniz.

Also, any thoughts on TEq as the name? The other option I thought about was Is.

[adelbertc]

I've found these to be useful, 👍

As for naming, I would prefer Leibniz and Liskov if only to provide access to the general Google-able principle

[tel]

I suppose I'm not sure how that particular bikeshed is painted in Cats. A Is B reads nicely to me and I like the infix, but Leibniz is also fine in my opinion. Is it sufficient to just document the technical term?

[tel]

I'll turn this into a PR to make the discussion a bit more concrete.

[tel]

@non, to be clear, I think this is a valuable shed to paint in a project like this and I definitely defer to those familiar with the style and spirit of the project!

[peterneyens]

Added in #1178.