namespace latin:/algebraic❚

/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
❚

fixmeta ur:/?LF ❚

theory Magma =
  include ☞latin:/?EqualityType❙
  op : carrier ⟶ carrier ⟶ carrier ❘# 1 ∘ 2 prec 50❙
❚

theory Semigroup =
  include ?Magma❙
  assoc: {x,y,z} (x∘y)∘z = x∘(y∘z)❙
  
  assocR: {x,y,z} x∘(y∘z) = (x∘y)∘z❘
        = [x,y,z] sym assoc❙

  assoc4:  {w,x,y,z} ((w∘x)∘y)∘z = w∘(x∘(y∘z))❘
        =  [w,x,y,z] trans3 (assoc congT [u]u∘z) assoc (assoc congT [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] trans4 (assoc4 congT [u]u∘z) assoc
                              (assoc congT [u]v∘u) (assoc congT [u]v∘(w∘u))❙
❚

theory Commutative =
  include ?Magma❙
  comm: {x,y} x∘y = y∘x❙
❚

theory Neutral =
  include ?Magma❙
  e  : carrier ❙  
  neutLeft: {x} e∘x = x❙
  neutRight: {x} x∘e = x❙
❚

theory Idempotent =
  include ?Magma❙
  idempotent: {x} x∘x = x❙
❚

theory Monoid =
  include ?Semigroup❙
  include ?Neutral❙
❚

theory CommSemigroup =
  include ?Semigroup❙
  include ?Commutative❙
❚

theory Band =
  include ?Semigroup❙
  include ?Idempotent❙
❚

theory CommMonoid =
  include ?Monoid❙
  include ?CommSemigroup❙
❚

theory Semilattice =
  include ?Band❙
  include ?CommSemigroup❙
❚

theory BoundedSemilattice =
  include ?Semilattice❙
  include ?CommMonoid❙
❚

theory Regular =
	include ?Band❙
  regular: {x,y,z} z∘x∘z∘y∘z = z∘x∘y∘z ❙
❚

theory LeftNormal =
	include ?Band❙
  leftregular1: {x,y,z} z∘x∘z∘y = z∘x∘y ❙
❚

theory LeftRegular =
	include ?Band❙
  leftregular: {x,z} z∘x∘z = z∘x ❙
❚

theory RightNormal =
	include ?Band❙
  rightregular1: {x,y,z} x∘z∘y∘z = x∘y∘z ❙
❚

theory RightRegular =
	include ?Band❙
  rightregular: {y,z} z∘y∘z = y∘z ❙
❚

/T views for the three stages of regular band theories ❚

implicit view Regular2LeftNormal : ?Regular -> ?LeftNormal =
  include ?Band❙
	regular = [x,y,z] leftregular1 congT [u]u∘z❙
❚

implicit view LeftNormal2LeftRegular : ?LeftNormal -> ?LeftRegular =
  include ?Band❙
	leftregular1 = [x,y,z] leftregular congT [u]u∘y❙
❚

implicit view Regular2RightNormal : ?Regular -> ?RightNormal =
  include ?Band❙
	regular = [x,y,z] trans3 assoc5 ((trans3 assoc4R rightregular1 assoc) congT [u]z∘u) assoc4R❙
❚

implicit view RightNormal2RightRegular : ?RightNormal -> ?RightRegular =
  include ?Band❙
	rightregular1 = [x,y,z] trans3 assoc4 ((trans assocR rightregular) congT [u] x∘u) assocR❙
❚

/T normal bands ❚

theory Normal =
	include ?Band❙
  normal: {x,y,z} z∘(x∘y)∘z = z∘(y∘x)∘z ❙
❚

theory RightCommutative =
	include ?Band❙
  leftnormal: {x,y,z} z∘(x∘y) = z∘(y∘x) ❙
❚

theory LeftCommutative =
	include ?Band❙
  rightnormal: {x,y,z} (x∘y)∘z = (y∘x)∘z ❙
❚

/T views for the diamond of normal band theories (with semilattices at the bottom) ❚

implicit view Normal2RightCommutative : ?Normal -> ?RightCommutative =
  include ?Band❙
	normal = [x,y,z] leftnormal congT [u]u∘z❙
❚

implicit view Normal2LeftCommutative : ?Normal -> ?LeftCommutative =
  include ?Band❙
	normal = [x,y,z] trans3 assoc (rightnormal congT [u]z∘u) assocR❙
❚

view RightCommutative2Semilattice : ?RightCommutative -> ?Semilattice =
  include ?Band❙
	leftnormal = [x,y,z] comm congT [u]z∘u❙
❚

implicit view LeftCommutative2Semilattice : ?LeftCommutative -> ?Semilattice =
  include ?Band❙
	rightnormal = [x,y,z] comm congT [u]u∘z❙
❚

/T views from regular to normal band theories ❚

implicit view LeftNormal2Normal : ?LeftNormal -> ?Normal =
  include ?Band❙
  // zxzy = zxzyzxzy = zx yz zxzy = zxy zx zy = zxy xz zy = zxy zxy = zxy❙
  leftregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent❙
❚

implicit view LeftRegular2RightCommutative : ?LeftRegular -> ?RightCommutative =
  include ?Band❙
	leftregular = [x,z] trans4 assoc leftnormal assocR (idempotent congT [u]u∘x)❙
❚

implicit view RightNormal2Normal : ?RightNormal -> ?Normal =
  include ?Band❙
  // xzyz = xzyz xzyz = x yz zxzyz = xy zxzyz = xyz zx yz = xyz xyz = xyz❙
	rightregular1 = [x,y,z] trans3 (sym idempotent) _ idempotent❙
❚

implicit view RightRegular2LeftCommutative : ?RightRegular -> ?LeftCommutative =
  include ?Band❙
	rightregular = [y,z] trans3 rightnormal assoc (idempotent congT [u]y∘u)❙
❚

/T rectangular bands (the axioms here already imply idempotency)❚

theory Rectangular =
	include ?Band❙
  rectangular: {x,y} x∘y∘x = x ❙
  
  // provable ❙
  rectangularAny: {x,y,z} x∘y∘z = x∘z❙
❚

theory LeftZero =
	include ?Band❙
  leftsingular: {x,y} x∘y = x ❙
❚

theory RightZero =
	include ?Band❙
  rightsingular: {x,y} x∘y = y ❙
❚