From 6a7d719b48e3f49189cecaf6009d80719087eb25 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sat, 18 Mar 2017 09:59:50 -0700
Subject: [PATCH 01/12] Adds an As class which represents subtyping
 relationships

This is a direct port of the Liskov class from scalaz.  I named it `As` to be
similar to our new `Is` class representing type equality, but there are aliases
named `<~<` and `Liskov`
---
 core/src/main/scala/cats/evidence/As.scala    | 268 ++++++++++++++++++
 .../main/scala/cats/evidence/package.scala    |  20 ++
 tests/src/test/scala/cats/tests/AsTests.scala |  24 ++
 3 files changed, 312 insertions(+)
 create mode 100644 core/src/main/scala/cats/evidence/As.scala
 create mode 100644 tests/src/test/scala/cats/tests/AsTests.scala

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
new file mode 100644
index 0000000000..f23fea7ed4
--- /dev/null
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -0,0 +1,268 @@
+package cats
+package evidence
+
+import arrow.Category
+
+/**
+ * As substitutability: A better `<:<`
+ * 
+ * This class exists to aid in the capture proof of subtyping
+ * relationships, which can be applied in other context to widen other
+ * type
+ *
+ * `A As B` holds whenever `A` could be used in any negative context
+ * that expects a `B`.  (e.g. if you could pass an `A` into any
+ * function that expects a `B` as input.)
+ * 
+ * This code was ported directly from scalaz to cats using this version from scalaz:
+ * https://github.com/scalaz/scalaz/blob/a89b6d63/core/src/main/scala/scalaz/As.scala
+ * 
+ *  The original contribution to scalaz came from Jason Zaugg
+ */
+sealed abstract class As[-A, +B] {
+  def apply(a: A): B = As.witness(this)(a)
+
+  /**
+   * Use this subtyping relationship to replace B with a value of type
+   * A in a contravariant context.  This would commonly be the input
+   * to a function, such as F in: `type F[-B] = B => String`. In this
+   * case, we could use A As B to turn an F[B] Into F[A].
+   */
+  def subst[F[-_]](p: F[B]): F[A]
+
+  final def andThen[C](that: As[B, C]): As[A, C] = As.trans(that, this)
+
+  final def compose[C](that: As[C, A]): As[C, B] = As.trans(this, that)
+
+  /**
+   * Use this relationship to widen the output type of a Function1
+   */
+  def onF[X](fa: X => A): X => B = As.co2_2[Function1, B, X, A](this)(fa)
+}
+
+sealed abstract class AsInstances {
+  import As._
+
+  /*
+   * Subtyping forms a category 
+   */
+  implicit val liskov: Category[<~<] = new Category[<~<] {
+    def id[A]: (A <~< A) = refl[A]
+
+    def compose[A, B, C](bc: B <~< C, ab: A <~< B): (A <~< C) = trans(bc, ab)
+  }
+}
+
+object As extends AsInstances {
+  /**
+   * Lift Scala's subtyping relationship 
+   */
+  implicit def isa[A, B >: A]: A <~< B =
+    new (A <~< B) {
+      def subst[F[-_]](p: F[B]): F[A] = p
+    }
+
+  /**
+   * We can witness the relationship by using it to make a substitution *
+   */
+  implicit def witness[A, B](lt: A <~< B): A => B = 
+    lt.subst[-? => B](identity)
+
+  /**
+   * Subtyping is reflexive 
+   */
+  implicit def refl[A]: (A <~< A) =
+    new (A <~< A) {
+      def subst[F[-_]](p: F[A]): F[A] = p
+    }
+
+  /**
+   * Subtyping is transitive 
+   */
+  def trans[A, B, C](f: B <~< C, g: A <~< B): A <~< C =
+    g.subst[λ[`-α` => α <~< C]](f)
+
+  /**
+   * We can lift subtyping into any covariant type constructor 
+   */
+  def co[T[+_], A, A2](a: A <~< A2): (T[A] <~< T[A2]) =
+    a.subst[λ[`-α` => T[α] <~< T[A2]]](refl)
+
+  // Similarly, we can do this any time we find a covariant type
+  // parameter. Here we provide the proof for what we expect to be the
+  // most common shapes.
+
+  def co2[T[+_, _], Z, A, B](a: A <~< Z): T[A, B] <~< T[Z, B] =
+    a.subst[λ[`-α` => T[α, B] <~< T[Z, B]]](refl)
+
+  /**
+   * Widen a F[X,+A] to as F[X,B] if A <~< B, this can be used to widen
+   * the output of a Function1, for example
+   */
+  def co2_2[T[_, +_], Z, A, B](a: B <~< Z): T[A, B] <~< T[A, Z] =
+    a.subst[λ[`-α` => T[A, α] <~< T[A, Z]]](refl)
+
+  def co3[T[+_, _, _], Z, A, B, C](a: A <~< Z): T[A, B, C] <~< T[Z, B, C] =
+    a.subst[λ[`-α` => T[α, B, C] <~< T[Z, B, C]]](refl)
+
+  def co4[T[+_, _, _, _], Z, A, B, C, D](a: A <~< Z): T[A, B, C, D] <~< T[Z, B, C, D] =
+    a.subst[λ[`-α` => T[α, B, C, D] <~< T[Z, B, C, D]]](refl)
+
+  /**
+   * widen two types for binary type constructors covariant in both
+   * parameters 
+   *  
+   * lift2(a,b) = co1_2(a) compose co2_2(b)
+   */
+  def lift2[T[+_, +_], A, A2, B, B2](
+    a: A <~< A2,
+    b: B <~< B2
+  ): (T[A, B] <~< T[A2, B2]) = {
+    type a[-X] = T[X, B2] <~< T[A2, B2]
+    type b[-X] = T[A, X] <~< T[A2, B2]
+    b.subst[b](a.subst[a](refl))
+  }
+
+  /**
+   * lift3(a,b,c) = co1_3(a) compose co2_3(b) compose co3_3(c) 
+   */
+  def lift3[T[+_, +_, +_], A, A2, B, B2, C, C2](
+    a: A <~< A2,
+    b: B <~< B2,
+    c: C <~< C2
+  ): (T[A, B, C] <~< T[A2, B2, C2]) = {
+    type a[-X] = T[X, B2, C2] <~< T[A2, B2, C2]
+    type b[-X] = T[A, X, C2] <~< T[A2, B2, C2]
+    type c[-X] = T[A, B, X] <~< T[A2, B2, C2]
+    c.subst[c](b.subst[b](a.subst[a](refl)))
+  }
+
+  /**
+   * lift4(a,b,c,d) = co1_3(a) compose co2_3(b) compose co3_3(c) compose co4_4(d) 
+   */
+  def lift4[T[+_, +_, +_, +_], A, A2, B, B2, C, C2, D, D2](
+    a: A <~< A2,
+    b: B <~< B2,
+    c: C <~< C2,
+    d: D <~< D2
+  ): (T[A, B, C, D] <~< T[A2, B2, C2, D2]) = {
+    type a[-X] = T[X, B2, C2, D2] <~< T[A2, B2, C2, D2]
+    type b[-X] = T[A, X, C2, D2] <~< T[A2, B2, C2, D2]
+    type c[-X] = T[A, B, X, D2] <~< T[A2, B2, C2, D2]
+    type d[-X] = T[A, B, C, X] <~< T[A2, B2, C2, D2]
+    d.subst[d](c.subst[c](b.subst[b](a.subst[a](refl))))
+  }
+
+  /**
+   *  We can lift a subtyping relationship into a contravariant type
+   *  constructor.
+   *  
+   *  Given that F has the shape: F[-_], we show that:
+   *     (A <~< B) implies (F[B] <~< F[A])
+   */
+  def contra[T[-_], A, B](a: A <~< B): (T[B] <~< T[A]) =
+    a.subst[λ[`-α` => T[B] <~< T[α]]](refl)
+
+  // Similarly, we can do this any time we find a contravariant type
+  // parameter. Here we provide the proof for what we expect to be the
+  // most common shapes.
+
+  // binary
+  def contra1_2[T[-_, _], Z, A, B](a: A <~< Z): (T[Z, B] <~< T[A, B]) =
+    a.subst[λ[`-α` => T[Z, B] <~< T[α, B]]](refl)
+
+  def contra2_2[T[_, -_], Z, A, B](a: B <~< Z): (T[A, Z] <~< T[A, B]) =
+    a.subst[λ[`-α` => T[A, Z] <~< T[A, α]]](refl)
+
+  // ternary
+  def contra1_3[T[-_, _, _], Z, A, B, C](a: A <~< Z): (T[Z, B, C] <~< T[A, B, C]) =
+    a.subst[λ[`-α` => T[Z, B, C] <~< T[α, B, C]]](refl)
+
+  def contra2_3[T[_, -_, _], Z, A, B, C](a: B <~< Z): (T[A, Z, C] <~< T[A, B, C]) =
+    a.subst[λ[`-α` => T[A, Z, C] <~< T[A, α, C]]](refl)
+
+  def contra3_3[T[_, _, -_], Z, A, B, C](a: C <~< Z): (T[A, B, Z] <~< T[A, B, C]) =
+    a.subst[λ[`-α` => T[A, B, Z] <~< T[A, B, α]]](refl)
+
+  def contra1_4[T[-_, _, _, _], Z, A, B, C, D](a: A <~< Z): (T[Z, B, C, D] <~< T[A, B, C, D]) =
+    a.subst[λ[`-α` => T[Z, B, C, D] <~< T[α, B, C, D]]](refl)
+
+  def contra2_4[T[_, -_, _, _], Z, A, B, C, D](a: B <~< Z): (T[A, Z, C, D] <~< T[A, B, C, D]) =
+    a.subst[λ[`-α` => T[A, Z, C, D] <~< T[A, α, C, D]]](refl)
+
+  def contra3_4[T[_, _, -_, _], Z, A, B, C, D](a: C <~< Z): (T[A, B, Z, D] <~< T[A, B, C, D]) =
+    a.subst[λ[`-α` => T[A, B, Z, D] <~< T[A, B, α, D]]](refl)
+
+  def contra4_4[T[_, _, _, -_], Z, A, B, C, D](a: D <~< Z): (T[A, B, C, Z] <~< T[A, B, C, D]) =
+    a.subst[λ[`-α` => T[A, B, C, Z] <~< T[A, B, C, α]]](refl)
+
+  /**
+   *  Lift subtyping into a Function1-like type
+   *  liftF1(a,r) = contra1_2(a) compose co2_2(b)
+   */
+  def liftF1[F[-_, +_], A, A2, R, R2](
+    a: A <~< A2,
+    r: R <~< R2
+  ): (F[A2, R] <~< F[A, R2]) = {
+    type a[-X] = F[A2, R2] <~< F[X, R2]
+    type r[-X] = F[A2, X] <~< F[A, R2]
+    r.subst[r](a.subst[a](refl))
+  }
+
+  /**
+   * Lift subtyping into a function
+   */
+  def liftF2[F[-_, -_, +_], A, A2, B, B2, R, R2](
+    a: A <~< A2,
+    b: B <~< B2,
+    r: R <~< R2
+  ): (F[A2, B2, R] <~< F[A, B, R2]) = {
+    type a[-X] = F[A2, B2, R2] <~< F[X, B2, R2]
+    type b[-X] = F[A2, B2, R2] <~< F[A, X, R2]
+    type r[-X] = F[A2, B2, X] <~< F[A, B, R2]
+    r.subst[r](b.subst[b](a.subst[a](refl)))
+  }
+
+  /**
+   * Lift subtyping into a function
+   * liftF3(a,b,c,r) = contra1_4(a) compose contra2_4(b) compose contra3_4(c) compose co3_4(d)
+   */
+  def liftF3[F[-_, -_, -_, +_], A, A2, B, B2, C, C2, R, R2](
+     a: A <~< A2,
+     b: B <~< B2,
+     c: C <~< C2,
+     r: R <~< R2
+  ): (F[A2, B2, C2, R] <~< F[A, B, C, R2]) = {
+    type a[-X] = F[A2, B2, C2, R2] <~< F[X, B2, C2, R2]
+    type b[-X] = F[A2, B2, C2, R2] <~< F[A, X, C2, R2]
+    type c[-X] = F[A2, B2, C2, R2] <~< F[A, B, X, R2]
+    type r[-X] = F[A2, B2, C2, X] <~< F[A, B, C, R2]
+    r.subst[r](c.subst[c](b.subst[b](a.subst[a](refl))))
+  }
+
+  /**
+   * Lift subtyping into a function 
+   */
+  def liftF4[F[-_, -_, -_, -_, +_], A, A2, B, B2, C, C2, D, D2, R, R2](
+     a: A <~< A2,
+     b: B <~< B2,
+     c: C <~< C2,
+     d: D <~< D2,
+     r: R <~< R2
+   ): (F[A2, B2, C2, D2, R] <~< F[A, B, C, D, R2]) = {
+    type a[-X] = F[A2, B2, C2, D2, R2] <~< F[X, B2, C2, D2, R2]
+    type b[-X] = F[A2, B2, C2, D2, R2] <~< F[A, X, C2, D2, R2]
+    type c[-X] = F[A2, B2, C2, D2, R2] <~< F[A, B, X, D2, R2]
+    type d[-X] = F[A2, B2, C2, D2, R2] <~< F[A, B, C, X, R2]
+    type r[-X] = F[A2, B2, C2, D2, X] <~< F[A, B, C, D, R2]
+    r.subst[r](d.subst[d](c.subst[c](b.subst[b](a.subst[a](refl)))))
+  }
+
+  /**
+   * Unsafely force a claim that A is a subtype of B 
+   */
+  def force[A, B]: A <~< B =
+    new (A <~< B) {
+      def subst[F[-_]](p: F[B]): F[A] = p.asInstanceOf[F[A]]
+    }
+}
diff --git a/core/src/main/scala/cats/evidence/package.scala b/core/src/main/scala/cats/evidence/package.scala
index 152af76433..12ac1fc4d3 100644
--- a/core/src/main/scala/cats/evidence/package.scala
+++ b/core/src/main/scala/cats/evidence/package.scala
@@ -2,4 +2,24 @@ package cats
 
 package object evidence {
   type Leibniz[A, B] = cats.evidence.Is[A, B]
+
+  /**
+   * A convenient type alias for As, this declares that A is a
+   * subtype of B, and should be able to be  a B is
+   * expected.
+   */
+  type <~<[-A, +B] = A As B
+
+  /** 
+   * A flipped alias, for those used to their arrows running left to right 
+   */
+  type >~>[+B, -A] = A As B
+
+  /**
+   * The property that a value of type A can be used in a context
+   * expecting a B if A <~< B is refered to as the "Liskov
+   * Substitution Principal", which is named for Barbara Liskov:
+   * https://en.wikipedia.org/wiki/Barbara_Liskov
+   */
+  type Liskov[-A, +B] = A As B
 }
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
new file mode 100644
index 0000000000..b09fb54fb0
--- /dev/null
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -0,0 +1,24 @@
+package cats
+package tests
+
+class AsTests extends CatsSuite {
+  import evidence._
+
+  def toMap[A, B, X](fa: List[X])(implicit ev: X <~< (A,B)): Map[A,B] =
+    fa.foldLeft(Map.empty[A,B])(As.contra2_3(ev)(_ + _))
+
+  test("narrow an input of a function2") {
+    // scala's GenTraversableOnce#toMap has a similar <:< constraint
+
+    toMap(List("String" -> 1))
+  }
+
+  test("lift <:") {
+    // scala's GenTraversableOnce#toMap has a similar <:< constraint
+    trait A
+    case class Foo(x: Int) extends A
+
+    val lifted: Foo <~< A = As.isa[Foo,A]
+    toMap(List("String" -> Foo(1)))(As.co2_2(lifted))
+  }
+}

From 974bdf5a8d83aee1d7bf1bd83d58306d4085cbb5 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 19 Mar 2017 01:19:05 -0700
Subject: [PATCH 02/12] incorporate suggestions from Oscar (Thanksgit diff
 --cached)git

---
 core/src/main/scala/cats/evidence/As.scala    | 247 +++++++-----------
 tests/src/test/scala/cats/tests/AsTests.scala |   2 +-
 2 files changed, 91 insertions(+), 158 deletions(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index f23fea7ed4..32f432602c 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -5,7 +5,7 @@ import arrow.Category
 
 /**
  * As substitutability: A better `<:<`
- * 
+ *
  * This class exists to aid in the capture proof of subtyping
  * relationships, which can be applied in other context to widen other
  * type
@@ -13,214 +13,172 @@ import arrow.Category
  * `A As B` holds whenever `A` could be used in any negative context
  * that expects a `B`.  (e.g. if you could pass an `A` into any
  * function that expects a `B` as input.)
- * 
+ *
  * This code was ported directly from scalaz to cats using this version from scalaz:
  * https://github.com/scalaz/scalaz/blob/a89b6d63/core/src/main/scala/scalaz/As.scala
- * 
+ *
  *  The original contribution to scalaz came from Jason Zaugg
  */
-sealed abstract class As[-A, +B] {
-  def apply(a: A): B = As.witness(this)(a)
-
+sealed abstract class As[-A, +B] extends Serializable {
   /**
    * Use this subtyping relationship to replace B with a value of type
    * A in a contravariant context.  This would commonly be the input
    * to a function, such as F in: `type F[-B] = B => String`. In this
    * case, we could use A As B to turn an F[B] Into F[A].
    */
-  def subst[F[-_]](p: F[B]): F[A]
+  def substitute[F[-_]](p: F[B]): F[A]
 
-  final def andThen[C](that: As[B, C]): As[A, C] = As.trans(that, this)
+  @inline final def andThen[C](that: (B As C)): (A As C) = As.compose(that, this)
 
-  final def compose[C](that: As[C, A]): As[C, B] = As.trans(this, that)
+  @inline final def compose[C](that: (C As A)): (C As B) = As.compose(this, that)
 
-  /**
-   * Use this relationship to widen the output type of a Function1
-   */
-  def onF[X](fa: X => A): X => B = As.co2_2[Function1, B, X, A](this)(fa)
+  @inline final def coerce(a: A): B = As.witness(this)(a)
 }
 
 sealed abstract class AsInstances {
   import As._
 
   /*
-   * Subtyping forms a category 
+   * Subtyping forms a category
    */
-  implicit val liskov: Category[<~<] = new Category[<~<] {
-    def id[A]: (A <~< A) = refl[A]
+  implicit val liskov: Category[As] = new Category[As] {
+    def id[A]: (A As A) = refl[A]
 
-    def compose[A, B, C](bc: B <~< C, ab: A <~< B): (A <~< C) = trans(bc, ab)
+    def compose[A, B, C](bc: B As C, ab: A As B): (A As C) = bc compose ab
   }
 }
 
 object As extends AsInstances {
   /**
-   * Lift Scala's subtyping relationship 
+   * In truth, "all values of `A Is B` are `refl`". `reflAny` is that
+   * single value.
+   */
+  private[this] val reflAny = new (Any As Any) {
+    def substitute[F[-_]](fa: F[Any]) = fa
+  }
+  /**
+   * Subtyping is reflexive
    */
-  implicit def isa[A, B >: A]: A <~< B =
-    new (A <~< B) {
-      def subst[F[-_]](p: F[B]): F[A] = p
-    }
+  implicit def refl[A]: (A As A) =
+    reflAny.asInstanceOf[A As A]
 
   /**
    * We can witness the relationship by using it to make a substitution *
    */
   implicit def witness[A, B](lt: A <~< B): A => B = 
-    lt.subst[-? => B](identity)
+    lt.substitute[-? => B](identity)
 
   /**
-   * Subtyping is reflexive 
+   * Subtyping is transitive
    */
-  implicit def refl[A]: (A <~< A) =
-    new (A <~< A) {
-      def subst[F[-_]](p: F[A]): F[A] = p
-    }
+  def compose[A, B, C](f: B <~< C, g: A <~< B): A <~< C =
+    g.substitute[λ[`-α` => α <~< C]](f)
 
   /**
-   * Subtyping is transitive 
+   * Lift Scala's subtyping relationship
    */
-  def trans[A, B, C](f: B <~< C, g: A <~< B): A <~< C =
-    g.subst[λ[`-α` => α <~< C]](f)
+  @inline def unsafeFromPredef[A, B >: A]: (A As B) =
+    reflAny.asInstanceOf[A As B]
 
   /**
-   * We can lift subtyping into any covariant type constructor 
+   * We can lift subtyping into any covariant type constructor
    */
-  def co[T[+_], A, A2](a: A <~< A2): (T[A] <~< T[A2]) =
-    a.subst[λ[`-α` => T[α] <~< T[A2]]](refl)
+  def co[T[+_], A, A2] (a: A As A2): (T[A] As T[A2]) =
+    a.substitute[λ[`-α` => T[α] As T[A2]]](refl)
 
   // Similarly, we can do this any time we find a covariant type
   // parameter. Here we provide the proof for what we expect to be the
   // most common shapes.
 
-  def co2[T[+_, _], Z, A, B](a: A <~< Z): T[A, B] <~< T[Z, B] =
-    a.subst[λ[`-α` => T[α, B] <~< T[Z, B]]](refl)
+  def co2[T[+_, _], Z, A, B](a: A As Z): T[A, B] As T[Z, B] =
+    a.substitute[λ[`-α` => T[α, B] As T[Z, B]]](refl)
 
   /**
-   * Widen a F[X,+A] to as F[X,B] if A <~< B, this can be used to widen
-   * the output of a Function1, for example
+   * Widen a F[X,+A] to a F[X,B] if (A As B). This can be used to widen
+   * the output of a Function1, for example.
    */
-  def co2_2[T[_, +_], Z, A, B](a: B <~< Z): T[A, B] <~< T[A, Z] =
-    a.subst[λ[`-α` => T[A, α] <~< T[A, Z]]](refl)
+  def co2_2[T[_, +_], Z, A, B](a: B As Z): T[A, B] As T[A, Z] =
+    a.substitute[λ[`-α` => T[A, α] As T[A, Z]]](refl)
 
-  def co3[T[+_, _, _], Z, A, B, C](a: A <~< Z): T[A, B, C] <~< T[Z, B, C] =
-    a.subst[λ[`-α` => T[α, B, C] <~< T[Z, B, C]]](refl)
+  def co3[T[+_, _, _], Z, A, B, C](a: A As Z): T[A, B, C] As T[Z, B, C] =
+    a.substitute[λ[`-α` => T[α, B, C] As T[Z, B, C]]](refl)
 
-  def co4[T[+_, _, _, _], Z, A, B, C, D](a: A <~< Z): T[A, B, C, D] <~< T[Z, B, C, D] =
-    a.subst[λ[`-α` => T[α, B, C, D] <~< T[Z, B, C, D]]](refl)
+  /**
+   * Use this relationship to widen the output type of a Function1
+   */
+  def onF[X, A, B](ev: A As B)(fa: X => A): X => B = co2_2[Function1, B, X, A](ev).coerce(fa)
 
   /**
    * widen two types for binary type constructors covariant in both
-   * parameters 
-   *  
+   * parameters
+   *
    * lift2(a,b) = co1_2(a) compose co2_2(b)
    */
   def lift2[T[+_, +_], A, A2, B, B2](
-    a: A <~< A2,
-    b: B <~< B2
-  ): (T[A, B] <~< T[A2, B2]) = {
-    type a[-X] = T[X, B2] <~< T[A2, B2]
-    type b[-X] = T[A, X] <~< T[A2, B2]
-    b.subst[b](a.subst[a](refl))
-  }
-
-  /**
-   * lift3(a,b,c) = co1_3(a) compose co2_3(b) compose co3_3(c) 
-   */
-  def lift3[T[+_, +_, +_], A, A2, B, B2, C, C2](
-    a: A <~< A2,
-    b: B <~< B2,
-    c: C <~< C2
-  ): (T[A, B, C] <~< T[A2, B2, C2]) = {
-    type a[-X] = T[X, B2, C2] <~< T[A2, B2, C2]
-    type b[-X] = T[A, X, C2] <~< T[A2, B2, C2]
-    type c[-X] = T[A, B, X] <~< T[A2, B2, C2]
-    c.subst[c](b.subst[b](a.subst[a](refl)))
-  }
-
-  /**
-   * lift4(a,b,c,d) = co1_3(a) compose co2_3(b) compose co3_3(c) compose co4_4(d) 
-   */
-  def lift4[T[+_, +_, +_, +_], A, A2, B, B2, C, C2, D, D2](
-    a: A <~< A2,
-    b: B <~< B2,
-    c: C <~< C2,
-    d: D <~< D2
-  ): (T[A, B, C, D] <~< T[A2, B2, C2, D2]) = {
-    type a[-X] = T[X, B2, C2, D2] <~< T[A2, B2, C2, D2]
-    type b[-X] = T[A, X, C2, D2] <~< T[A2, B2, C2, D2]
-    type c[-X] = T[A, B, X, D2] <~< T[A2, B2, C2, D2]
-    type d[-X] = T[A, B, C, X] <~< T[A2, B2, C2, D2]
-    d.subst[d](c.subst[c](b.subst[b](a.subst[a](refl))))
+    a: A As A2,
+    b: B As B2
+  ): (T[A, B] As T[A2, B2]) = {
+    type a[-X] = T[X, B2] As T[A2, B2]
+    type b[-X] = T[A, X] As T[A2, B2]
+    b.substitute[b](a.substitute[a](refl))
   }
 
   /**
    *  We can lift a subtyping relationship into a contravariant type
    *  constructor.
-   *  
+   *
    *  Given that F has the shape: F[-_], we show that:
-   *     (A <~< B) implies (F[B] <~< F[A])
+   *     (A As B) implies (F[B] As F[A])
    */
-  def contra[T[-_], A, B](a: A <~< B): (T[B] <~< T[A]) =
-    a.subst[λ[`-α` => T[B] <~< T[α]]](refl)
+  def contra[T[-_], A, B](a: A As B): (T[B] As T[A]) =
+    a.substitute[λ[`-α` => T[B] As T[α]]](refl)
 
   // Similarly, we can do this any time we find a contravariant type
   // parameter. Here we provide the proof for what we expect to be the
   // most common shapes.
 
   // binary
-  def contra1_2[T[-_, _], Z, A, B](a: A <~< Z): (T[Z, B] <~< T[A, B]) =
-    a.subst[λ[`-α` => T[Z, B] <~< T[α, B]]](refl)
+  def contra1_2[T[-_, _], Z, A, B](a: A As Z): (T[Z, B] As T[A, B]) =
+    a.substitute[λ[`-α` => T[Z, B] As T[α, B]]](refl)
 
-  def contra2_2[T[_, -_], Z, A, B](a: B <~< Z): (T[A, Z] <~< T[A, B]) =
-    a.subst[λ[`-α` => T[A, Z] <~< T[A, α]]](refl)
+  def contra2_2[T[_, -_], Z, A, B](a: B As Z): (T[A, Z] As T[A, B]) =
+    a.substitute[λ[`-α` => T[A, Z] As T[A, α]]](refl)
 
   // ternary
-  def contra1_3[T[-_, _, _], Z, A, B, C](a: A <~< Z): (T[Z, B, C] <~< T[A, B, C]) =
-    a.subst[λ[`-α` => T[Z, B, C] <~< T[α, B, C]]](refl)
-
-  def contra2_3[T[_, -_, _], Z, A, B, C](a: B <~< Z): (T[A, Z, C] <~< T[A, B, C]) =
-    a.subst[λ[`-α` => T[A, Z, C] <~< T[A, α, C]]](refl)
-
-  def contra3_3[T[_, _, -_], Z, A, B, C](a: C <~< Z): (T[A, B, Z] <~< T[A, B, C]) =
-    a.subst[λ[`-α` => T[A, B, Z] <~< T[A, B, α]]](refl)
-
-  def contra1_4[T[-_, _, _, _], Z, A, B, C, D](a: A <~< Z): (T[Z, B, C, D] <~< T[A, B, C, D]) =
-    a.subst[λ[`-α` => T[Z, B, C, D] <~< T[α, B, C, D]]](refl)
+  def contra1_3[T[-_, _, _], Z, A, B, C](a: A As Z): (T[Z, B, C] As T[A, B, C]) =
+    a.substitute[λ[`-α` => T[Z, B, C] As T[α, B, C]]](refl)
 
-  def contra2_4[T[_, -_, _, _], Z, A, B, C, D](a: B <~< Z): (T[A, Z, C, D] <~< T[A, B, C, D]) =
-    a.subst[λ[`-α` => T[A, Z, C, D] <~< T[A, α, C, D]]](refl)
+  def contra2_3[T[_, -_, _], Z, A, B, C](a: B As Z): (T[A, Z, C] As T[A, B, C]) =
+    a.substitute[λ[`-α` => T[A, Z, C] As T[A, α, C]]](refl)
 
-  def contra3_4[T[_, _, -_, _], Z, A, B, C, D](a: C <~< Z): (T[A, B, Z, D] <~< T[A, B, C, D]) =
-    a.subst[λ[`-α` => T[A, B, Z, D] <~< T[A, B, α, D]]](refl)
-
-  def contra4_4[T[_, _, _, -_], Z, A, B, C, D](a: D <~< Z): (T[A, B, C, Z] <~< T[A, B, C, D]) =
-    a.subst[λ[`-α` => T[A, B, C, Z] <~< T[A, B, C, α]]](refl)
+  def contra3_3[T[_, _, -_], Z, A, B, C](a: C As Z): (T[A, B, Z] As T[A, B, C]) =
+    a.substitute[λ[`-α` => T[A, B, Z] As T[A, B, α]]](refl)
 
   /**
    *  Lift subtyping into a Function1-like type
    *  liftF1(a,r) = contra1_2(a) compose co2_2(b)
    */
   def liftF1[F[-_, +_], A, A2, R, R2](
-    a: A <~< A2,
-    r: R <~< R2
-  ): (F[A2, R] <~< F[A, R2]) = {
-    type a[-X] = F[A2, R2] <~< F[X, R2]
-    type r[-X] = F[A2, X] <~< F[A, R2]
-    r.subst[r](a.subst[a](refl))
+    a: A As A2,
+    r: R As R2
+  ): (F[A2, R] As F[A, R2]) = {
+    type a[-X] = F[A2, R2] As F[X, R2]
+    type r[-X] = F[A2, X] As F[A, R2]
+    r.substitute[r](a.substitute[a](refl))
   }
 
   /**
    * Lift subtyping into a function
    */
   def liftF2[F[-_, -_, +_], A, A2, B, B2, R, R2](
-    a: A <~< A2,
-    b: B <~< B2,
-    r: R <~< R2
-  ): (F[A2, B2, R] <~< F[A, B, R2]) = {
-    type a[-X] = F[A2, B2, R2] <~< F[X, B2, R2]
-    type b[-X] = F[A2, B2, R2] <~< F[A, X, R2]
-    type r[-X] = F[A2, B2, X] <~< F[A, B, R2]
-    r.subst[r](b.subst[b](a.subst[a](refl)))
+    a: A As A2,
+    b: B As B2,
+    r: R As R2
+  ): (F[A2, B2, R] As F[A, B, R2]) = {
+    type a[-X] = F[A2, B2, R2] As F[X, B2, R2]
+    type b[-X] = F[A2, B2, R2] As F[A, X, R2]
+    type r[-X] = F[A2, B2, X] As F[A, B, R2]
+    r.substitute[r](b.substitute[b](a.substitute[a](refl)))
   }
 
   /**
@@ -228,41 +186,16 @@ object As extends AsInstances {
    * liftF3(a,b,c,r) = contra1_4(a) compose contra2_4(b) compose contra3_4(c) compose co3_4(d)
    */
   def liftF3[F[-_, -_, -_, +_], A, A2, B, B2, C, C2, R, R2](
-     a: A <~< A2,
-     b: B <~< B2,
-     c: C <~< C2,
-     r: R <~< R2
-  ): (F[A2, B2, C2, R] <~< F[A, B, C, R2]) = {
-    type a[-X] = F[A2, B2, C2, R2] <~< F[X, B2, C2, R2]
-    type b[-X] = F[A2, B2, C2, R2] <~< F[A, X, C2, R2]
-    type c[-X] = F[A2, B2, C2, R2] <~< F[A, B, X, R2]
-    type r[-X] = F[A2, B2, C2, X] <~< F[A, B, C, R2]
-    r.subst[r](c.subst[c](b.subst[b](a.subst[a](refl))))
+     a: A As A2,
+     b: B As B2,
+     c: C As C2,
+     r: R As R2
+  ): (F[A2, B2, C2, R] As F[A, B, C, R2]) = {
+    type a[-X] = F[A2, B2, C2, R2] As F[X, B2, C2, R2]
+    type b[-X] = F[A2, B2, C2, R2] As F[A, X, C2, R2]
+    type c[-X] = F[A2, B2, C2, R2] As F[A, B, X, R2]
+    type r[-X] = F[A2, B2, C2, X] As F[A, B, C, R2]
+    r.substitute[r](c.substitute[c](b.substitute[b](a.substitute[a](refl))))
   }
 
-  /**
-   * Lift subtyping into a function 
-   */
-  def liftF4[F[-_, -_, -_, -_, +_], A, A2, B, B2, C, C2, D, D2, R, R2](
-     a: A <~< A2,
-     b: B <~< B2,
-     c: C <~< C2,
-     d: D <~< D2,
-     r: R <~< R2
-   ): (F[A2, B2, C2, D2, R] <~< F[A, B, C, D, R2]) = {
-    type a[-X] = F[A2, B2, C2, D2, R2] <~< F[X, B2, C2, D2, R2]
-    type b[-X] = F[A2, B2, C2, D2, R2] <~< F[A, X, C2, D2, R2]
-    type c[-X] = F[A2, B2, C2, D2, R2] <~< F[A, B, X, D2, R2]
-    type d[-X] = F[A2, B2, C2, D2, R2] <~< F[A, B, C, X, R2]
-    type r[-X] = F[A2, B2, C2, D2, X] <~< F[A, B, C, D, R2]
-    r.subst[r](d.subst[d](c.subst[c](b.subst[b](a.subst[a](refl)))))
-  }
-
-  /**
-   * Unsafely force a claim that A is a subtype of B 
-   */
-  def force[A, B]: A <~< B =
-    new (A <~< B) {
-      def subst[F[-_]](p: F[B]): F[A] = p.asInstanceOf[F[A]]
-    }
 }
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index b09fb54fb0..b1971f1b95 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -18,7 +18,7 @@ class AsTests extends CatsSuite {
     trait A
     case class Foo(x: Int) extends A
 
-    val lifted: Foo <~< A = As.isa[Foo,A]
+    val lifted: Foo <~< A = As.unsafeFromPredef[Foo,A]
     toMap(List("String" -> Foo(1)))(As.co2_2(lifted))
   }
 }

From 03411c15ae0798fb0c32a74378da17cef5b58392 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 19 Mar 2017 01:21:06 -0700
Subject: [PATCH 03/12] delete-trailing-whitespace

---
 core/src/main/scala/cats/evidence/As.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index 32f432602c..a481a311e3 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -65,7 +65,7 @@ object As extends AsInstances {
   /**
    * We can witness the relationship by using it to make a substitution *
    */
-  implicit def witness[A, B](lt: A <~< B): A => B = 
+  implicit def witness[A, B](lt: A <~< B): A => B =
     lt.substitute[-? => B](identity)
 
   /**

From 399dce328eb48e307d329413c1b1c0c6a3a6f1a7 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 19 Mar 2017 08:59:00 -0700
Subject: [PATCH 04/12] Minor changes to evidence/packages.scala

remove explicit reference to package in Is type alias (for posco)
add === type alias for `Is` (for sellout)
---
 core/src/main/scala/cats/evidence/package.scala | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/core/src/main/scala/cats/evidence/package.scala b/core/src/main/scala/cats/evidence/package.scala
index 12ac1fc4d3..dc471f8ad0 100644
--- a/core/src/main/scala/cats/evidence/package.scala
+++ b/core/src/main/scala/cats/evidence/package.scala
@@ -1,7 +1,18 @@
 package cats
 
 package object evidence {
-  type Leibniz[A, B] = cats.evidence.Is[A, B]
+  /**
+   * A convenient type alias for Is, which declares that A is the same
+   * type as B.
+   */
+  type ===[A, B] = A Is B
+
+  /**
+   * This type level equality represented by `Is` is referred to as
+   * "Leibniz equality", and it had the name "Leibniz" in the scalaz
+   *  https://en.wikipedia.org/wiki/Gottfried_Wilhelm_Leibniz
+   */
+  type Leibniz[A, B] = A Is B
 
   /**
    * A convenient type alias for As, this declares that A is a

From fbee74bbc555583722eee745977d26f1d158ec6b Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sat, 25 Mar 2017 11:50:14 -0700
Subject: [PATCH 05/12] More enhancements for posco's feedback (thanks!)

- change unsafeFromPredef to just use refl
- add tests for some expected relationships such as Int <~< Any,
  and List[String] <~< List[Any]
---
 core/src/main/scala/cats/evidence/As.scala      | 3 +--
 core/src/main/scala/cats/evidence/package.scala | 4 ++--
 tests/src/test/scala/cats/tests/AsTests.scala   | 8 ++++++++
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index a481a311e3..5ae1095602 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -77,8 +77,7 @@ object As extends AsInstances {
   /**
    * Lift Scala's subtyping relationship
    */
-  @inline def unsafeFromPredef[A, B >: A]: (A As B) =
-    reflAny.asInstanceOf[A As B]
+  @inline def unsafeFromPredef[A, B >: A]: (A As B) = refl
 
   /**
    * We can lift subtyping into any covariant type constructor
diff --git a/core/src/main/scala/cats/evidence/package.scala b/core/src/main/scala/cats/evidence/package.scala
index dc471f8ad0..518e6f7024 100644
--- a/core/src/main/scala/cats/evidence/package.scala
+++ b/core/src/main/scala/cats/evidence/package.scala
@@ -21,8 +21,8 @@ package object evidence {
    */
   type <~<[-A, +B] = A As B
 
-  /** 
-   * A flipped alias, for those used to their arrows running left to right 
+  /**
+   * A flipped alias, for those used to their arrows running left to right
    */
   type >~>[+B, -A] = A As B
 
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index b1971f1b95..2ffab33718 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -21,4 +21,12 @@ class AsTests extends CatsSuite {
     val lifted: Foo <~< A = As.unsafeFromPredef[Foo,A]
     toMap(List("String" -> Foo(1)))(As.co2_2(lifted))
   }
+
+  test("check expected relationships") {
+    // scala's GenTraversableOnce#toMap has a similar <:< constraint
+    implicitly[Int <~< Any]
+    implicitly[String <~< Any]
+    implicitly[String <~< AnyRef]
+    implicitly[scala.collection.immutable.List[String] <~< scala.collection.Seq[Any]]
+  }
 }

From 7ffa0db139f20d18b731b53fddd366754248b599 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sat, 25 Mar 2017 12:00:46 -0700
Subject: [PATCH 06/12] ome more

---
 tests/src/test/scala/cats/tests/AsTests.scala | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index 2ffab33718..3c0514adea 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -27,6 +27,8 @@ class AsTests extends CatsSuite {
     implicitly[Int <~< Any]
     implicitly[String <~< Any]
     implicitly[String <~< AnyRef]
+    implicitly[String <~< AnyRef]
+    implicitly[(String,Int) <~< (AnyRef,Any)]
     implicitly[scala.collection.immutable.List[String] <~< scala.collection.Seq[Any]]
   }
 }

From 4e59c6ea2e224480ce8abeb9087faebe37ed732d Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 16 Apr 2017 11:18:04 -0700
Subject: [PATCH 07/12] add more tests, contravariant tests still pending

---
 core/src/main/scala/cats/evidence/As.scala    | 25 ++++++++--
 tests/src/test/scala/cats/tests/AsTests.scala | 48 +++++++++++++++++--
 2 files changed, 65 insertions(+), 8 deletions(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index 5ae1095602..a45560e812 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -65,19 +65,28 @@ object As extends AsInstances {
   /**
    * We can witness the relationship by using it to make a substitution *
    */
-  implicit def witness[A, B](lt: A <~< B): A => B =
+  implicit def witness[A, B](lt: A As B): A => B =
     lt.substitute[-? => B](identity)
 
   /**
    * Subtyping is transitive
    */
-  def compose[A, B, C](f: B <~< C, g: A <~< B): A <~< C =
-    g.substitute[λ[`-α` => α <~< C]](f)
+  def compose[A, B, C](f: B As C, g: A As B): A As C =
+    g.substitute[λ[`-α` => α As C]](f)
 
   /**
-   * Lift Scala's subtyping relationship
+   * reify a subtype relationship as a Liskov relaationship
    */
-  @inline def unsafeFromPredef[A, B >: A]: (A As B) = refl
+  @inline def reify[A, B >: A]: (A As B) = refl
+
+  /**
+    * It can be convenient to convert a [[<:<]] value into a `<~<` value.
+    * This is not strictly valid as while it is almost certainly true that
+    * `A <:< B` implies `A <~< B` it is not the case that you can create
+    * evidence of `A <~< B` except via a coercion. Use responsibly.
+    */
+  def fromPredef[A, B](eq: A <:< B): A As B =
+    reflAny.asInstanceOf[A As B]
 
   /**
    * We can lift subtyping into any covariant type constructor
@@ -102,6 +111,12 @@ object As extends AsInstances {
   def co3[T[+_, _, _], Z, A, B, C](a: A As Z): T[A, B, C] As T[Z, B, C] =
     a.substitute[λ[`-α` => T[α, B, C] As T[Z, B, C]]](refl)
 
+  def co3_2[T[_, +_, _], Z, A, B, C](a: B As Z): T[A, B, C] As T[A, Z, C] =
+    a.substitute[λ[`-α` => T[A, α, C] As T[A, Z, C]]](refl)
+
+  def co3_3[T[+_, _, +_], Z, A, B, C](a: C As Z): T[A, B, C] As T[A, B, Z] =
+    a.substitute[λ[`-α` => T[A, B, α] As T[A, B, Z]]](refl)
+
   /**
    * Use this relationship to widen the output type of a Function1
    */
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index 3c0514adea..298af2be1c 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -15,10 +15,10 @@ class AsTests extends CatsSuite {
 
   test("lift <:") {
     // scala's GenTraversableOnce#toMap has a similar <:< constraint
-    trait A
-    case class Foo(x: Int) extends A
+    trait Bar
+    case class Foo(x: Int) extends Bar
 
-    val lifted: Foo <~< A = As.unsafeFromPredef[Foo,A]
+    val lifted: Foo <~< Bar = As.reify[Foo, Bar]
     toMap(List("String" -> Foo(1)))(As.co2_2(lifted))
   }
 
@@ -31,4 +31,46 @@ class AsTests extends CatsSuite {
     implicitly[(String,Int) <~< (AnyRef,Any)]
     implicitly[scala.collection.immutable.List[String] <~< scala.collection.Seq[Any]]
   }
+
+  trait Top {
+    def foo: String = this.getClass.getName
+  }
+  trait Middle extends Top
+  case class Bottom() extends Middle
+
+  test("subtyping relationships compose") {
+
+    val cAsB: Bottom As Middle = As.reify[Bottom,Middle]
+    val bAsA: Middle As Top = As.fromPredef(implicitly)
+
+    val one: Bottom As Top = cAsB andThen bAsA
+    val two: Bottom As Top = bAsA compose cAsB 
+  }
+
+
+  test("we can use As to coerce a value") {
+    val cAsA: Bottom As Top = implicitly
+
+    val c: Bottom = Bottom()
+
+    val a: Top = cAsA.coerce(c)
+    a.foo
+  }
+
+  test("we can lift subtyping to covariant type constructors") {
+    val cAsA: Bottom As Top = implicitly
+    val co: List[Bottom] As List[Top] = As.co(cAsA)
+    val co2: ((Bottom, String) As (Top, String)) = As.co2(cAsA)
+    val co2_2: ((String, Bottom) As (String, Top)) = As.co2_2(cAsA)
+    val co3: ((Bottom, Unit, Unit) As (Top, Unit, Unit)) = As.co3(cAsA)
+    val co3_2: ((Unit, Bottom, Unit) As (Unit, Top, Unit)) = As.co3_2(cAsA)
+    val co3_3: ((Unit, Unit, Bottom) As (Unit, Unit, Top)) = As.co3_3(cAsA)
+    val lift2: ((Bottom, String) As (Top,Any)) = As.lift2(cAsA,implicitly)
+  }
+
+  test("we can widen a function1") {
+    val f: Any => Bottom = _ => Bottom()
+    val cAsA: Bottom As Top = implicitly
+    val f2: Any => Top = As.onF(cAsA)(f)
+  }
 }

From 5be603707ff6a9d873f7a5e962afbc85cfcaeca1 Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 16 Apr 2017 15:00:29 -0700
Subject: [PATCH 08/12] add contra tests and get rid fo the liftF like
 functions (they can be derrived from what we have, and I can't find anyone
 using them in the wild)

---
 core/src/main/scala/cats/evidence/As.scala    | 45 -------------------
 tests/src/test/scala/cats/tests/AsTests.scala | 21 +++++++++
 2 files changed, 21 insertions(+), 45 deletions(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index a45560e812..9265bb72a9 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -167,49 +167,4 @@ object As extends AsInstances {
 
   def contra3_3[T[_, _, -_], Z, A, B, C](a: C As Z): (T[A, B, Z] As T[A, B, C]) =
     a.substitute[λ[`-α` => T[A, B, Z] As T[A, B, α]]](refl)
-
-  /**
-   *  Lift subtyping into a Function1-like type
-   *  liftF1(a,r) = contra1_2(a) compose co2_2(b)
-   */
-  def liftF1[F[-_, +_], A, A2, R, R2](
-    a: A As A2,
-    r: R As R2
-  ): (F[A2, R] As F[A, R2]) = {
-    type a[-X] = F[A2, R2] As F[X, R2]
-    type r[-X] = F[A2, X] As F[A, R2]
-    r.substitute[r](a.substitute[a](refl))
-  }
-
-  /**
-   * Lift subtyping into a function
-   */
-  def liftF2[F[-_, -_, +_], A, A2, B, B2, R, R2](
-    a: A As A2,
-    b: B As B2,
-    r: R As R2
-  ): (F[A2, B2, R] As F[A, B, R2]) = {
-    type a[-X] = F[A2, B2, R2] As F[X, B2, R2]
-    type b[-X] = F[A2, B2, R2] As F[A, X, R2]
-    type r[-X] = F[A2, B2, X] As F[A, B, R2]
-    r.substitute[r](b.substitute[b](a.substitute[a](refl)))
-  }
-
-  /**
-   * Lift subtyping into a function
-   * liftF3(a,b,c,r) = contra1_4(a) compose contra2_4(b) compose contra3_4(c) compose co3_4(d)
-   */
-  def liftF3[F[-_, -_, -_, +_], A, A2, B, B2, C, C2, R, R2](
-     a: A As A2,
-     b: B As B2,
-     c: C As C2,
-     r: R As R2
-  ): (F[A2, B2, C2, R] As F[A, B, C, R2]) = {
-    type a[-X] = F[A2, B2, C2, R2] As F[X, B2, C2, R2]
-    type b[-X] = F[A2, B2, C2, R2] As F[A, X, C2, R2]
-    type c[-X] = F[A2, B2, C2, R2] As F[A, B, X, R2]
-    type r[-X] = F[A2, B2, C2, X] As F[A, B, C, R2]
-    r.substitute[r](c.substitute[c](b.substitute[b](a.substitute[a](refl))))
-  }
-
 }
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index 298af2be1c..e0a702d6ba 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -68,9 +68,30 @@ class AsTests extends CatsSuite {
     val lift2: ((Bottom, String) As (Top,Any)) = As.lift2(cAsA,implicitly)
   }
 
+  test("we can lift subtyping to contravariant type constructors") {
+    type Eat[-A] = A => Unit
+    type EatF[-A, B] = A => B
+    type Eatꟻ[B, -A] = A => B
+    type EatF13[-A, B, C] = A => (B, C)
+    type EatF23[B, -A, C] = A => (B, C)
+    type EatF33[B, C, -A] = A => (B, C)
+
+    val cAsA: (Bottom As Top) = implicitly
+    val contra: Eat[Top] As Eat[Bottom] = As.contra(cAsA)
+    val contra1_2: EatF[Top, Unit] As EatF[Bottom,Unit] = As.contra1_2(cAsA)
+    val contra2_2: Eatꟻ[Unit, Top] As Eatꟻ[Unit,Bottom] = As.contra2_2(cAsA)
+    val contra1_3: EatF13[Top, Unit,Unit] As EatF13[Bottom, Unit, Unit] = As.contra1_3(cAsA)
+    val contra2_3: EatF23[Unit, Top, Unit] As EatF23[Unit, Bottom, Unit] = As.contra2_3(cAsA)
+    val contra3_3: EatF33[Unit, Unit, Top] As EatF33[Unit, Unit, Bottom] = As.contra3_3(cAsA)
+  }
+
   test("we can widen a function1") {
     val f: Any => Bottom = _ => Bottom()
     val cAsA: Bottom As Top = implicitly
     val f2: Any => Top = As.onF(cAsA)(f)
   }
+
+  test("we can simultaneously narrow the input and widen the ouptut of a Function1") {
+
+  }
 }

From 2c9b8b0605af345a7194322576debb7d4b65141a Mon Sep 17 00:00:00 2001
From: Stew O'Connor <michaelx.oconnor@oncue.com>
Date: Sun, 16 Apr 2017 16:18:06 -0700
Subject: [PATCH 09/12] don't try to link the type in the scaladoc

---
 core/src/main/scala/cats/evidence/As.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index 9265bb72a9..cebcd08135 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -80,7 +80,7 @@ object As extends AsInstances {
   @inline def reify[A, B >: A]: (A As B) = refl
 
   /**
-    * It can be convenient to convert a [[<:<]] value into a `<~<` value.
+    * It can be convenient to convert a <:< value into a `<~<` value.
     * This is not strictly valid as while it is almost certainly true that
     * `A <:< B` implies `A <~< B` it is not the case that you can create
     * evidence of `A <~< B` except via a coercion. Use responsibly.

From 3954ec73c2cf7e7e641f63dbcfb3cffc08a35d0b Mon Sep 17 00:00:00 2001
From: "Mike (stew) O'Connor" <stew@vireo.org>
Date: Fri, 19 May 2017 08:28:36 -0700
Subject: [PATCH 10/12] fix test failure on 2.10.6 + scalajs

Thank you very much @kailuowang for the solutiongit diff
---
 tests/src/test/scala/cats/tests/AsTests.scala | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index e0a702d6ba..df1e0c7e2a 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -4,8 +4,12 @@ package tests
 class AsTests extends CatsSuite {
   import evidence._
 
-  def toMap[A, B, X](fa: List[X])(implicit ev: X <~< (A,B)): Map[A,B] =
-    fa.foldLeft(Map.empty[A,B])(As.contra2_3(ev)(_ + _))
+  def toMap[A, B, X](fa: List[X])(implicit ev: X <~< (A,B)): Map[A,B] = {
+    type RequiredFunc = (Map[A, B], X) => Map[A, B]
+    type GivenFunc = (Map[A, B], (A, B)) => Map[A, B]
+    val subst: GivenFunc <~< RequiredFunc = As.contra2_3(ev) //introduced because inference failed on scalajs on 2.10.6
+    fa.foldLeft(Map.empty[A,B])(subst(_ + _))
+  }
 
   test("narrow an input of a function2") {
     // scala's GenTraversableOnce#toMap has a similar <:< constraint

From 384e887a6de9be84ab26f1127c7adbd955139cf3 Mon Sep 17 00:00:00 2001
From: Kailuo Wang <kailuo.wang@gmail.com>
Date: Mon, 12 Jun 2017 15:55:59 -0400
Subject: [PATCH 11/12] added helper methods for converting Function1

---
 core/src/main/scala/cats/evidence/As.scala    | 14 ++++++++++++--
 tests/src/test/scala/cats/tests/AsTests.scala | 13 ++++++++++---
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/core/src/main/scala/cats/evidence/As.scala b/core/src/main/scala/cats/evidence/As.scala
index cebcd08135..3d1429c97d 100644
--- a/core/src/main/scala/cats/evidence/As.scala
+++ b/core/src/main/scala/cats/evidence/As.scala
@@ -151,14 +151,12 @@ object As extends AsInstances {
   // parameter. Here we provide the proof for what we expect to be the
   // most common shapes.
 
-  // binary
   def contra1_2[T[-_, _], Z, A, B](a: A As Z): (T[Z, B] As T[A, B]) =
     a.substitute[λ[`-α` => T[Z, B] As T[α, B]]](refl)
 
   def contra2_2[T[_, -_], Z, A, B](a: B As Z): (T[A, Z] As T[A, B]) =
     a.substitute[λ[`-α` => T[A, Z] As T[A, α]]](refl)
 
-  // ternary
   def contra1_3[T[-_, _, _], Z, A, B, C](a: A As Z): (T[Z, B, C] As T[A, B, C]) =
     a.substitute[λ[`-α` => T[Z, B, C] As T[α, B, C]]](refl)
 
@@ -167,4 +165,16 @@ object As extends AsInstances {
 
   def contra3_3[T[_, _, -_], Z, A, B, C](a: C As Z): (T[A, B, Z] As T[A, B, C]) =
     a.substitute[λ[`-α` => T[A, B, Z] As T[A, B, α]]](refl)
+
+  /**
+   * Use this relationship to narrow the input type of a Function1
+   */
+  def conF[A, B, C](ev: B As A)(fa: A => C): B => C =
+    contra1_2[Function1, A, B, C](ev).coerce(fa)
+
+  /**
+   * Use this relationship to widen the output type and narrow the input type of a Function1
+   */
+  def invF[C, D, A, B](ev1: D As C, ev2: A As B)(fa: C => A): D => B =
+    conF(ev1)(onF(ev2)(fa))
 }
diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index df1e0c7e2a..4e26816e98 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -51,7 +51,6 @@ class AsTests extends CatsSuite {
     val two: Bottom As Top = bAsA compose cAsB 
   }
 
-
   test("we can use As to coerce a value") {
     val cAsA: Bottom As Top = implicitly
 
@@ -89,13 +88,21 @@ class AsTests extends CatsSuite {
     val contra3_3: EatF33[Unit, Unit, Top] As EatF33[Unit, Unit, Bottom] = As.contra3_3(cAsA)
   }
 
-  test("we can widen a function1") {
+  test("we can widen the output of a function1") {
     val f: Any => Bottom = _ => Bottom()
     val cAsA: Bottom As Top = implicitly
     val f2: Any => Top = As.onF(cAsA)(f)
   }
 
-  test("we can simultaneously narrow the input and widen the ouptut of a Function1") {
+  test("we can narrow the input of a function1") {
+    val f: Top => Any = (t: Top) => t
+    val cAsA: Bottom As Top = implicitly
+    val f2: Bottom => Any = As.conF(cAsA)(f)
+  }
 
+  test("we can simultaneously narrow the input and widen the ouptut of a Function1") {
+    val f: Top => Bottom = _ => Bottom()
+    val cAsA: Bottom As Top = implicitly
+    val f2: Bottom => Top = As.invF(cAsA, cAsA)(f)
   }
 }

From 48f539f9398c117de703d68c76d2a992f1e79e35 Mon Sep 17 00:00:00 2001
From: Kailuo Wang <kailuo.wang@gmail.com>
Date: Tue, 13 Jun 2017 10:15:12 -0400
Subject: [PATCH 12/12] added category law tests

---
 tests/src/test/scala/cats/tests/AsTests.scala | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/src/test/scala/cats/tests/AsTests.scala b/tests/src/test/scala/cats/tests/AsTests.scala
index 4e26816e98..acb24d2acf 100644
--- a/tests/src/test/scala/cats/tests/AsTests.scala
+++ b/tests/src/test/scala/cats/tests/AsTests.scala
@@ -1,6 +1,9 @@
 package cats
 package tests
 
+import cats.laws.discipline.{CategoryTests, SerializableTests}
+import org.scalacheck.{Arbitrary, Gen}
+import cats.arrow.Category
 class AsTests extends CatsSuite {
   import evidence._
 
@@ -11,6 +14,11 @@ class AsTests extends CatsSuite {
     fa.foldLeft(Map.empty[A,B])(subst(_ + _))
   }
 
+  implicit def arbAs[A, B](implicit ev: A <~< B) = Arbitrary(Gen.const(ev))
+  implicit def eq[A, B]: Eq[As[A, B]] = Eq.fromUniversalEquals
+
+
+
   test("narrow an input of a function2") {
     // scala's GenTraversableOnce#toMap has a similar <:< constraint
 
@@ -42,6 +50,9 @@ class AsTests extends CatsSuite {
   trait Middle extends Top
   case class Bottom() extends Middle
 
+  checkAll("As[Bottom, Middle]", CategoryTests[As].category[Bottom, Middle, Top, Any])
+  checkAll("Category[As]", SerializableTests.serializable(Category[As]))
+
   test("subtyping relationships compose") {
 
     val cAsB: Bottom As Middle = As.reify[Bottom,Middle]