trying to make fixed sized vectors using dependent types

Bool.scala

package dep

sealed trait Bool {
  type Cata[T <: U, F <: U, U] <: U
}

sealed trait True extends Bool {
  type Cata[T <: U, F <: U, U] = T
}

sealed trait False extends Bool {
  type Cata[T <: U, F <: U, U] = F
}

object Bool {
  type And[A <: Bool, B <: Bool] = A#Cata[B, False, Bool]
  type Or[A <: Bool, B <: Bool] = A#Cata[True, B, Bool]
  type Not[A <: Bool] = A#Cata[False, True, Bool]
}

Cmp.scala

package dep

sealed trait Cmp {
  type Cata[L <: Up, E <: Up, G <: Up, Up] <: Up

  type lt = Cata[True, False, False, Bool]
  type eq = Cata[False, True, False, Bool]
  type gt = Cata[False, False, True, Bool]
}

sealed trait Lt extends Cmp {
  type Cata[L <: Up, E <: Up, G <: Up, Up] = L
}

sealed trait Eq extends Cmp {
  type Cata[L <: Up, E <: Up, G <: Up, Up] = E
}

sealed trait Gt extends Cmp {
  type Cata[L <: Up, E <: Up, G <: Up, Up] = G
}

dep.scala

package dep

sealed trait Vec[N <: Nat, A]
case class Nil[Zero, A]() extends Vec[Zero, A]
case class Cons[N <: Nat, A](h: A, t: Vec[N, A]) extends Vec[Succ[N], A]

case object Vec {
  import Nat.Add

  def concat[Lx <: Nat, Ly <: Nat, A](
    xs: Vec[Lx, A],
    ys: Vec[Ly, A])
  : Vec[Add[Lx,Ly], A] =
    xs match {
      case _: Nil[Zero, A] => ys
      case Cons(h, t) => Cons(h, concat(t, ys))
    }
}

object Main extends App {
  def toBoolean[B <: Bool](implicit rep: BoolRep[B]): Boolean = rep.value
  case class BoolRep[B <: Bool](value: Boolean)
  implicit val trueRep = BoolRep[True](true)
  implicit val falseRep = BoolRep[False](false)

  type _0 = Zero
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]

  import Nat.Add
  type ===[A <: Nat, B <: Nat] = A#Compare[B]#eq
  val b = toBoolean[ _3 === Add[_2, _1]  ]
  println(b)
}

Fold.scala

package dep

trait Fold[-Element, Value] {
  type Apply[E <: Element, V <: Value] <: Value
}

Nat.scala

package dep

trait Nat {
  type Cata[Z <: U, S[N <: Nat] <: U, U] <: U
  type Compare[N <: Nat] <: Cmp
  type FoldR[I <: U, U, F <: Fold[Nat, U]] <: U
}

trait Zero extends Nat {
  type Cata[Z <: U, S[N <: Nat] <: U, U] = Z
  type Compare[N <: Nat] = N#Cata[Eq, ConstLt, Cmp]
  type ConstLt[A] = Lt
  type FoldR[I <: U, U, F <: Fold[Nat, U]] = I
}

trait Succ[N <: Nat] extends Nat {
  type Cata[Z <: U, S[N <: Nat] <: U, U] = S[N]
  type Compare[O <: Nat] = O#Cata[Gt, N#Compare, Cmp]
  type FoldR[I <: U, U, F <: Fold[Nat, U]] =
    F#Apply[Succ[N], N#FoldR[I, U, F]]
}

object Nat {
  type Add[A <: Nat, B <: Nat] = A#FoldR[B, Nat, Inc]
  type Inc = Fold[Nat, Nat] {
    type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]
  }
}

[error] ./dep.scala:15: type mismatch;
[error]  found   : dep.Vec[Ly,A]
[error]  required: dep.Vec[dep.Nat.Add[Lx,Ly],A]
[error]       case _: Nil[Zero, A] => ys
[error]                               ^
[error] ./dep.scala:16: type mismatch;
[error]  found   : dep.Cons[dep.Nat.Add[dep.Nat,Ly],A]
[error]  required: dep.Vec[dep.Nat.Add[Lx,Ly],A]
[error] Note: dep.Nat.Add[dep.Nat,Ly] >: dep.Nat.Add[Lx,Ly], but trait Vec is invariant in type N.
[error] You may wish to define N as -N instead. (SLS 4.5)
[error]       case Cons(h, t) => Cons(h, concat(t, ys))