no message

source/bands.mmt

 namespace http://cds.omdoc.org/examples❚
 
-/T regular bands❚
+/T regular bands and views between them
+mostly following the wikipedia page on Bands
+
+Notes: 
+- some names that were not given on Wikipedia are made up
+- most views do not actually use (all of) the Band properties
+- LeftX and RightX are stronger than X, not weaker
+❚
 
 theory Regular : ?FOLEQNatDed =
 	include ?Band ❙
@@ -31,22 +38,22 @@ theory RightRegular : ?FOLEQNatDed =
 
 implicit view Regular2LeftRegular1 : ?Regular -> ?LeftRegular1 =
   include ?Band = ?Band❙
-	regular = [x,y,z] congT ([u] u∘z) leftregular1❙
+	regular = [x,y,z] congT leftregular1 [u]u∘z❙
 ❚
 
 implicit view LeftRegular12LeftRegular : ?LeftRegular1 -> ?LeftRegular =
   include ?Band = ?Band❙
-	leftregular1 = [x,y,z] congT ([u] u∘y) leftregular❙
+	leftregular1 = [x,y,z] congT leftregular [u]u∘y❙
 ❚
 
 implicit view Regular2RightRegular1 : ?Regular -> ?RightRegular1 =
   include ?Band = ?Band❙
-	regular = [x,y,z] trans3 assoc5 (congT ([u] z∘u) trans3 assoc4R rightregular1 assoc) assoc4R❙
+	regular = [x,y,z] trans3 assoc5 (congT (trans3 assoc4R rightregular1 assoc) [u]z∘u) assoc4R❙
 ❚
 
 implicit view RightRegular12RightRegular : ?RightRegular1 -> ?RightRegular =
   include ?Band = ?Band❙
-	rightregular1 = [x,y,z] trans3 assoc4 (congT ([u] x∘u) trans assocR rightregular) assocR❙
+	rightregular1 = [x,y,z] trans3 assoc4 (congT (trans assocR rightregular) [u] x∘u) assocR❙
 ❚
 
 /T normal bands ❚
@@ -54,6 +61,9 @@ implicit view RightRegular12RightRegular : ?RightRegular1 -> ?RightRegular =
 theory Normal : ?FOLEQNatDed =
 	include ?Band ❙
   normal: {x,y,z} ⊦ z∘(x∘y)∘z ≐ z∘(y∘x)∘z ❙
+  
+  lr: {x,y,z} ⊦ z∘x∘z∘y ≐ z∘(z∘x)∘y  ❘= [x,y,z] trans (congT assoc [u]u∘y) normal❙
+
 ❚
 
 theory LeftNormal : ?FOLEQNatDed =
@@ -70,34 +80,35 @@ theory RightNormal : ?FOLEQNatDed =
 
 implicit view Normal2LeftNormal : ?Normal -> ?LeftNormal =
   include ?Band = ?Band❙
-	normal = [x,y,z] congT ([u] u∘z) leftnormal❙
+	normal = [x,y,z] congT leftnormal [u]u∘z❙
 ❚
 
 implicit view Normal2RightNormal : ?Normal -> ?RightNormal =
   include ?Band = ?Band❙
-	normal = [x,y,z] trans3 assoc (congT ([u] z∘u) rightnormal) assocR❙
+	normal = [x,y,z] trans3 assoc (congT rightnormal [u]z∘u) assocR❙
 ❚
 
 implicit view LeftNormal2Semilattice : ?LeftNormal -> ?Semilattice =
   include ?Band = ?Band❙
-	leftnormal = [x,y,z] congT ([u] z∘u) comm❙
+	leftnormal = [x,y,z] congT comm [u]z∘u❙
 ❚
 
 implicit view RightNormal2Semilattice : ?RightNormal -> ?Semilattice =
   include ?Band = ?Band❙
-	rightnormal = [x,y,z] congT ([u] u∘z) comm❙
+	rightnormal = [x,y,z] congT comm [u]u∘z❙
 ❚
 
 /T views from regular to normal band theories ❚
 
 implicit view LeftRegular12Normal : ?LeftRegular1 -> ?Normal =
   include ?Band = ?Band❙
+  // zxzy = zxzyzxzy = zx yz zxzy = zxy zx zy = zxy xz zy = zxy zxy = zxy❙
   leftregular1 = [x,y,z] _❙
 ❚
 
 implicit view LeftRegular2LeftNormal : ?LeftRegular -> ?LeftNormal =
   include ?Band = ?Band❙
-	leftregular = [x,y,z] _❙
+	leftregular = [x,z] trans4 assoc leftnormal assocR (congT idempotent [u]u∘x)❙
 ❚
 
 implicit view RightRegular12Normal : ?RightRegular1 -> ?Normal =
@@ -107,5 +118,25 @@ implicit view RightRegular12Normal : ?RightRegular1 -> ?Normal =
 
 implicit view RightRegular2RightNormal : ?RightRegular -> ?RightNormal =
   include ?Band = ?Band❙
-	rightregular = [x,y,z] _❙
+	rightregular = [y,z] trans3 rightnormal assoc (congT idempotent [u]y∘u)❙
+❚
+
+/T rectangular bands (the axioms here already imply idempotency)❚
+
+theory Rectangular : ?FOLEQNatDed =
+	include ?Band ❙
+  rectangular: {x,y} ⊦ x∘y∘x ≐ x ❙
+  
+  // provable ❙
+  rectangularAny: {x,y,z} ⊦ x∘y∘z ≐ x∘z❙
+❚
+
+theory LeftSingular : ?FOLEQNatDed =
+	include ?Band ❙
+  leftsingular: {x,y} ⊦ x∘y ≐ x ❙
+❚
+
+theory RightSingular : ?FOLEQNatDed =
+	include ?Band ❙
+  rightsingular: {x,y} ⊦ x∘y ≐ y ❙
 ❚

source/logic/fol.mmt

@@ -28,8 +28,8 @@ theory FOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
   include ?FOLEQ❙
   include ?FOLNatDed  ❙
   refl     : {x} ⊦ x ≐ x❙
-  congT    : {x,y}{T: term ⟶ term} ⊦ x ≐ y ⟶ ⊦ (T x) ≐ (T y) ❘# congT 3 4❙
-  congF    : {x,y}{F: term ⟶ prop} ⊦ x ≐ y ⟶ ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5❙
+  congT    : {x,y} ⊦ x ≐ y ⟶ {T: term ⟶ term} ⊦ (T x) ≐ (T y) ❘# congT 3 4❙
+  congF    : {x,y} ⊦ x ≐ y ⟶ {F: term ⟶ prop} ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5❙
   sym      : {x,y} ⊦ x ≐ y ⟶ ⊦ y ≐ x❙
   trans    : {x,y,z} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z❙
   

source/magmas.mmt

@@ -12,11 +12,11 @@ theory Semigroup : ?FOLEQNatDed =
         = [x,y,z] sym assoc❙
 
   assoc4:  {w,x,y,z} ⊦ ((w∘x)∘y)∘z ≐ w∘(x∘(y∘z))❘
-        =  [w,x,y,z] trans3 (congT ([u]u∘z) assoc) assoc (congT ([u]w∘u) assoc)❙
+        =  [w,x,y,z] trans3 (congT assoc [u]u∘z) assoc (congT assoc [u]w∘u)❙
   assoc4R: {w,x,y,z} ⊦ w∘(x∘(y∘z)) ≐ ((w∘x)∘y)∘z❘
         = [w,x,y,z] sym assoc4❙
   assoc5: {v,w,x,y,z} ⊦ (((v∘w)∘x)∘y)∘z ≐ v∘(w∘(x∘(y∘z)))❘
-        = [v,w,x,y,z] trans3 (congT ([u]u∘z) assoc4) assoc (congT ([u]v∘u) assoc4)❙
+        = [v,w,x,y,z] trans3 (congT assoc4 [u]u∘z) assoc (congT assoc4 [u]v∘u)❙
 ❚
 
 theory Commutative : ?FOLEQNatDed =