sample of abuse of Java/Scala type system for simulate given formal system

CAT.scala

package cat

object CAT {

  // system traits
  sealed trait Type[Self <: Type[Self]]
  sealed trait Of[Self <: Of[Self, T], T <: Type[T]]

  // types
  case class Ob()
    extends Type[Ob]
  case class Hom
    [ A <: Of[A, Ob], B <: Of[B, Ob] ]
    ( a: A, b: B )
    extends Type[Hom[A, B]]
  case class Equ
    [ A <: Of[A, Ob], B <: Of[B, Ob],
      F <: Of[F, Hom[A, B]], G <: Of[G, Hom[A, B]] ]
    ( f: F, g: G )
    extends Type[Equ[A, B, F, G]]

  // category structure
  case class Refl
    [ A <: Of[A, Ob], B <: Of[B, Ob],
      F0 <: Of[F0, Hom[A, B]] ]
    ( f0: F0 )
    extends Of[Refl[A, B, F0], Equ[A, B, F0, F0]]
  case class Trans
    [ A <: Of[A, Ob], B <: Of[B, Ob],
      F1 <: Of[F1, Hom[A, B]], F2 <: Of[F2, Hom[A, B]], F3 <: Of[F3, Hom[A, B]],
      E12 <: Of[E12, Equ[A, B, F1, F2]], E23 <: Of[E23, Equ[A, B, F2, F3]] ]
    ( e12: E12, e23: E23 )
    extends Of[Trans[A, B, F1, F2, F3, E12, E23], Equ[A, B, F1, F3]]
  case class Sym
    [ A <: Of[A, Ob], B <: Of[B, Ob],
      F1 <: Of[F1, Hom[A, B]], F2 <: Of[F2, Hom[A, B]],
      E12 <: Of[E12, Equ[A, B, F1, F2]] ]
    ( e12: E12 )
    extends Of[Sym[A, B, F1, F2, E12], Equ[A, B, F2, F1]]
  case class Id
    [ A <: Of[A, Ob] ]
    ()
    extends Of[Id[A], Hom[A, A]]
  case class Mul
    [ A <: Of[A, Ob], B <: Of[B, Ob], C <: Of[C, Ob],
      F <: Of[F, Hom[A, B]], G <: Of[G, Hom[B, C]] ]
    ( f: F, g: G )
    extends Of[Mul[A, B, C, F, G], Hom[A, C]]
  case class MulEqu
    [ A <: Of[A, Ob], B <: Of[B, Ob], C <: Of[C, Ob],
      F1 <: Of[F1, Hom[A, B]], F2 <: Of[F2, Hom[A, B]],
      G1 <: Of[G1, Hom[B, C]], G2 <: Of[G2, Hom[B, C]],
      F12 <: Of[F12, Equ[A, B, F1, F2]],
      G12 <: Of[G12, Equ[B, C, G1, G2]] ]
    ( f12: F12, g12: G12 )
    extends Of[
        MulEqu[A, B, C, F1, F2, G1, G2, F12, G12],
        Equ[A, C, Mul[A, B, C, F1, G1], Mul[A, B, C, F2, G2]] ]

}