namespace latin:/algebraic❚

fixmeta latin:/?SFOLEQND❚

theory AdditiveSet = 
  structure add : ?Set❙
❚

theory AdditiveMagma = 
  include ?AdditiveSet❙
  structure add : ?Magma =
    include ?AdditiveSet/add❙
    op # 1 + 2 prec 40❙
  ❚
❚

theory AdditiveCommutative = 
  include ?AdditiveMagma ❙
  structure add : ?Commutative =
    include ?AdditiveMagma/add❙
  ❚
❚

theory AdditiveIdempotent = 
  include ?AdditiveMagma ❙
  structure add : ?Idempotent =
    include ?AdditiveMagma/add❙
  ❚
❚

theory AdditiveSemigroup = 
  include ?AdditiveMagma❙
  structure add : ?Semigroup =
    include ?AdditiveMagma/add❙
  ❚
❚

theory AdditiveCommSemigroup = 
  include ?AdditiveSemigroup❙
  include ?AdditiveCommutative❙
  structure add : ?CommSemigroup =
    include ?AdditiveSemigroup/add❙
    include ?AdditiveCommutative/add❙
  ❚
❚