ContAndApart.scala

type Void <: Nothing
def absurd[A](v: Void): A = v


type Id[x] = x

trait Forall[F[_]] {
  def apply[A]: F[A]
}

final case class Cont[R, +A](run: (A => R) => R) {
  def map[B](f: A => B): Cont[R, B] =
    Cont[R, B](nb => run(a => nb(f(a))))
    
  def flatMap[B](f: A => Cont[R, B]): Cont[R, B] =
    Cont[R, B](nb => run(a => f(a).run(b => nb(b))))
}
object Cont {
  def pure[R, A](a: A): Cont[R, A] = 
    Cont[R, A](f => f(a))
  
  def either[R, A]: Cont[R, Either[A => R, A]] = 
    Cont(f => f(Left(a => f(Right(a)))))
    
  def and[R, A, B](f: (A, B) => R): Cont[R, Either[A => R, B => R]] = 
    Cont(p => p(Right(b => p(Left(a => f(a, b))))))
}


type =!=[A, B] = Apart[A, B]
type ===[A, B] = Is[A, B]

trait Is[A, B] { ab =>
  def apply[F[_]](fa: F[A]): F[B]
  
  def andThen[C](bc: B === C): A === C = {
    type f[a] = A === a
    bc.apply[f](ab)
  }
  
  def flip: B === A = {
    type f[a] = a === A
    ab.apply[f](Is.refl[A])
  }
  
  def not[R](nab: A =!= B): R =
    nab.apply[Id](ab)[Unit, R][Id](())
    
  def lift[F[_]]: F[A] === F[B] = {
    type f[a] = F[A] === F[a]
    ab.apply[f](Is.refl[F[A]])
  }
}
object Is {
  def refl[A]: A === A = new (A === A) {
    def apply[F[_]](fa: F[A]): F[A] = fa
  }
  
  def force[A, B]: A === B = Is.refl[A].asInstanceOf[A === B]
}

trait Constant[F[_]] {
  def apply[A, B]: F[A] === F[B]
}

trait Apart[A, B] { nab =>
  def apply[F[_]](f: F[A] === F[B]): Constant[F]
  
  def flip: B =!= A = Apart.symm[A, B](this)
  
  def not[R](ab: A === B): R =
    nab.apply[Id](ab)[Unit, R][Id](())
}

object Apart {
  // Irreflexivity.
  def irreflexive[A](aa: A =!= A): Void = 
    aa.not(Is.refl[A])

  // Symmetry.
  def symm[A, B](ab: A =!= B): B =!= A = new (B =!= A) {
    def apply[F[_]](f: F[B] === F[A]): Constant[F] = ab.apply[F](f.flip)
  }
  
  def tight[A, B](f: (A === B) => Void): A =!= B = new (A =!= B) {
    def apply[F[_]](f: F[A] === F[B]): Constant[F] = new Constant[F] {
      def apply[X, Y]: F[X] === F[Y] = Is.force[F[X], F[Y]]
    }
  }
  
  // Co-transitivity.
  def comp[A, B, C](ab: A =!= B): Cont[Void, Either[A =!= C, B =!= C]] = { 
    val f: (A === C, B === C) => Void = (ac, bc) => ab.not(ac andThen bc.flip)
    Cont.and(f).map {
      case Left(nac) => Left(tight(nac))
      case Right(nbc) => Right(tight(nbc))
    }
  }
}