refactor laws !!!

cleanup structure

fix unicode chars in SM

src/main/scala/svarog/EquationalLaws.scala

@@ -0,0 +1,67 @@
+package svarog
+
+object EquationalLaws {
+
+  // I * a == a and a == a * I
+  def unitality[X](a: X, binOp: (X,X) => X, unit: X): Boolean =
+    (binOp(unit, a) == a) && (a == binOp(a, unit))
+
+  // (a * b) * c == a * (b * c)
+  def associativity[X](a: X, b: X, c: X, binOp: (X,X) => X): Boolean =
+    binOp(binOp(a,b), c) == binOp(a, binOp(b,c))
+
+  // a - a == 0
+  def reflexivity[X](a: X, rel: (X,X) => Boolean): Boolean =
+    rel(a,a)
+
+  // a < b and b < c then a < c
+  def transitivity[X](a: X, b: X, c: X, rel: (X,X) => Boolean): Boolean =
+    if(rel(a,b) && rel(b,c)) rel(a,c)
+    else true
+
+  // a * b == b * a
+  def symmetry[X,Y](a: X, b: X, binOp: (X,X) => Y): Boolean =
+    binOp(a,b) == binOp(b,a)
+
+  def monotonicity[X](a1: X, a2: X, b1: X, b2: X, binOp: (X,X) => X, rel: (X,X) => Boolean): Boolean =
+    if( rel(a1, b1) && rel(a2, b2) ) rel( binOp(a1, a2), binOp(b1, b2) )
+    else true
+
+  // if a ~ b then a == b
+  def skeletality[X](a: X, b: X, rel: (X,X) => Boolean): Boolean =
+    if( rel(a,b) ) a == b
+    else true
+
+  // if (a + b) <= c then a <= b - c
+  // - could be monus(a,b) = max(0,b-a)
+  // TODO what is the mathematical name of this property
+  def minusPlusPreorder[X](a: X, b: X, c: X, plus: (X,X) => X, monus: (X, X) => X, lessOrEqual: (X,X) => Boolean): Boolean = {
+    if( lessOrEqual(plus(a,b), c) ) lessOrEqual(a, monus(b,c) )
+    else if( lessOrEqual(a, monus(b,c) ) ) lessOrEqual( plus(a,b), c)
+    else true
+  }
+
+  // TODO this is probabl wrong - generalized badly - redo it
+  def triangleInequality[X,Y](x: X, y: X, z: X, distance: (X,X) => Y, lessOrEqual: (Y,Y) => Boolean, plus: (Y,Y) => Y): Boolean =
+    lessOrEqual(
+      distance(x,z),
+      plus(distance(x,y), distance(y,z))
+    )
+
+  // back(there(start)) == start
+  def isAdjoint[A,B](start: A, there: A => B, back: B => A)(rel: (A,A) => Boolean): Boolean = {
+    val dest = there(start)
+    val bc2 = back(dest)
+    rel(start,bc2)
+  }
+
+  // f(x) binOp f(y) == f(x binOp y)
+  def preserveOp[X,Y](x: X, y: X, f: X => X, binOp: (X,X) => X): Boolean = {
+    val eq: (X,X) => Boolean = _ == _
+    preserveOp[X,X](x, y, f, binOp, binOp, eq)
+  }
+
+  // f(p1) binOpY f(p2) <= f(p1 binOpX p2)
+  def preserveOp[X,Y](x: X, y: X, f: X => Y, binOpX: (X,X) => X, binOpY: (Y,Y) => Y, rel: (Y,Y) => Boolean): Boolean =
+    rel( binOpY( f(x), f(y) ), f(binOpX(x,y)) )
+}

src/main/scala/svarog/Equivalence.scala

@@ -9,23 +9,20 @@ import simulacrum.{op, typeclass}
  * - (transitivity) forall a,b,c∈A if a ~ b and b ~ c then a ~ c
  */
 @typeclass
-trait Equivalence[A] {
+trait Equivalence[A] { // consider just using scala.Equiv without simulacrum magic
+
   @op("~")
   def equivalent(a: A, b: A): Boolean
 }
 
 trait EquivalenceLaws {
-  import Equivalence.ops._
 
   def reflexivity[A](a: A)(implicit E: Equivalence[A]): Boolean =
-    a ~ a
+    EquationalLaws.reflexivity(a, E.equivalent)
 
   def symmetry[A](a: A, b: A)(implicit E: Equivalence[A]): Boolean =
-    if(a ~ b) b ~ a
-    else if(b ~ a) a ~ b
-    else true
+    EquationalLaws.symmetry(a,b,E.equivalent)
 
   def transitivity[A](a: A, b: A, c: A)(implicit E: Equivalence[A]): Boolean =
-    if ((a ~ b) && (b ~ c)) b ~ c
-    else true
+    EquationalLaws.transitivity(a,b,c,E.equivalent)
 }

src/main/scala/svarog/algebra/Semigroup.scala

@@ -1,17 +1,16 @@
 package svarog.algebra
 
 import simulacrum.typeclass
+import svarog.EquationalLaws
 
 @typeclass
 trait Semigroup[X] extends Magma[X]
 
 trait SemigroupLaws {
 
   /** forall a,b,c ∈ X, (a ⊗ b) ⊗ c􏰆 = a ⊗ (b ⊗ c) */
-  def associativity[X](a: X, b: X, c: X)(implicit P: Monoid[X]): Boolean = {
-    import Monoid.ops._
-    ((a * b) * c) == (a * (b * c))
-  }
+  def associativity[X](a: X, b: X, c: X)(implicit P: Semigroup[X]): Boolean =
+    EquationalLaws.associativity(a,b,c, P.multiply)
 }
 
 object SemigroupLaws extends SemigroupLaws {}

src/main/scala/svarog/algebra/SymmetricMonoid.scala

@@ -1,21 +1,20 @@
 package svarog.algebra
 
 import simulacrum.typeclass
+import svarog.EquationalLaws
 
 @typeclass
 trait SymmetricMonoid[X]
   extends Monoid[X]
 
 /**
  * Laws for SymmetricMonoidalPreorder:
- * - symmetry: forall a,b ∈ X, a ⊗ b􏰆 = b ⊗ a
+ * - symmetry: forall a,b ∈ X, a ⊗ b = b ⊗ a
  */
 trait SymmetricMonoidLaws
   extends MonoidLaws {
 
-  /** forall a,b ∈ X, a ⊗ b􏰆 = b ⊗ a */
-  def symmetry[X](a: X, b: X)(implicit P: SymmetricMonoid[X]): Boolean = {
-    import P._
-    multiply(a,b) == multiply(b,a)
-  }
+  /** forall a,b ∈ X, a ⊗ b = b ⊗ a */
+  def symmetry[X](a: X, b: X)(implicit P: SymmetricMonoid[X]): Boolean =
+    EquationalLaws.symmetry(a,b,P.multiply)
 }

src/main/scala/svarog/algebra/UnitalMagma.scala

@@ -1,6 +1,7 @@
 package svarog.algebra
 
 import simulacrum.typeclass
+import svarog.EquationalLaws
 
 @typeclass
 trait UnitalMagma[X]
@@ -12,11 +13,8 @@ trait UnitalMagma[X]
 trait UnitalMagmaLaws {
 
   /** forall a ∈ X, I ⊗ a􏰆 = a and a ⊗ I = 􏰆a */
-  def unitality[X](a: X)(implicit P: UnitalMagma[X]): Boolean = {
-    import UnitalMagma.ops._
-    import P.I
-    ((I * a) == a) && (a == (a * I))
-  }
+  def unitality[X](a: X)(implicit P: UnitalMagma[X]): Boolean =
+    EquationalLaws.unitality(a, P.multiply, P.I)
 }
 
 object UnitalMagmaLaws extends UnitalMagmaLaws {}

src/main/scala/svarog/enrichment/BoolCategory.scala

@@ -1,35 +1,36 @@
 package svarog.enrichment
 
-import svarog.enrichment.BoolCategory.BoolCategory
+import svarog.EquationalLaws
+import svarog.enrichment.BoolCategory.BoolCat
 import svarog.preorders.{Preorder, SymmetricMonoidalPreorder}
-import svarog.preorders.SymmetricMonoidalPreorder.SMPBoolAndLe
+import svarog.preorders.SymmetricMonoidalPreorder.`(B, ≤, true, ∧)`
 
 // There is a one-to-one correspondence between preorders and Bool-categories
 object BoolCategory {
 
-  type BoolCategory[X] = EnrichedCategory[Boolean, X]
+  type BoolCat[X] = EnrichedCategory[Boolean, X]
 
-  def apply[X](pre: Preorder[X]): BoolCategory[X] = new BoolCategory[X] {
-    override def base: SymmetricMonoidalPreorder[Boolean] = SMPBoolAndLe
+  def apply[X](pre: Preorder[X]): BoolCat[X] = new BoolCat[X] {
+    override def base: SymmetricMonoidalPreorder[Boolean] = `(B, ≤, true, ∧)`
     override def homObject(x: X, y: X): Boolean = pre.le(x, y)
   }
 
-  implicit def asPreorder[X](implicit bc: BoolCategory[X]): Preorder[X] =
+  implicit def asPreorder[X](bc: BoolCat[X]): Preorder[X] =
     (a: X, b: X) => bc.homObject(a,b)
 }
 
 trait BoolCategoryLaws {
   import BoolCategory.asPreorder
 
-  def property1[X](bc: BoolCategory[X]): Boolean = {
-    val p = asPreorder(bc)
-    val bc2 = BoolCategory(p)
-    bc == bc2 // TODO we need equivalence for BoolCategory[X]
+  def toPreorderAndBackToBoolCategoryIsNoOp[X](bc: BoolCat[X])(a: X, b: X): Boolean = {
+    EquationalLaws.isAdjoint[BoolCat[X],Preorder[X]](bc,asPreorder,BoolCategory.apply) { case (b1, b2) =>
+      b1.homObject(a, b) == b2.homObject(a, b)
+    }
   }
 
-  def property2[X](p: Preorder[X]): Boolean = {
-    val bc = BoolCategory(p)
-    val p2 = asPreorder(bc)
-    p2 == p // TODO we need equivalence for BoolCategory[X]
+  def toBoolCatAndBackToPreorderIsNoOp[X](p: Preorder[X],a: X, b:X): Boolean = {
+    EquationalLaws.isAdjoint[Preorder[X],BoolCat[X]](p,BoolCategory.apply,asPreorder) { case (b1, b2) =>
+      b1.le(a, b) == b2.le(a, b)
+    }
   }
 }

src/main/scala/svarog/enrichment/DaggerEnrichedCategory.scala

@@ -1,5 +1,6 @@
 package svarog.enrichment
 
+import svarog.EquationalLaws
 
 trait DaggerEnrichedCategory[V,X]
   extends EnrichedCategory[V,X]
@@ -8,5 +9,5 @@ trait DaggerEnrichedCategoryLaws
   extends EnrichedCategoryLaws {
 
   def symmetry[V,X](ec: EnrichedCategory[V,X],a: X, b: X): Boolean =
-    ec.homObject(a,b) == ec.homObject(b,a)
+    EquationalLaws.symmetry(a,b,ec.homObject)
 }

src/main/scala/svarog/enrichment/EnrichedCategory.scala

@@ -1,27 +1,29 @@
 package svarog.enrichment
 
-import svarog.preorders.{Preorder, MonoidalPreorder}
+import svarog.EquationalLaws
+import svarog.preorders.{MonoidalPreorder, Preorder}
 import svarog.sets.MathSet
 
 trait EnrichedCategory[V, X] { self =>
   def base: MonoidalPreorder[V]
   def objects: MathSet[X] = Function.const(true)
   def homObject(x: X, y: X): V
+
+  def Stanislaw(a: X, b: X): Boolean =
+    base.le(base.I, homObject(a,b))
 }
 
 trait EnrichedCategoryLaws {
   import svarog.preorders.MonoidalPreorder.ops._
 
   /** forall x ∈ Ob(X), I ≤ X(x,x) */
-  def ecLaw1[V,X](x: X)(implicit ec: EnrichedCategory[V,X]): Boolean = {
-    implicit val b = ec.base
-    import ec._
-    if(objects(x)) base.I <= homObject(x,x)
+  def reflexivity[V,X](x: X)(implicit ec: EnrichedCategory[V,X]): Boolean =
+    if(ec.objects(x)) EquationalLaws.reflexivity(x,ec.Stanislaw)
     else true
-  }
 
   /** forall x,y,z ∈ Ob(X), X(x,y) ⊗ X(y,z) ≤ X(x,z) */
-  def ecLaw2[V,X](ec: EnrichedCategory[V,X], x: X, y: X, z: X): Boolean = {
+  def triangleInequality[V,X](ec: EnrichedCategory[V,X], x: X, y: X, z: X): Boolean = {
+    // TODO looks like triangleInequality but the equality is wrong :(
     implicit val b = ec.base
     import ec._
     if( objects(x) && objects(y) && objects(z) ) {

src/main/scala/svarog/enrichment/SkeletalEnrichedCategory.scala

@@ -1,13 +1,21 @@
 package svarog.enrichment
 
+import svarog.{EquationalLaws, Equivalence}
+
 trait SkeletalEnrichedCategory[V,X]
   extends EnrichedCategory[V,X]
+  with Equivalence[X] {
+
+  def homRelation(a: X, b: X): Boolean =
+    base.le(base.I, homObject(a,b))
+
+  override def equivalent(a: X, b: X): Boolean =
+    homRelation(a,b) && homRelation(b,a)
+}
 
 trait SkeletalEnrichedCategoryLaws
   extends EnrichedCategoryLaws {
 
-  def skeletality[V,X](a: X, b: X)(implicit P: EnrichedCategory[V,X]): Boolean =
-    if( P.base.le(P.base.I, P.homObject(a,b)) &&
-      P.base.le(P.base.I, P.homObject(b,a)) ) a == b
-    else true
+  def skeletality[V,X](a: X, b: X)(implicit P: SkeletalEnrichedCategory[V,X]): Boolean =
+    EquationalLaws.skeletality(a,b, P.homRelation)
 }

src/main/scala/svarog/metric/ExtendedMetricSpace.scala

@@ -1,7 +1,8 @@
 package svarog.metric
 
 import simulacrum.typeclass
-import svarog.data.PositiveRealsWithInfinity.ZERO
+import svarog.EquationalLaws
+import svarog.sets.PositiveRealsWithInfinity.ZERO
 
 @typeclass
 trait ExtendedMetricSpace[X]
@@ -11,7 +12,7 @@ trait ExtendedMetricSpaceLaws
   extends LawvereMetricSpaceLaws {
 
   def symmetry[X](x: X, y: X)(implicit ms: MetricSpace[X]): Boolean =
-    ms.distance(x,y) == ms.distance(y,x)
+    EquationalLaws.symmetry(x,y,ms.distance)
 
   def msLaw2[X](x: X, y: X)(implicit ms: ExtendedMetricSpace[X]): Boolean = {
     if( ms.distance(x,y) == ZERO ) x == y

src/main/scala/svarog/metric/LawvereMetricSpace.scala

@@ -1,22 +1,26 @@
 package svarog.metric
 
-import simulacrum.typeclass
-import svarog.data.PositiveRealsWithInfinity.{ZERO, `[0,oo]`}
+import simulacrum.{op, typeclass}
+import svarog.EquationalLaws
+import svarog.sets.PositiveRealsWithInfinity.{ZERO, `[0,oo]`}
+import svarog.sets.PositiveRealsWithInfinity.`([0, ∞], ≥, 0, +)`
 
 @typeclass
 trait LawvereMetricSpace[X]{
+  @op("|-|")
   def distance(a: X, b: X): `[0,oo]`
+
+  def noEffort(a: X, b: X): Boolean =
+    distance(a,b) == ZERO
 }
 
 trait LawvereMetricSpaceLaws {
-  import svarog.preorders.SymmetricMonoidalClosedPreorder.ops._
-  import svarog.data.PositiveRealsWithInfinity.SMCP
 
-  def msLaw1[X](x: X)(implicit ms: LawvereMetricSpace[X]): Boolean =
-    ms.distance(x,x) == ZERO
+  def zeroDistanceReflexivity[X](x: X)(implicit ms: LawvereMetricSpace[X]): Boolean =
+    EquationalLaws.reflexivity(x,ms.noEffort)
 
   def trianglInequality[X](x: X, y: X, z: X)(implicit ms: LawvereMetricSpace[X]): Boolean =
-    ms.distance(x,z) <= ms.distance(x,y) * ms.distance(y,z)
+    EquationalLaws.triangleInequality(x,y,z,ms.distance,`([0, ∞], ≥, 0, +)`.le,`([0, ∞], ≥, 0, +)`.multiply) // TODO check if SMCP def alight with this law!
 }
 
 // TODO weight graph into Lawvere metric space

src/main/scala/svarog/metric/MetricSpace.scala

@@ -1,24 +1,33 @@
 package svarog.metric
 
-trait MetricSpace[X] {
+import simulacrum.{op, typeclass}
+import svarog.{EquationalLaws, Equivalence}
+
+@typeclass
+trait MetricSpace[X]
+  extends Equivalence[X] {
+
+  @op("|-|")
   def distance(a: X, b: X): BigDecimal // TODO ensure >= 0
+
+  val zero = BigDecimal(0)
+  override def equivalent(a: X, b: X): Boolean =
+    distance(a,b) == zero
 }
 
 trait MetricSpaceLaws {
-  val zero = BigDecimal(0)
 
   def noDistanceFromPointToItself[X](x: X)(implicit ms: MetricSpace[X]): Boolean =
-   ms.distance(x,x) == zero
+    EquationalLaws.reflexivity(x,ms.equivalent)
 
   def symmetry[X](x: X, y: X)(implicit ms: MetricSpace[X]): Boolean =
-    ms.distance(x,y) == ms.distance(y,x)
+    EquationalLaws.symmetry(x,y, ms.distance)
 
   def equalWhenNoDistance[X](x: X, y: X)(implicit ms: MetricSpace[X]): Boolean =
-    if( ms.distance(x,y) == zero ) x == y
-    else true
+    EquationalLaws.skeletality(x,y,ms.equivalent)
 
-  def trianglInequality[X](x: X, y: X, z: X)(implicit ms: MetricSpace[X]): Boolean =
-    ms.distance(x,y) + ms.distance(y,z) >= ms.distance(x,z)
+  def triangleInequality[X](x: X, y: X, z: X)(implicit ms: MetricSpace[X]): Boolean =
+    EquationalLaws.triangleInequality[X,BigDecimal](x,y,z,ms.distance, _ <= _, _ + _)
 }