namespace latin:/algebraic❚

fixmeta latin:/?SFOLEQND❚

theory Magma = 
  include ?Set ❙
  op : U ⟶ U ⟶ U ❘# 1 ∘ 2 prec 50❙
  
  total structure divisibility : ?Relation =
    include ?Set❙
    rel = [x,z] ∃[y]x∘y≐z❙
  ❚
❚

theory MagmaHom = 
  include ?SetHom ❙
  structure domain : ?Magma =
    include ?SetHom/domain❙
  ❚
  structure codomain : ?Magma = 
    include ?SetHom/codomain❙
  ❚
  op : ⊦ ∀[x]∀[y] U (x domain/∘ y) ≐ U x codomain/∘ U y ❙
❚

theory SubMagma = 
  include ?SubSet❙
  structure parent : ?Magma =
    include ?SubSet/parent❙
  ❚
  op: ⊦ ∀[x]∀[y] U x ⇒ U y ⇒ U (x parent/∘ y)  ❙
❚

theory Commutative = 
  include ?Magma ❙
  comm_ax : ⊦ ∀[x]∀[y] x∘y ≐ y∘x❙
  comm : {x,y} ⊦ x∘y ≐ y∘x❘ = [x,y] comm_ax forallE x forallE y❙
❚

view OppositeMagma : ?Magma → ?Magma = 
  universe = universe ❙
  U = U ❙
  op = [x, y] y ∘ x ❙
❚

theory Idempotent = 
  include ?Magma ❙
  idem_ax: ⊦ ∀[x] x∘x ≐ x ❙
  idem : {x} ⊦ x∘x≐x❘ = [x] idem_ax forallE x❙
❚

view OppositeCommMagma : ?Commutative → ?Commutative =
  include ?OppositeMagma ❙
  op = op ❙
  comm_ax = comm_ax ❙
❚

theory PowerAssociative = 
  include ?Magma ❙
  power_assoc : ⊦ ∀[x] (x∘x)∘x ≐ x∘(x∘x)❙
❚

theory Semigroup = 
  include ?Magma ❙
  assoc_ax : ⊦ ∀[x]∀[y]∀[z] (x∘y)∘z ≐ x∘(y∘z)❙
  
  assoc: {x,y,z} ⊦ (x∘y)∘z ≐ x∘(y∘z)❘
       = [x,y,z] assoc_ax forallE x forallE y forallE z❙
  assocR: {x,y,z} ⊦ x∘(y∘z) ≐ (x∘y)∘z❘
        = [x,y,z] assoc sym❙
  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] assoc4 sym❙
  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))❙
  
  realize ?PowerAssociative❙
  power_assoc = forallI [x] assoc❙
  
//  total structure divisibility : ?Transitivity =
    include ?Magma/divisibility❙
//    metarel/trans = [x,y,z,p,q] p existsE [xy,xyP] q existsE [yz,yzP]
      existsI (xy ∘ yz) trans3 assocR (xyP congT [u]u∘yz) yzP❙
//  ❚
❚

view OppositeSemigroup : ?Semigroup → ?Semigroup = 
  include ?OppositeMagma ❙
  op = op ❙
  assoc_ax = assoc_ax❙
❚

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

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

theory CommIdempotent =
  include ?Idempotent❙
  include ?Commutative❙
❚

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

theory Pointed = 
  include ?Set❙
  elem : U❙
❚

theory UnitElement =
  include ?Magma❙
  structure unitelem : ?Pointed =
    include ?Set❙
    elem # e❙
  ❚
  involution : U ⟶ prop❘ = [x] x∘x≐e❙
❚

theory RightUnital =
  include ?UnitElement❙
  neutralR : ⊦ ∀[x] x∘e ≐ x❙
  neutR: {x} ⊦ x∘e≐x❘= [x] neutralR forallE x❘role Simplify❙
❚

theory LeftUnital = 
  include ?UnitElement❙
  neutralL : ⊦ ∀[x] e∘x ≐ x❙
  neutL: {x} ⊦ e∘x≐x❘= [x] neutralL forallE x❘ role Simplify❙ 
❚

theory Unital = 
  include ?LeftUnital ❙
  include ?RightUnital ❙
❚

theory AbsorbingElement =
  include ?Magma❙
  structure absorbingelem : ?Pointed =
    include ?Set❙
    elem # abs❙
  ❚
❚

theory RightAbsorptive =
  include ?AbsorbingElement❙
  absorbR : ⊦ ∀[x] x∘abs ≐ abs❙
  absR : {x} ⊦ x∘abs ≐ abs❘ = [x] absorbR forallE x❘role Simplify❙
❚

theory LeftAbsorptive =
  include ?AbsorbingElement❙
  absorbL : ⊦ ∀[x] abs∘x ≐ abs❙
  absL : {x} ⊦ abs∘x ≐ abs❘ = [x] absorbL forallE x❘role Simplify❙
❚

theory Absorptive = 
  include ?LeftAbsorptive❙
  include ?RightAbsorptive❙
❚

theory FirstNonNeutral =
  include ?Unital❙
  firstNonNeutral : ⊦ ∀[x] x≠e ⇒ ∀[y]x∘y≐x❙  
  // realize ?Monoid❙
❚

theory LastNonNeutral =
  include ?Unital❙
  lastNonNeutral : ⊦ ∀[x] x≠e ⇒ ∀[y]x∘y≐x❙  
  // realize ?Monoid❙
❚

theory Powers = 
  include ?PowerAssociative❙
  include ?Unital❙
  include ☞latin:/?Nat❙
  power : U ⟶ ℕ ⟶ U❘# 1 ^ 2 prec 60❙
  power_zero: {x} ⊦ x^0 ≐ e❘ role Simplify❙
  power_succ: {x,n} ⊦ x^(n') ≐ x^n∘x❘ role Simplify❙
❚

theory Monoid = 
  include ?Semigroup❙
  include ?Unital❙

  inverse : U ⟶ U ⟶ prop❘ = [x,xˈ] x∘xˈ≐e ∧ xˈ∘x≐e❘# inverse 1 2 prec 30❙

  inverse_sym : {x,xˈ} ⊦ inverse x xˈ ⟶ ⊦ inverse xˈ x❘
              = [x,xˈ,p] andI (p andEr) (p andEl)❙
  inverse_unique : {x,x1,x2} ⊦ inverse x x1 ⟶ ⊦ inverse x x2 ⟶ ⊦ x1≐x2❘
                 = [x,x1,x2,p,q] trans3
                   ((neutR sym) trans (q andEl sym congT [u]x1∘u))
                   assocR
                   ((p andEr congT [u]u∘x2) trans neutL)❙

  inverse_neutral : ⊦ inverse e e❘
                  = andI neutL neutL❙
  inverse_op : {x,y,xˈ,yˈ} ⊦ inverse x xˈ ⟶ ⊦ inverse y yˈ ⟶ ⊦ inverse (x∘y) (yˈ∘xˈ)❘
             = [x,y,xˈ,yˈ,p,q] andI
             (trans3 assoc ((trans3 assocR (q andEl congT [u]u∘xˈ) neutL) congT [u]x∘u) (p andEl))
             (trans3 assoc ((trans3 assocR (p andEr congT [u]u∘y) neutL) congT [u]yˈ∘u) (q andEr))
             ❙

  involution_inverse: {x} ⊦ involution x ⇔ inverse x x❘
             = [x] equivI ([p] andI p p) ([p] p andEl)❙
❚

theory Involutory =
  include ?Monoid❙
  involutory: {x} ⊦ involution x❙
  
  inverse_refl : {x} ⊦ inverse x x❘
               = [x] involution_inverse equivEl involutory❙
  inverse_ident : {x,y} ⊦ inverse x y ⟶ ⊦ x≐y❘
                = [x,y,p] inverse_unique inverse_refl p❙
❚

theory IdempotentMonoid = 
  include ?Monoid❙
  include ?Band❙
❚

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

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