diff --git a/Manifest.toml b/Manifest.toml
index d32678dd8..b8fa4d0dd 100644
--- a/Manifest.toml
+++ b/Manifest.toml
@@ -119,9 +119,9 @@ uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb"
 
 [[Libiconv_jll]]
 deps = ["Libdl", "Pkg"]
-git-tree-sha1 = "e5256a3b0ebc710dbd6da0c0b212164a3681037f"
+git-tree-sha1 = "a06937d9aa48855f52484c9a77a2670158fa90e2"
 uuid = "94ce4f54-9a6c-5748-9c1c-f9c7231a4531"
-version = "1.16.0+2"
+version = "1.16.0+4"
 
 [[LightGraphs]]
 deps = ["ArnoldiMethod", "DataStructures", "Distributed", "Inflate", "LinearAlgebra", "Random", "SharedArrays", "SimpleTraits", "SparseArrays", "Statistics"]
@@ -285,12 +285,12 @@ uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5"
 
 [[XML2_jll]]
 deps = ["Libdl", "Libiconv_jll", "Pkg", "Zlib_jll"]
-git-tree-sha1 = "987c02a43fa10a491a5f0f7c46a6d3559ed6a8e2"
+git-tree-sha1 = "6b2ffe6728bdba991da4fc1aa5980a53db46a23f"
 uuid = "02c8fc9c-b97f-50b9-bbe4-9be30ff0a78a"
-version = "2.9.9+4"
+version = "2.9.9+5"
 
 [[Zlib_jll]]
 deps = ["Libdl", "Pkg"]
-git-tree-sha1 = "2f6c3e15e20e036ee0a0965879b31442b7ec50fa"
+git-tree-sha1 = "33d31d2b2a24d2fdbc60633b68229ee462811c8b"
 uuid = "83775a58-1f1d-513f-b197-d71354ab007a"
-version = "1.2.11+9"
+version = "1.2.11+13"
diff --git a/Project.toml b/Project.toml
index 9db6e10af..004718e4a 100644
--- a/Project.toml
+++ b/Project.toml
@@ -23,6 +23,7 @@ Pkg = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f"
 Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
 Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
 Requires = "ae029012-a4dd-5104-9daa-d747884805df"
+SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
 StaticArrays = "90137ffa-7385-5640-81b9-e52037218182"
 Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
diff --git a/docs/literate/graphics/composejl_wiring_diagrams.jl b/docs/literate/graphics/composejl_wiring_diagrams.jl
index 2cb40b927..dc6e66231 100644
--- a/docs/literate/graphics/composejl_wiring_diagrams.jl
+++ b/docs/literate/graphics/composejl_wiring_diagrams.jl
@@ -98,16 +98,15 @@ to_composejl((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dco
 # ### Abelian bicategory of relations
 
 # In an abelian bicategory of relations, such as the category of linear
-# relations, the duplication morphisms $\Delta_X: X \to X \otimes X$ and
-# addition morphisms $\blacktriangledown_X: X \otimes X \to X$ belong to a
-# bimonoid. Among other things, this means that the following two morphisms are
-# equal.
+# relations, the duplication morphisms $\Delta_X: X \to X \oplus X$ and addition
+# morphisms $\blacktriangledown_X: X \oplus X \to X$ belong to a bimonoid. Among
+# other things, this means that the following two morphisms are equal.
 
 X = Ob(FreeAbelianBicategoryRelations, :X)
 
 to_composejl(plus(X) ⋅ mcopy(X))
 #-
-to_composejl((mcopy(X)⊗mcopy(X)) ⋅ (id(X)⊗braid(X,X)⊗id(X)) ⋅ (plus(X)⊗plus(X)))
+to_composejl((mcopy(X)⊕mcopy(X)) ⋅ (id(X)⊕swap(X,X)⊕id(X)) ⋅ (plus(X)⊕plus(X)))
 
 # ## Custom styles
 
diff --git a/docs/literate/graphics/tikz_wiring_diagrams.jl b/docs/literate/graphics/tikz_wiring_diagrams.jl
index a1465f06c..6841daac1 100644
--- a/docs/literate/graphics/tikz_wiring_diagrams.jl
+++ b/docs/literate/graphics/tikz_wiring_diagrams.jl
@@ -102,16 +102,15 @@ to_tikz((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dcounit(
 # ### Abelian bicategory of relations
 
 # In an abelian bicategory of relations, such as the category of linear
-# relations, the duplication morphisms $\Delta_X: X \to X \otimes X$ and
-# addition morphisms $\blacktriangledown_X: X \otimes X \to X$ belong to a
-# bimonoid. Among other things, this means that the following two morphisms are
-# equal.
+# relations, the duplication morphisms $\Delta_X: X \to X \oplus X$ and addition
+# morphisms $\blacktriangledown_X: X \oplus X \to X$ belong to a bimonoid. Among
+# other things, this means that the following two morphisms are equal.
 
 X = Ob(FreeAbelianBicategoryRelations, :X)
 
 to_tikz(plus(X) ⋅ mcopy(X))
 #-
-to_tikz((mcopy(X)⊗mcopy(X)) ⋅ (id(X)⊗braid(X,X)⊗id(X)) ⋅ (plus(X)⊗plus(X)))
+to_composejl((mcopy(X)⊕mcopy(X)) ⋅ (id(X)⊕swap(X,X)⊕id(X)) ⋅ (plus(X)⊕plus(X)))
 
 # ## Custom styles
 
diff --git a/src/categorical_algebra/CategoricalAlgebra.jl b/src/categorical_algebra/CategoricalAlgebra.jl
index b4f902af8..fbdc06563 100644
--- a/src/categorical_algebra/CategoricalAlgebra.jl
+++ b/src/categorical_algebra/CategoricalAlgebra.jl
@@ -1,7 +1,9 @@
 module CategoricalAlgebra
 
 include("ShapeDiagrams.jl")
+include("Matrices.jl")
 include("FinSets.jl")
+include("FinRelations.jl")
 include("Permutations.jl")
 
 end
diff --git a/src/categorical_algebra/FinRelations.jl b/src/categorical_algebra/FinRelations.jl
new file mode 100644
index 000000000..ce7a1b891
--- /dev/null
+++ b/src/categorical_algebra/FinRelations.jl
@@ -0,0 +1,28 @@
+""" Computing in the category of finite sets and relations, and its skeleton.
+"""
+module FinRelations
+export BoolRig, RelationMatrix
+
+import Base: +, *, zero, one
+using AutoHashEquals
+
+using ..Matrices
+
+""" The rig of booleans.
+
+This struct is needed because in base Julia, the product of booleans is another
+boolean, but a sum of booleans is coerced to an integer: `true + true == 2`.
+"""
+@auto_hash_equals struct BoolRig
+  value::Bool
+end
++(x::BoolRig, y::BoolRig) = x.value || y.value
+*(x::BoolRig, y::BoolRig) = x.value && y.value
+zero(::Type{BoolRig}) = false
+one(::Type{BoolRig}) = true
+
+""" A relation matrix, also known as a boolean matrix or logical matrix.
+"""
+const RelationMatrix = AbstractMatrix{BoolRig}
+
+end
diff --git a/src/categorical_algebra/FinSets.jl b/src/categorical_algebra/FinSets.jl
index 513f04723..69500e332 100644
--- a/src/categorical_algebra/FinSets.jl
+++ b/src/categorical_algebra/FinSets.jl
@@ -1,3 +1,5 @@
+""" Computing in the category of finite sets and functions, and its skeleton.
+"""
 module FinSets
 export FinOrd, FinOrdFunction, force, terminal, product, equalizer, pullback,
   initial, coproduct, coequalizer, pushout
@@ -7,9 +9,9 @@ using DataStructures: IntDisjointSets, union!, find_root
 
 using ...GAT
 using ...Theories: Category
-using ..ShapeDiagrams
 import ...Theories: dom, codom, id, compose, ⋅, ∘,
   terminal, product, equalizer, initial, coproduct, coequalizer
+using ..ShapeDiagrams
 
 # Data types
 ############
diff --git a/src/categorical_algebra/Matrices.jl b/src/categorical_algebra/Matrices.jl
new file mode 100644
index 000000000..1f2381859
--- /dev/null
+++ b/src/categorical_algebra/Matrices.jl
@@ -0,0 +1,110 @@
+""" Categories of matrices.
+"""
+module Matrices
+export MatrixDom, dom, codom, id, compose, ⋅, ∘,
+  otimes, ⊗, munit, braid, oplus, ⊕, mzero, swap,
+  mcopy, Δ, delete, ◊, plus, zero, pair, copair, proj1, proj2, coproj1, coproj2
+
+import Base: +, *, zero, one
+using LinearAlgebra: I
+using SparseArrays
+import SparseArrays: blockdiag
+
+using ...GAT
+using ...Theories: DistributiveSemiadditiveCategory
+import ...Theories: dom, codom, id, compose, ⋅, ∘,
+  otimes, ⊗, munit, braid, oplus, ⊕, mzero, swap,
+  mcopy, Δ, delete, ◊, plus, zero, pair, copair, proj1, proj2, coproj1, coproj2
+
+# Matrices over a commutative rig
+#################################
+
+""" Domain or codomain of a Julia matrix of a specific type.
+
+Object in the category of matrices of this type.
+"""
+struct MatrixDom{M <: AbstractMatrix}
+  dim::Int
+end
+
++(m::MD, n::MD) where MD <: MatrixDom = MD(m.dim + n.dim)
+*(m::MD, n::MD) where MD <: MatrixDom = MD(m.dim * n.dim)
+zero(::Type{MD}) where MD <: MatrixDom = MD(0)
+one(::Type{MD}) where MD <: MatrixDom = MD(1)
+
+""" Biproduct category of Julia matrices of specific type.
+
+The matrices can be dense or sparse, and the element type can be any
+[commutative rig](https://ncatlab.org/nlab/show/rig) (commutative semiring): any
+Julia type implementing `+`, `*`, `zero`, `one` and obeying the axioms. Note
+that commutativity is required only in order to define `braid`.
+
+For a similar design (only for sparse matrices) by the Julia core developers,
+see [SemiringAlgebra.jl](https://github.com/JuliaComputing/SemiringAlgebra.jl)
+and [accompanying short paper](https://doi.org/10.1109/HPEC.2013.6670347).
+"""
+@instance DistributiveSemiadditiveCategory(MatrixDom, AbstractMatrix) begin
+  # FIXME: Cannot define type-parameterized instances.
+  #@instance AdditiveBiproductCategory(MatrixDom{M}, M) where M <: AbstractMatrix begin
+  @import +, dom, codom, id, mzero, munit, braid
+  
+  compose(A::AbstractMatrix, B::AbstractMatrix) = B*A
+  plus(A::AbstractMatrix, B::AbstractMatrix) = A+B
+  
+  oplus(m::MatrixDom, n::MatrixDom) = m+n
+  oplus(A::AbstractMatrix, B::AbstractMatrix) = blockdiag(A, B)
+  swap(m::MatrixDom, n::MatrixDom) = [zero(n,m) id(n); id(m) zero(m,n)]
+  
+  otimes(m::MatrixDom, n::MatrixDom) = m*n
+  otimes(A::AbstractMatrix, B::AbstractMatrix) = kron(A, B)
+  
+  mcopy(m::MatrixDom) = pair(id(m), id(m))
+  delete(m::MatrixDom) = zero(zero(typeof(m)), m)
+  plus(m::MatrixDom) = copair(id(m), id(m))
+  zero(m::MatrixDom) = zero(m, zero(typeof(m)))
+  
+  pair(A::AbstractMatrix, B::AbstractMatrix) = [A; B]
+  copair(A::AbstractMatrix, B::AbstractMatrix) = [A B]
+  proj1(m::MatrixDom, n::MatrixDom) = [id(m) zero(m,n)]
+  proj2(m::MatrixDom, n::MatrixDom) = [zero(n,m) id(n)]
+  coproj1(m::MatrixDom, n::MatrixDom) = [id(m); zero(n,m)]
+  coproj2(m::MatrixDom, n::MatrixDom) = [zero(m,n); id(n)]
+end
+
+dom(A::M) where M <: AbstractMatrix = MatrixDom{M}(size(A,2))
+codom(A::M) where M <: AbstractMatrix = MatrixDom{M}(size(A,1))
+
+id(m::MatrixDom{M}) where M = M(I, m.dim, m.dim)
+mzero(::Type{MD}) where MD <: MatrixDom = MD(0)
+munit(::Type{MD}) where MD <: MatrixDom = MD(1)
+braid(m::MatrixDom{M}, n::MatrixDom{M}) where M =
+  vec_permutation_matrix(M, m.dim, n.dim)
+zero(m::MatrixDom{M}, n::MatrixDom{M}) where M = zero_matrix(M, m.dim, n.dim)
+
+# Matrix utilities
+##################
+
+# Block diagonal only implemented for sparse matrices.
+blockdiag(A::AbstractMatrix...) = cat(A..., dims=(1,2))
+
+# Dense and sparse matrices have different APIs for creating zero matrices.
+zero_matrix(::Type{<:AbstractMatrix{T}}, dims...) where T = zeros(T, dims...)
+zero_matrix(::Type{SparseMatrixCSC{T}}, dims...) where T = spzeros(T, dims...)
+
+function unit_vector(::Type{M}, n::Int, i::Int) where {T, M <: AbstractMatrix{T}}
+  x = zero_matrix(M, n, 1)
+  x[i,1] = one(T)
+  x
+end
+
+""" The "vec-permutation" matrix, aka the "perfect shuffle" permutation matrix.
+
+This formula is (Henderson & Searle, 1981, "The vec-permutation matrix, the vec
+operator and Kronecker products: a review", Equation 18). Many other formulas
+are given there.
+"""
+function vec_permutation_matrix(::Type{M}, m::Int, n::Int) where M <: AbstractMatrix
+  hcat((kron(M(I, n, n), unit_vector(M, m, j)) for j in 1:m)...)
+end
+
+end
diff --git a/src/graphics/WiringDiagramLayouts.jl b/src/graphics/WiringDiagramLayouts.jl
index c83713fa2..007bbd4a1 100644
--- a/src/graphics/WiringDiagramLayouts.jl
+++ b/src/graphics/WiringDiagramLayouts.jl
@@ -159,11 +159,12 @@ layout_hom_expr(f::HomExpr, opts) = layout_box(f, opts)
 
 layout_hom_expr(f::HomExpr{:compose}, opts) =
   compose_with_layout!(map(arg -> layout_hom_expr(arg, opts), args(f)), opts)
-layout_hom_expr(f::HomExpr{:otimes}, opts) =
+layout_hom_expr(f::Union{HomExpr{:otimes},HomExpr{:oplus}}, opts) =
   otimes_with_layout!(map(arg -> layout_hom_expr(arg, opts), args(f)), opts)
 
 layout_hom_expr(f::HomExpr{:id}, opts) = layout_pure_wiring(f, opts)
-layout_hom_expr(f::HomExpr{:braid}, opts) = layout_pure_wiring(f, opts)
+layout_hom_expr(f::Union{HomExpr{:braid},HomExpr{:swap}}, opts) =
+  layout_pure_wiring(f, opts)
 
 layout_hom_expr(f::HomExpr{:mcopy}, opts) = layout_supply(f, opts, shape=:junction)
 layout_hom_expr(f::HomExpr{:delete}, opts) = layout_supply(f, opts, shape=:junction)
diff --git a/src/linear_algebra/GLA.jl b/src/linear_algebra/GLA.jl
index 1e1fe3faf..cf27f10bc 100644
--- a/src/linear_algebra/GLA.jl
+++ b/src/linear_algebra/GLA.jl
@@ -1,13 +1,11 @@
 module GraphicalLinearAlgebra
 export LinearFunctions, FreeLinearFunctions, LinearRelations,
-  FreeLinearRelations, LinearMapDom, LinearMap,
-  LinearOpDom, LinearOperator,
-  Ob, Hom, dom, codom, compose, ⋅, ∘, id, oplus, ⊕, mzero, braid,
+  FreeLinearRelations, LinearMapDom, LinearMap, LinearOpDom, LinearOperator,
+  Ob, Hom, dom, codom, compose, ⋅, ∘, id, oplus, ⊕, mzero, swap,
   dagger, dunit, docunit, mcopy, Δ, delete, ◊, mmerge, ∇, create, □,
-  pplus, zero, coplus, cozero, plus, +, meet, top, join, bottom,
+  plus, +, zero, coplus, cozero, meet, top, join, bottom,
   scalar, antipode, antipode, adjoint, evaluate
 
-import Base: +
 using AutoHashEquals
 using LinearMaps
 import LinearMaps: adjoint
@@ -18,9 +16,9 @@ import LinearOperators:
 
 using ...Catlab, ...Theories
 import ...Theories:
-  Ob, Hom, dom, codom, compose, ⋅, ∘, id, oplus, ⊕, mzero, braid,
+  Ob, Hom, dom, codom, compose, ⋅, ∘, id, oplus, ⊕, mzero, swap,
   dagger, dunit, dcounit, mcopy, Δ, delete, ◊, mmerge, ∇, create, □,
-  plus, zero, coplus, cozero, meet, top, join, bottom
+  plus, +, zero, coplus, cozero, meet, top, join, bottom
 using ...Programs
 import ...Programs: evaluate_hom
 
@@ -31,46 +29,23 @@ import ...Programs: evaluate_hom
 
 Functional fragment of graphical linear algebra.
 """
-@theory AdditiveSymmetricMonoidalCategory(Ob,Hom) => LinearFunctions(Ob,Hom) begin
-  # Copying and deleting maps.
-  mcopy(A::Ob)::(A → (A ⊕ A))
-  @op (Δ) := mcopy
-  delete(A::Ob)::(A → mzero())
-  @op (◊) := delete
-
-  # Addition and zero maps.
-  plus(A::Ob)::((A ⊕ A) → A)
-  @op (+) := plus
-  zero(A::Ob)::(mzero() → A)
-
-  plus(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
+@theory SemiadditiveCategory(Ob,Hom) => LinearFunctions(Ob,Hom) begin
   adjoint(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
-
+  
   scalar(A::Ob, c::Number)::(A → A)
   antipode(A::Ob)::(A → A)
 
-  # Axioms
-  antipode(A) == scalar(A, -1) ⊣ (A::Ob)
-
-  Δ(A) == Δ(A) ⋅ σ(A,A) ⊣ (A::Ob)
-  Δ(A) ⋅ (Δ(A) ⊕ id(A)) == Δ(A) ⋅ (id(A) ⊕ Δ(A)) ⊣ (A::Ob)
-  Δ(A) ⋅ (◊(A) ⊕ id(A)) == id(A) ⊣ (A::Ob)
-  plus(A) == σ(A,A) ⋅ plus(A) ⊣ (A::Ob)
-  (plus(A) ⊕ id(A)) ⋅ plus(A) == (id(A) ⊕ plus(A)) ⋅ plus(A) ⊣ (A::Ob)
-  (zero(A) ⊕ id(A)) ⋅ plus(A) == id(A) ⊣ (A::Ob)
-  plus(A) ⋅ Δ(A) == ((Δ(A) ⊕ Δ(A)) ⋅ (id(A) ⊕ (σ(A, A) ⊕ id(A)))) ⋅ (plus(A) ⊕ plus(A)) ⊣ (A::Ob)
-  plus(A) ⋅ ◊(A) == ◊(A) ⊕ ◊(A) ⊣ (A::Ob)
-  zero(A) ⋅ Δ(A) == zero(A) ⊕ zero(A) ⊣ (A::Ob)
-  zero(A) ⋅ ◊(A) == id(mzero()) ⊣ (A::Ob)
+  # Scalar and antipode axioms.
   scalar(A, a) ⋅ scalar(A, b) == scalar(A, a*b) ⊣ (A::Ob, a::Number, b::Number)
   scalar(A, 1) == id(A) ⊣ (A::Ob)
   scalar(A, a) ⋅ Δ(A) == Δ(A) ⋅ (scalar(A, a) ⊕ scalar(A, a)) ⊣ (A::Ob, a::Number)
   scalar(A, a) ⋅ ◊(A) == ◊(A) ⊣ (A::Ob, a::Number)
-  (Δ(A) ⋅ (scalar(A, a) ⊕ scalar(A, b))) ⋅ plus(A) == scalar(A, a+b) ⊣ (A::Ob, a::Number, b::Number)
+  Δ(A) ⋅ (scalar(A, a) ⊕ scalar(A, b)) ⋅ plus(A) == scalar(A, a+b) ⊣ (A::Ob, a::Number, b::Number)
   scalar(A, 0) == ◊(A) ⋅ zero(A) ⊣ (A::Ob)
   zero(A) ⋅ scalar(A, a) == zero(A) ⊣ (A::Ob, a::Number)
+  antipode(A) == scalar(A, -1) ⊣ (A::Ob)
 
-  plus(A) ⋅ f == (f ⊕ f) ⋅ plus(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  # Homogeneity axiom. Additivity is inherited from `SemiadditiveCategory`.
   scalar(A, c) ⋅ f == f ⋅ scalar(B, c) ⊣ (A::Ob, B::Ob, c::Number, f::(A → B))
 end
 
@@ -82,38 +57,24 @@ end
 
 """ Theory of *linear relations*
 
-The full relational language of graphical linear algebra. This is an abelian
-bicategory of relations (`AbelianBicategoryRelations`), written additively.
+The full relational language of graphical linear algebra.
 """
-@signature LinearFunctions(Ob,Hom) => LinearRelations(Ob,Hom) begin
-  # Dagger category.
-  dagger(f::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
-
-  # Self-dual compact closed category.
-  dunit(A::Ob)::(mzero() → (A ⊕ A))
-  dcounit(A::Ob)::((A ⊕ A) → mzero())
-
-  # Merging and creating relations (converses of copying and deleting maps).
-  mmerge(A::Ob)::((A ⊕ A) → A)
-  @op (∇) := mmerge
-  create(A::Ob)::(mzero() → A)
-  @op (□) := create
-
-  # Co-addition and co-zero relations (converses of addition and zero maps)
-  coplus(A::Ob)::(A → (A ⊕ A))
-  cozero(A::Ob)::(A → mzero())
-
-  # Lattice of linear relations.
-  meet(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
-  top(A::Ob, B::Ob)::(A → B)
-  join(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
-  bottom(A::Ob, B::Ob)::(A → B)
+@theory AbelianBicategoryRelations(Ob,Hom) => LinearRelations(Ob,Hom) begin
+  adjoint(R::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
+
+  scalar(A::Ob, c::Number)::(A → A)
+  antipode(A::Ob)::(A → A)
+
+  # Linearity axioms.
+  plus(A)⋅R == (R⊕R)⋅plus(B) ⊣ (A::Ob, B::Ob, R::(A → B))
+  zero(A)⋅R == zero(B) ⊣ (A::Ob, B::Ob, R::(A → B))
+  scalar(A, c) ⋅ R == R ⋅ scalar(B, c) ⊣ (A::Ob, B::Ob, c::Number, R::(A → B))
 end
 
 @syntax FreeLinearRelations(ObExpr,HomExpr) LinearRelations begin
   oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
-  oplus(f::Hom, g::Hom) = associate(new(f,g))
-  compose(f::Hom, g::Hom) = new(f,g; strict=true) # No normalization!
+  oplus(R::Hom, S::Hom) = associate(new(R,S))
+  compose(R::Hom, S::Hom) = new(R,S; strict=true) # No normalization!
 end
 
 # Evaluation
@@ -138,8 +99,8 @@ end
   oplus(V::LinearMapDom, W::LinearMapDom) = LinearMapDom(V.N + W.N)
   oplus(f::LinearMap, g::LinearMap) = LMs.BlockDiagonalMap(f, g)
   mzero(::Type{LinearMapDom}) = LinearMapDom(0)
-  braid(V::LinearMapDom, W::LinearMapDom) =
-    LinearMap(braid_lm(V.N), braid_lm(W.N), W.N+V.N, V.N+W.N)
+  swap(V::LinearMapDom, W::LinearMapDom) =
+    LinearMap(swap_lm(V.N), swap_lm(W.N), W.N+V.N, V.N+W.N)
 
   mcopy(V::LinearMapDom) = LinearMap(mcopy_lm, plus_lm, 2*V.N, V.N)
   delete(V::LinearMapDom) = LinearMap(delete_lm, zero_lm(V.N), 0, V.N)
@@ -149,9 +110,16 @@ end
   plus(f::LinearMap, g::LinearMap) = f+g
   scalar(V::LinearMapDom, c::Number) = LMs.UniformScalingMap(c, V.N)
   antipode(V::LinearMapDom) = LMs.UniformScalingMap(-1, V.N)
+  
+  pair(f::LinearMap, g::LinearMap) = mcopy(dom(f)) ⋅ (f ⊕ g)
+  copair(f::LinearMap, g::LinearMap) = (f ⊕ g) ⋅ plus(codom(f))
+  proj1(A::LinearMapDom, B::LinearMapDom) = id(A) ⊕ delete(B)
+  proj2(A::LinearMapDom, B::LinearMapDom) = delete(A) ⊕ id(B)
+  coproj1(A::LinearMapDom, B::LinearMapDom) = id(A) ⊕ zero(B)
+  coproj2(A::LinearMapDom, B::LinearMapDom) = zero(A) ⊕ id(B)
 end
 
-braid_lm(n::Int) = x::AbstractVector -> vcat(x[n+1:end], x[1:n])
+swap_lm(n::Int) = x::AbstractVector -> vcat(x[n+1:end], x[1:n])
 mcopy_lm(x::AbstractVector) = vcat(x, x)
 delete_lm(x::AbstractVector) = eltype(x)[]
 plus_lm(x::AbstractVector) = begin
@@ -189,7 +157,7 @@ end
     fOp + gOp
   end
   mzero(::Type{LinearOpDom}) = LinearOpDom(0)
-  braid(V::LinearOpDom, W::LinearOpDom) =
+  swap(V::LinearOpDom, W::LinearOpDom) =
     opExtension(1:W.N, V.N+W.N) * opRestriction((V.N+1):(V.N+W.N),V.N+W.N) +
     opExtension((W.N+1):(V.N+W.N), V.N+W.N) * opRestriction(1:V.N,V.N+W.N)
   mcopy(V::LinearOpDom) =
@@ -202,9 +170,15 @@ end
   plus(f::LinearOperator, g::LinearOperator) = f+g
   scalar(V::LinearOpDom, c::Number) = opEye(typeof(c),V.N)*c
   antipode(V::LinearOpDom) = scalar(V,-1)
+  
+  pair(f::LinearOperator, g::LinearOperator) = mcopy(dom(f)) ⋅ (f ⊕ g)
+  copair(f::LinearOperator, g::LinearOperator) = (f ⊕ g) ⋅ plus(codom(f))
+  proj1(A::LinearOpDom, B::LinearOpDom) = id(A) ⊕ delete(B)
+  proj2(A::LinearOpDom, B::LinearOpDom) = delete(A) ⊕ id(B)
+  coproj1(A::LinearOpDom, B::LinearOpDom) = id(A) ⊕ zero(B)
+  coproj2(A::LinearOpDom, B::LinearOpDom) = zero(A) ⊕ id(B)
 end
 
-
 # Catlab evaluate
 #----------------
 
diff --git a/src/theories/AdditiveMonoidal.jl b/src/theories/AdditiveMonoidal.jl
deleted file mode 100644
index b5be6ea5a..000000000
--- a/src/theories/AdditiveMonoidal.jl
+++ /dev/null
@@ -1,120 +0,0 @@
-export AdditiveMonoidalCategory, oplus, ⊕, mzero,
-  AdditiveSymmetricMonoidalCategory, FreeAdditiveSymmetricMonoidalCategory,
-  MonoidalCategoryWithCodiagonals, CocartesianCategory, FreeCocartesianCategory,
-  mmerge, create, copair, coproj1, coproj2, ∇, □, braid, σ
-
-import Base: collect, ndims
-
-# Monoidal category
-###################
-
-""" Theory of *monoidal categories*, in additive notation
-
-Mathematically the same as `MonoidalCategory` but with different notation.
-"""
-@signature Category(Ob,Hom) => AdditiveMonoidalCategory(Ob,Hom) begin
-  oplus(A::Ob, B::Ob)::Ob
-  oplus(f::Hom(A,B), g::Hom(C,D))::Hom(oplus(A,C),oplus(B,D)) <=
-    (A::Ob, B::Ob, C::Ob, D::Ob)
-  @op (⊕) := oplus
-  mzero()::Ob
-end
-
-# Convenience constructors
-oplus(xs::Vector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
-oplus(x, y, z, xs...) = oplus([x, y, z, xs...])
-
-# Overload `collect` and `ndims` as for multiplicative monoidal categories.
-collect(expr::ObExpr{:oplus}) = vcat(map(collect, args(expr))...)
-collect(expr::ObExpr{:mzero}) = roottypeof(expr)[]
-ndims(expr::ObExpr{:oplus}) = sum(map(ndims, args(expr)))
-ndims(expr::ObExpr{:mzero}) = 0
-
-function show_unicode(io::IO, expr::Union{ObExpr{:oplus},HomExpr{:oplus}}; kw...)
-  Syntax.show_unicode_infix(io, expr, "⊕"; kw...)
-end
-show_unicode(io::IO, expr::ObExpr{:mzero}; kw...) = print(io, "O")
-
-function show_latex(io::IO, expr::Union{ObExpr{:oplus},HomExpr{:oplus}}; kw...)
-  Syntax.show_latex_infix(io, expr, "\\oplus"; kw...)
-end
-show_latex(io::IO, expr::ObExpr{:mzero}; kw...) = print(io, "O")
-
-# Symmetric monoidal category
-#############################
-
-""" Theory of *symmetric monoidal categories*, in additive notation
-
-Mathematically the same as `SymmetricMonoidalCategory` but with different
-notation.
-"""
-@signature AdditiveMonoidalCategory(Ob,Hom) => AdditiveSymmetricMonoidalCategory(Ob,Hom) begin
-  braid(A::Ob, B::Ob)::Hom(oplus(A,B),oplus(B,A))
-  @op (σ) := braid
-end
-
-@syntax FreeAdditiveSymmetricMonoidalCategory(ObExpr,HomExpr) AdditiveSymmetricMonoidalCategory begin
-  oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
-  oplus(f::Hom, g::Hom) = associate(new(f,g))
-  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-end
-
-# Cocartesian category
-######################
-
-""" Theory of *monoidal categories with codiagonals*
-
-A monoidal category with codiagonals is a symmetric monoidal category equipped
-with coherent collections of merging and creating morphisms (monoids).
-Unlike in a cocartesian category, the naturality axioms need not be satisfied.
-
-For references, see `MonoidalCategoryWithDiagonals`.
-"""
-@signature AdditiveSymmetricMonoidalCategory(Ob,Hom) => MonoidalCategoryWithCodiagonals(Ob,Hom) begin
-  mmerge(A::Ob)::Hom(oplus(A,A),A)
-  @op (∇) := mmerge
-  create(A::Ob)::Hom(mzero(),A)
-  @op (□) := create
-end
-
-""" Theory of *cocartesian (monoidal) categories*
-
-For the traditional axiomatization of coproducts, see
-[`CategoryWithCoproducts`](@ref).
-"""
-@theory MonoidalCategoryWithCodiagonals(Ob,Hom) => CocartesianCategory(Ob,Hom) begin
-  copair(f::Hom(A,C), g::Hom(B,C))::Hom(oplus(A,B),C) <= (A::Ob, B::Ob, C::Ob)
-  coproj1(A::Ob, B::Ob)::Hom(A,oplus(A,B))
-  coproj2(A::Ob, B::Ob)::Hom(B,oplus(A,B))
-  
-  copair(f,g) == (f⊗g)⋅∇(C) ⊣ (A::Ob, B::Ob, C::Ob, f::(A → C), g::(B → C))
-  coproj1(A,B) == id(A)⊗□(B) ⊣ (A::Ob, B::Ob)
-  coproj2(A,B) == □(A)⊗id(B) ⊣ (A::Ob, B::Ob)
-  
-  # Naturality axioms.
-  ∇(A)⋅f == (f⊗f)⋅∇(B) ⊣ (A::Ob, B::Ob, f::(A → B))
-  □(A)⋅f == □(B) ⊣ (A::Ob, B::Ob, f::(A → B))
-end
-
-""" Syntax for a free cocartesian category.
-
-In this syntax, the copairing and inclusion operations are defined using merging
-and creation, and do not have their own syntactic elements. This convention
-could be dropped or reversed.
-"""
-@syntax FreeCocartesianCategory(ObExpr,HomExpr) CocartesianCategory begin
-  oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
-  oplus(f::Hom, g::Hom) = associate(new(f,g))
-  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-
-  copair(f::Hom, g::Hom) = compose(oplus(f,g), mmerge(codom(f)))
-  coproj1(A::Ob, B::Ob) = oplus(id(A), create(B))
-  coproj2(A::Ob, B::Ob) = oplus(create(A), id(B))
-end
-
-function show_latex(io::IO, expr::HomExpr{:mmerge}; kw...)
-  Syntax.show_latex_script(io, expr, "\\nabla")
-end
-function show_latex(io::IO, expr::HomExpr{:create}; kw...)
-  Syntax.show_latex_script(io, expr, "\\square")
-end
diff --git a/src/theories/Monoidal.jl b/src/theories/Monoidal.jl
index 254b5a467..256017724 100644
--- a/src/theories/Monoidal.jl
+++ b/src/theories/Monoidal.jl
@@ -89,11 +89,14 @@ end
 """ Theory of *monoidal categories with diagonals*
 
 A monoidal category with diagonals is a symmetric monoidal category equipped
-with coherent collections of copying and deleting morphisms (comonoids).
-Unlike in a cartesian category, the naturality axioms need not be satisfied.
+with coherent operations of copying and deleting, also known as a supply of
+commutative comonoids. Unlike in a cartesian category, the naturality axioms
+need not be satisfied.
 
 References:
 
+- Fong & Spivak, 2019, "Supplying bells and whistles in symmetric monoidal
+  categories" ([arxiv:1908.02633](https://arxiv.org/abs/1908.02633))
 - Selinger, 2010, "A survey of graphical languages for monoidal categories",
   Section 6.6: "Cartesian center"
 - Selinger, 1999, "Categorical structure of asynchrony"
@@ -153,39 +156,40 @@ end
 """ Theory of *monoidal categories with bidiagonals*
 
 The terminology is nonstandard (is there any standard terminology?) but is
-intended to mean a monoidal category with coherent diagonals and codiagonals.
+supposed to mean a monoidal category with coherent diagonals and codiagonals.
 Unlike in a biproduct category, the naturality axioms need not be satisfied.
-
-FIXME: This theory should extend both `MonoidalCategoryWithDiagonals` and
-`MonoidalCategoryWithCodiagonals`, but multiple inheritance is not yet
-supported.
 """
-@signature SymmetricMonoidalCategory(Ob,Hom) => MonoidalCategoryWithBidiagonals(Ob,Hom) begin
-  mcopy(A::Ob)::(A → (A ⊗ A))
-  @op (Δ) := mcopy
+@signature MonoidalCategoryWithDiagonals(Ob,Hom) => MonoidalCategoryWithBidiagonals(Ob,Hom) begin
   mmerge(A::Ob)::((A ⊗ A) → A)
   @op (∇) := mmerge
-  delete(A::Ob)::(A → munit())
-  @op (◊) := delete
   create(A::Ob)::(munit() → A)
   @op (□) := create
 end
 
 """ Theory of *biproduct categories*
 
-Also known as *semiadditive categories*.
-
-FIXME: This theory should extend `MonoidalCategoryWithBidiagonals`,
-`CartesianCategory`, and `CocartesianCategory`, but multiple inheritance is not
-yet supported.
+Mathematically the same as [`SemiadditiveCategory`](@ref) but written
+multiplicatively, instead of additively.
 """
-@signature MonoidalCategoryWithBidiagonals(Ob,Hom) => BiproductCategory(Ob,Hom) begin
+@theory MonoidalCategoryWithBidiagonals(Ob,Hom) => BiproductCategory(Ob,Hom) begin
   pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
   copair(f::(A → C), g::(B → C))::((A ⊗ B) → C) ⊣ (A::Ob, B::Ob, C::Ob)
   proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
   proj2(A::Ob, B::Ob)::((A ⊗ B) → B)
   coproj1(A::Ob, B::Ob)::(A → (A ⊗ B))
   coproj2(A::Ob, B::Ob)::(B → (A ⊗ B))
+  
+  # Naturality axioms.
+  f⋅Δ(B) == Δ(A)⋅(f⊗f) ⊣ (A::Ob, B::Ob, f::(A → B))
+  f⋅◊(B) == ◊(A) ⊣ (A::Ob, B::Ob, f::(A → B))
+  ∇(A)⋅f == (f⊗f)⋅∇(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  □(A)⋅f == □(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  
+  # Bimonoid axioms. (These follow from naturality + coherence axioms.)
+  ∇(A)⋅Δ(A) == (Δ(A)⊗Δ(A)) ⋅ (id(A)⊗σ(A,A)⊗id(A)) ⋅ (∇(A)⊗∇(A)) ⊣ (A::Ob)
+  ∇(A)⋅◊(A) == ◊(A) ⊗ ◊(A) ⊣ (A::Ob)
+  □(A)⋅Δ(A) == □(A) ⊗ □(A) ⊣ (A::Ob)
+  □(A)⋅◊(A) == id(munit()) ⊣ (A::Ob)
 end
 
 @syntax FreeBiproductCategory(ObExpr,HomExpr) BiproductCategory begin
@@ -193,14 +197,21 @@ end
   otimes(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 
-  pair(f::Hom, g::Hom) = Δ(dom(f)) → (f ⊗ g)
-  copair(f::Hom, g::Hom) = (f ⊗ g) → ∇(codom(f))
+  pair(f::Hom, g::Hom) = Δ(dom(f)) ⋅ (f ⊗ g)
+  copair(f::Hom, g::Hom) = (f ⊗ g) ⋅ ∇(codom(f))
   proj1(A::Ob, B::Ob) = id(A) ⊗ ◊(B)
   proj2(A::Ob, B::Ob) = ◊(A) ⊗ id(B)
   coproj1(A::Ob, B::Ob) = id(A) ⊗ □(B)
   coproj2(A::Ob, B::Ob) = □(A) ⊗ id(B)
 end
 
+function show_latex(io::IO, expr::HomExpr{:mmerge}; kw...)
+  Syntax.show_latex_script(io, expr, "\\nabla")
+end
+function show_latex(io::IO, expr::HomExpr{:create}; kw...)
+  Syntax.show_latex_script(io, expr, "\\square")
+end
+
 # Closed monoidal category
 ##########################
 
@@ -247,7 +258,7 @@ end
 
 A CCC is a cartesian category with internal homs (aka, exponential objects).
 
-FIXME: This theory should extend `ClosedMonoidalCategory`, but multiple
+FIXME: This theory should also extend `ClosedMonoidalCategory`, but multiple
 inheritance is not yet supported.
 """
 @signature CartesianCategory(Ob,Hom) => CartesianClosedCategory(Ob,Hom) begin
@@ -265,7 +276,7 @@ See also `FreeCartesianCategory`.
   otimes(f::Hom, g::Hom) = associate(new(f,g))
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 
-  pair(f::Hom, g::Hom) = Δ(dom(f)) → (f ⊗ g)
+  pair(f::Hom, g::Hom) = Δ(dom(f)) ⋅ (f ⊗ g)
   proj1(A::Ob, B::Ob) = id(A) ⊗ ◊(B)
   proj2(A::Ob, B::Ob) = ◊(A) ⊗ id(B)
 end
@@ -354,8 +365,8 @@ end
 Also known as a [symmetric monoidal dagger
 category](https://ncatlab.org/nlab/show/symmetric+monoidal+dagger-category).
 
-FIXME: This theory should extend both `DaggerCategory` and
-`SymmetricMonoidalCategory`, but multiple inheritance is not yet supported.
+FIXME: This theory should also extend `DaggerCategory`, but multiple inheritance
+is not yet supported.
 """
 @signature SymmetricMonoidalCategory(Ob,Hom) => DaggerSymmetricMonoidalCategory(Ob,Hom) begin
   dagger(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
@@ -380,8 +391,8 @@ in the official `LinearAlegbra` module. For the general relationship between
 mates and daggers, see Selinger's survey of graphical languages for monoidal
 categories.
 
-FIXME: This theory should extend both `DaggerCategory` and
-`CompactClosedCategory`, but multiple inheritance is not yet supported.
+FIXME: This theory should also extend `DaggerCategory`, but multiple inheritance
+is not yet supported.
 """
 @signature CompactClosedCategory(Ob,Hom) => DaggerCompactCategory(Ob,Hom) begin
   dagger(f::(A → B))::(B → A) ⊣ (A::Ob, B::Ob)
diff --git a/src/theories/MonoidalAdditive.jl b/src/theories/MonoidalAdditive.jl
new file mode 100644
index 000000000..36947803d
--- /dev/null
+++ b/src/theories/MonoidalAdditive.jl
@@ -0,0 +1,187 @@
+export MonoidalCategoryAdditive, SymmetricMonoidalCategoryAdditive,
+  FreeSymmetricMonoidalCategoryAdditive, oplus, ⊕, mzero, swap,
+  MonoidalCategoryWithCodiagonals, CocartesianCategory, FreeCocartesianCategory,
+  plus, zero, copair, coproj1, coproj2,
+  MonoidalCategoryWithBidiagonalsAdditive, SemiadditiveCategory,
+  mcopy, delete, pair, proj1, proj2, Δ, ◊, +
+
+import Base: collect, ndims, +, zero
+
+# Monoidal category
+###################
+
+""" Theory of *monoidal categories*, in additive notation
+
+Mathematically the same as [`MonoidalCategory`](@ref) but with different
+notation.
+"""
+@signature Category(Ob,Hom) => MonoidalCategoryAdditive(Ob,Hom) begin
+  oplus(A::Ob, B::Ob)::Ob
+  oplus(f::(A → B), g::(C → D))::((A ⊕ C) → (B ⊕ D)) <=
+    (A::Ob, B::Ob, C::Ob, D::Ob)
+  @op (⊕) := oplus
+  mzero()::Ob
+end
+
+# Convenience constructors
+oplus(xs::Vector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
+oplus(x, y, z, xs...) = oplus([x, y, z, xs...])
+
+# Overload `collect` and `ndims` as for multiplicative monoidal categories.
+collect(expr::ObExpr{:oplus}) = vcat(map(collect, args(expr))...)
+collect(expr::ObExpr{:mzero}) = roottypeof(expr)[]
+ndims(expr::ObExpr{:oplus}) = sum(map(ndims, args(expr)))
+ndims(expr::ObExpr{:mzero}) = 0
+
+function show_unicode(io::IO, expr::Union{ObExpr{:oplus},HomExpr{:oplus}}; kw...)
+  Syntax.show_unicode_infix(io, expr, "⊕"; kw...)
+end
+show_unicode(io::IO, expr::ObExpr{:mzero}; kw...) = print(io, "O")
+
+function show_latex(io::IO, expr::Union{ObExpr{:oplus},HomExpr{:oplus}}; kw...)
+  Syntax.show_latex_infix(io, expr, "\\oplus"; kw...)
+end
+show_latex(io::IO, expr::ObExpr{:mzero}; kw...) = print(io, "O")
+
+# Symmetric monoidal category
+#############################
+
+""" Theory of *symmetric monoidal categories*, in additive notation
+
+Mathematically the same as [`SymmetricMonoidalCategory`](@ref) but with
+different notation.
+"""
+@signature MonoidalCategoryAdditive(Ob,Hom) => SymmetricMonoidalCategoryAdditive(Ob,Hom) begin
+  swap(A::Ob, B::Ob)::Hom(oplus(A,B),oplus(B,A))
+end
+
+@syntax FreeSymmetricMonoidalCategoryAdditive(ObExpr,HomExpr) SymmetricMonoidalCategoryAdditive begin
+  oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
+  oplus(f::Hom, g::Hom) = associate(new(f,g))
+  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
+end
+
+function show_latex(io::IO, expr::HomExpr{:swap}; kw...)
+  Syntax.show_latex_script(io, expr, "\\sigma")
+end
+
+# Cocartesian category
+######################
+
+""" Theory of *monoidal categories with codiagonals*
+
+A monoidal category with codiagonals is a symmetric monoidal category equipped
+with coherent collections of merging and creating morphisms (monoids).
+Unlike in a cocartesian category, the naturality axioms need not be satisfied.
+
+For references, see [`MonoidalCategoryWithDiagonals`](@ref).
+"""
+@theory SymmetricMonoidalCategoryAdditive(Ob,Hom) => MonoidalCategoryWithCodiagonals(Ob,Hom) begin
+  plus(A::Ob)::((A ⊕ A) → A)
+  zero(A::Ob)::(mzero() → A)
+  
+  # Commutative monoid axioms.
+  plus(A) == swap(A,A) ⋅ plus(A) ⊣ (A::Ob)
+  (plus(A) ⊕ id(A)) ⋅ plus(A) == (id(A) ⊕ plus(A)) ⋅ plus(A) ⊣ (A::Ob)
+  (zero(A) ⊕ id(A)) ⋅ plus(A) == id(A) ⊣ (A::Ob)
+  (id(A) ⊕ zero(A)) ⋅ plus(A) == id(A) ⊣ (A::Ob)
+end
+
+""" Theory of *cocartesian (monoidal) categories*
+
+For the traditional axiomatization of coproducts, see
+[`CategoryWithCoproducts`](@ref).
+"""
+@theory MonoidalCategoryWithCodiagonals(Ob,Hom) => CocartesianCategory(Ob,Hom) begin
+  copair(f::(A → C), g::(B → C))::((A ⊕ B) → C) <= (A::Ob, B::Ob, C::Ob)
+  coproj1(A::Ob, B::Ob)::(A → (A ⊕ B))
+  coproj2(A::Ob, B::Ob)::(B → (A ⊕ B))
+  
+  copair(f,g) == (f⊕g)⋅plus(C) ⊣ (A::Ob, B::Ob, C::Ob, f::(A → C), g::(B → C))
+  coproj1(A,B) == id(A)⊕zero(B) ⊣ (A::Ob, B::Ob)
+  coproj2(A,B) == zero(A)⊕id(B) ⊣ (A::Ob, B::Ob)
+  
+  # Naturality axioms.
+  plus(A)⋅f == (f⊕f)⋅plus(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  zero(A)⋅f == zero(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+end
+
+""" Syntax for a free cocartesian category.
+
+In this syntax, the copairing and inclusion operations are defined using merging
+and creation, and do not have their own syntactic elements. This convention
+could be dropped or reversed.
+"""
+@syntax FreeCocartesianCategory(ObExpr,HomExpr) CocartesianCategory begin
+  oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
+  oplus(f::Hom, g::Hom) = associate(new(f,g))
+  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
+
+  copair(f::Hom, g::Hom) = compose(oplus(f,g), plus(codom(f)))
+  coproj1(A::Ob, B::Ob) = oplus(id(A), zero(B))
+  coproj2(A::Ob, B::Ob) = oplus(zero(A), id(B))
+end
+
+function show_latex(io::IO, expr::HomExpr{:plus}; kw...)
+  if length(args(expr)) >= 2
+    Syntax.show_latex_infix(io, expr, "+"; kw...)
+  else
+    Syntax.show_latex_script(io, expr, "\\nabla")
+  end
+end
+
+function show_latex(io::IO, expr::HomExpr{:zero}; kw...)
+  Syntax.show_latex_script(io, expr, "0")
+end
+
+# Biproduct category
+####################
+
+""" Theory of *monoidal categories with bidiagonals*, in additive notation
+
+Mathematically the same as [`MonoidalCategoryWithBidiagonals`](@ref) but written
+additively, instead of multiplicatively.
+"""
+@theory MonoidalCategoryWithCodiagonals(Ob,Hom) =>
+    MonoidalCategoryWithBidiagonalsAdditive(Ob,Hom) begin
+  mcopy(A::Ob)::(A → (A ⊕ A))
+  @op (Δ) := mcopy
+  delete(A::Ob)::(A → mzero())
+  @op (◊) := delete
+  
+  # Commutative comonoid axioms.
+  Δ(A) == Δ(A) ⋅ swap(A,A) ⊣ (A::Ob)
+  Δ(A) ⋅ (Δ(A) ⊕ id(A)) == Δ(A) ⋅ (id(A) ⊕ Δ(A)) ⊣ (A::Ob)
+  Δ(A) ⋅ (◊(A) ⊕ id(A)) == id(A) ⊣ (A::Ob)
+  Δ(A) ⋅ (id(A) ⊕ ◊(A)) == id(A) ⊣ (A::Ob)
+end
+
+""" Theory of *semiadditive categories*
+
+Mathematically the same as [`BiproductCategory`](@ref) but written additively,
+instead of multiplicatively.
+"""
+@theory MonoidalCategoryWithBidiagonalsAdditive(Ob,Hom) =>
+    SemiadditiveCategory(Ob,Hom) begin
+  pair(f::(A → B), g::(A → C))::(A → (B ⊕ C)) ⊣ (A::Ob, B::Ob, C::Ob)
+  copair(f::(A → C), g::(B → C))::((A ⊕ B) → C) ⊣ (A::Ob, B::Ob, C::Ob)
+  proj1(A::Ob, B::Ob)::((A ⊕ B) → A)
+  proj2(A::Ob, B::Ob)::((A ⊕ B) → B)
+  coproj1(A::Ob, B::Ob)::(A → (A ⊕ B))
+  coproj2(A::Ob, B::Ob)::(B → (A ⊕ B))
+  
+  plus(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
+  @op (+) := plus
+  
+  # Naturality axioms.
+  f⋅Δ(B) == Δ(A)⋅(f⊕f) ⊣ (A::Ob, B::Ob, f::(A → B))
+  f⋅◊(B) == ◊(A) ⊣ (A::Ob, B::Ob, f::(A → B))
+  plus(A)⋅f == (f⊕f)⋅plus(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  zero(A)⋅f == zero(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  
+  # Bimonoid axioms. (These follow from naturality + coherence axioms.)
+  plus(A)⋅Δ(A) == (Δ(A)⊕Δ(A)) ⋅ (id(A)⊕swap(A,A)⊕id(A)) ⋅ (plus(A)⊕plus(A)) ⊣ (A::Ob)
+  plus(A)⋅◊(A) == ◊(A) ⊕ ◊(A) ⊣ (A::Ob)
+  zero(A)⋅Δ(A) == zero(A) ⊕ zero(A) ⊣ (A::Ob)
+  zero(A)⋅◊(A) == id(mzero()) ⊣ (A::Ob)
+end
diff --git a/src/theories/MonoidalMultiple.jl b/src/theories/MonoidalMultiple.jl
new file mode 100644
index 000000000..1e7ad9d37
--- /dev/null
+++ b/src/theories/MonoidalMultiple.jl
@@ -0,0 +1,108 @@
+export RigCategory, SymmetricRigCategory, DistributiveMonoidalCategory,
+  DistributiveSemiadditiveCategory, DistributiveCategory
+
+# Distributive categories
+#########################
+
+""" Theory of a *rig category*, also known as a *bimonoidal category*
+
+[Rig categories](https://ncatlab.org/nlab/show/rig+category) are the most
+general in the hierarchy of [distributive monoidal
+structures](https://ncatlab.org/nlab/show/distributivity+for+monoidal+structures).
+
+TODO: Do we also want the distributivty and absorption isomorphisms? Usually we
+ignore coherence isomorphisms such as associators and unitors.
+
+FIXME: This theory should also inherit `MonoidalCategory`, but multiple
+inheritance is not supported.
+"""
+@signature SymmetricMonoidalCategoryAdditive(Ob,Hom) => RigCategory(Ob,Hom) begin
+  otimes(A::Ob, B::Ob)::Ob
+  otimes(f::(A → B), g::(C → D))::((A ⊗ C) → (B ⊗ D)) ⊣
+    (A::Ob, B::Ob, C::Ob, D::Ob)
+  @op (⊗) := otimes
+  munit()::Ob
+end
+
+""" Theory of a *symmetric rig category*
+
+FIXME: Should also inherit `SymmetricMonoidalCategory`.
+"""
+@signature RigCategory(Ob,Hom) => SymmetricRigCategory(Ob,Hom) begin
+  braid(A::Ob, B::Ob)::((A ⊗ B) → (B ⊗ A))
+  @op (σ) := braid
+end
+
+""" Theory of a *distributive (symmetric) monoidal category*
+
+Reference: Jay, 1992, LFCS tech report LFCS-92-205, "Tail recursion through
+universal invariants", Section 3.2
+
+FIXME: Should also inherit `CocartesianCategory`.
+"""
+@theory SymmetricRigCategory(Ob,Hom) => DistributiveMonoidalCategory(Ob,Hom) begin
+  plus(A::Ob)::((A ⊕ A) → A)
+  zero(A::Ob)::(mzero() → A)
+  
+  copair(f::(A → C), g::(B → C))::((A ⊕ B) → C) <= (A::Ob, B::Ob, C::Ob)
+  coproj1(A::Ob, B::Ob)::(A → (A ⊕ B))
+  coproj2(A::Ob, B::Ob)::(B → (A ⊕ B))
+  
+  copair(f,g) == (f⊕g)⋅plus(C) ⊣ (A::Ob, B::Ob, C::Ob, f::(A → C), g::(B → C))
+  coproj1(A,B) == id(A)⊕zero(B) ⊣ (A::Ob, B::Ob)
+  coproj2(A,B) == zero(A)⊕id(B) ⊣ (A::Ob, B::Ob)
+  
+  # Naturality axioms.
+  plus(A)⋅f == (f⊕f)⋅plus(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+  zero(A)⋅f == zero(B) ⊣ (A::Ob, B::Ob, f::(A → B))
+end
+
+""" Theory of a *distributive semiadditive category*
+
+This terminology is not standard but the concept occurs frequently. A
+distributive semiadditive category is a semiadditive category (or biproduct)
+category, written additively, with a tensor product that distributes over the
+biproduct.
+
+FIXME: Should also inherit `SemiadditiveCategory`
+"""
+@theory DistributiveMonoidalCategory(Ob,Hom) => DistributiveSemiadditiveCategory(Ob,Hom) begin
+  mcopy(A::Ob)::(A → (A ⊕ A))
+  @op (Δ) := mcopy
+  delete(A::Ob)::(A → mzero())
+  @op (◊) := delete
+
+  pair(f::(A → B), g::(A → C))::(A → (B ⊕ C)) ⊣ (A::Ob, B::Ob, C::Ob)
+  proj1(A::Ob, B::Ob)::((A ⊕ B) → A)
+  proj2(A::Ob, B::Ob)::((A ⊕ B) → B)
+  
+  # Naturality axioms.
+  f⋅Δ(B) == Δ(A)⋅(f⊕f) ⊣ (A::Ob, B::Ob, f::(A → B))
+  f⋅◊(B) == ◊(A) ⊣ (A::Ob, B::Ob, f::(A → B))
+end
+
+""" Theory of a *distributive category*
+
+A distributive category is a distributive monoidal category whose tensor product
+is the cartesian product, see [`DistributiveMonoidalCategory`](@ref).
+
+FIXME: Should also inherit `CartesianCategory`.
+"""
+@theory DistributiveMonoidalCategory(Ob,Hom) => DistributiveCategory(Ob,Hom) begin
+  mcopy(A::Ob)::(A → (A ⊗ A))
+  @op (Δ) := mcopy
+  delete(A::Ob)::(A → munit())
+  @op (◊) := delete
+  
+  pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)
+  proj1(A::Ob, B::Ob)::((A ⊗ B) → A)
+  proj2(A::Ob, B::Ob)::((A ⊗ B) → B)
+
+  pair(f,g) == Δ(C)⋅(f⊗g) ⊣ (A::Ob, B::Ob, C::Ob, f::(C → A), g::(C → B))
+  proj1(A,B) == id(A)⊗◊(B) ⊣ (A::Ob, B::Ob)
+  proj2(A,B) == ◊(A)⊗id(B) ⊣ (A::Ob, B::Ob)
+  
+  # Naturality axioms.
+  f⋅Δ(B) == Δ(A)⋅(f⊗f) ⊣ (A::Ob, B::Ob, f::(A → B))
+  f⋅◊(B) == ◊(A) ⊣ (A::Ob, B::Ob, f::(A → B))
+end
diff --git a/src/theories/Relations.jl b/src/theories/Relations.jl
index 4c750fbfa..047df4c9d 100644
--- a/src/theories/Relations.jl
+++ b/src/theories/Relations.jl
@@ -9,7 +9,7 @@ import Base: join, zero
 
 """ Theory of *bicategories of relations*
 
-TODO: The 2-morphisms are missing. I haven't decided how to handle them yet.
+TODO: The 2-morphisms are missing.
 
 References:
 
@@ -18,70 +18,67 @@ References:
   http://rfcwalters.blogspot.com/2009/10/categorical-algebras-of-relations.html
 """
 @signature MonoidalCategoryWithBidiagonals(Ob,Hom) => BicategoryRelations(Ob,Hom) begin
-  # Dagger category.
-  dagger(f::(A → B))::(B → A) ⊣ (A::Ob,B::Ob)
-
-  # Self-dual compact closed category.
+  # Self-dual dagger compact category.
+  dagger(R::(A → B))::(B → A) ⊣ (A::Ob,B::Ob)
   dunit(A::Ob)::(munit() → (A ⊗ A))
   dcounit(A::Ob)::((A ⊗ A) → munit())
 
   # Logical operations.
-  meet(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
+  meet(R::(A → B), S::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
   top(A::Ob, B::Ob)::(A → B)
 end
 
 @syntax FreeBicategoryRelations(ObExpr,HomExpr) BicategoryRelations begin
   otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
-  otimes(f::Hom, g::Hom) = associate(new(f,g))
-  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(new(f))),
+  otimes(R::Hom, S::Hom) = associate(new(R,S))
+  compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
+  dagger(R::Hom) = distribute_unary(distribute_dagger(involute(new(R))),
                                     dagger, otimes)
-  meet(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f)))
+  meet(R::Hom, S::Hom) = compose(mcopy(dom(R)), otimes(R,S), mmerge(codom(R)))
   top(A::Ob, B::Ob) = compose(delete(A), create(B))
 end
 
 """ Theory of *abelian bicategories of relations*
 
-Unlike Carboni & Walters, we use additive notation and nomenclature.
+Unlike [`BicategoryRelations`](@ref), this theory uses additive notation.
 
 References:
 
 - Carboni & Walters, 1987, "Cartesian bicategories I", Sec. 5
 - Baez & Erbele, 2015, "Categories in control"
 """
-@signature BicategoryRelations(Ob,Hom) => AbelianBicategoryRelations(Ob,Hom) begin
-  # Second diagonal and codiagonal.
-  plus(A::Ob)::((A ⊗ A) → A)
-  zero(A::Ob)::(munit() → A)
-  coplus(A::Ob)::(A → (A ⊗ A))
-  cozero(A::Ob)::(A → munit())
+@signature MonoidalCategoryWithBidiagonalsAdditive(Ob,Hom) =>
+    AbelianBicategoryRelations(Ob,Hom) begin
+  # Self-dual dagger compact category.
+  dagger(R::(A → B))::(B → A) ⊣ (A::Ob,B::Ob)
+  dunit(A::Ob)::(mzero() → (A ⊕ A))
+  dcounit(A::Ob)::((A ⊕ A) → mzero())
+
+  # Merging and creating (right adjoints of copying and deleting maps).
+  mmerge(A::Ob)::((A ⊕ A) → A)
+  @op (∇) := mmerge
+  create(A::Ob)::(mzero() → A)
+  @op (□) := create
+
+  # Co-addition and co-zero (right adjoints of addition and zero maps).
+  coplus(A::Ob)::(A → (A ⊕ A))
+  cozero(A::Ob)::(A → mzero())
 
   # Logical operations.
-  join(f::(A → B), g::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
+  meet(R::(A → B), S::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
+  top(A::Ob, B::Ob)::(A → B)
+  join(R::(A → B), S::(A → B))::(A → B) ⊣ (A::Ob, B::Ob)
   bottom(A::Ob, B::Ob)::(A → B)
 end
 
 @syntax FreeAbelianBicategoryRelations(ObExpr,HomExpr) AbelianBicategoryRelations begin
-  otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
-  otimes(f::Hom, g::Hom) = associate(new(f,g))
-  compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
-  dagger(f::Hom) = distribute_unary(distribute_dagger(involute(new(f))),
-                                    dagger, otimes)
-  meet(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f)))
-  join(f::Hom, g::Hom) = compose(coplus(dom(f)), otimes(f,g), plus(codom(f)))
+  oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
+  oplus(R::Hom, S::Hom) = associate(new(R,S))
+  compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
+  dagger(R::Hom) = distribute_unary(distribute_dagger(involute(new(R))),
+                                    dagger, oplus)
+  meet(R::Hom, S::Hom) = compose(mcopy(dom(R)), oplus(R,S), mmerge(codom(R)))
+  join(R::Hom, S::Hom) = compose(coplus(dom(R)), oplus(R,S), plus(codom(R)))
   top(A::Ob, B::Ob) = compose(delete(A), create(B))
   bottom(A::Ob, B::Ob) = compose(cozero(A), zero(B))
 end
-
-function show_latex(io::IO, expr::HomExpr{:plus}; kw...)
-  Syntax.show_latex_script(io, expr, "\\blacktriangledown")
-end
-function show_latex(io::IO, expr::HomExpr{:coplus}; kw...)
-  Syntax.show_latex_script(io, expr, "\\blacktriangle")
-end
-function show_latex(io::IO, expr::HomExpr{:zero}; kw...)
-  Syntax.show_latex_script(io, expr, "\\blacksquare")
-end
-function show_latex(io::IO, expr::HomExpr{:cozero}; kw...)
-  Syntax.show_latex_script(io, expr, "\\blacklozenge")
-end
diff --git a/src/theories/Theories.jl b/src/theories/Theories.jl
index d1b52f468..12e7b1d75 100644
--- a/src/theories/Theories.jl
+++ b/src/theories/Theories.jl
@@ -30,7 +30,8 @@ end
 include("Category.jl")
 include("Limits.jl")
 include("Monoidal.jl")
-include("AdditiveMonoidal.jl")
+include("MonoidalAdditive.jl")
+include("MonoidalMultiple.jl")
 include("Preorders.jl")
 include("Relations.jl")
 
diff --git a/src/wiring_diagrams/Algebraic.jl b/src/wiring_diagrams/Algebraic.jl
index beb65767a..85839fe06 100644
--- a/src/wiring_diagrams/Algebraic.jl
+++ b/src/wiring_diagrams/Algebraic.jl
@@ -6,8 +6,8 @@ types and functions to represent diagonals, codiagonals, duals, caps, cups,
 daggers, and other structures in wiring diagrams.
 """
 module AlgebraicWiringDiagrams
-export Ports, Junction, PortOp, BoxOp,
-  functor, dom, codom, id, compose, ⋅, ∘, otimes, ⊗, munit, braid, permute,
+export Ports, Junction, PortOp, BoxOp, functor, dom, codom, id, compose, ⋅, ∘,
+  otimes, ⊗, munit, braid, σ, oplus, ⊕, mzero, swap, permute,
   mcopy, delete, Δ, ◊, mmerge, create, ∇, □, dual, dunit, dcounit, mate, dagger,
   plus, zero, coplus, cozero, meet, join, top, bottom, trace, ocompose,
   implicit_mcopy, implicit_mmerge, junctioned_mcopy, junctioned_mmerge,
@@ -18,7 +18,8 @@ using AutoHashEquals
 using LightGraphs
 
 using ...GAT, ...Theories
-import ...Theories: dom, codom, id, compose, ⋅, ∘, otimes, ⊗, munit, braid,
+import ...Theories: dom, codom, id, compose, ⋅, ∘,
+  otimes, ⊗, munit, braid, σ, oplus, ⊕, mzero, swap,
   mcopy, delete, Δ, ◊, mmerge, create, ∇, □, dual, dunit, dcounit, mate, dagger,
   plus, zero, coplus, cozero, meet, join, top, bottom, trace
 import ...Syntax: functor, head
@@ -336,6 +337,12 @@ top(A::Ports{BiRel}, B::Ports{BiRel}) = compose(delete(A), create(B))
 
 const AbBiRel = AbelianBicategoryRelations
 
+# Additive notation. FIXME: Use @instance.
+oplus(f::WiringDiagram{AbBiRel}, g::WiringDiagram{AbBiRel}) = otimes(f,g)
+⊕(f::WiringDiagram{AbBiRel}, g::WiringDiagram{AbBiRel}) = oplus(f,g)
+mzero(::Type{T}) where T <: Ports{AbBiRel} = munit(T)
+swap(A::Ports{AbBiRel}, B::Ports{AbBiRel}) = braid(A, B)
+
 mcopy(A::Ports{AbBiRel}, n::Int) = junctioned_mcopy(A, n; op=:times)
 mmerge(A::Ports{AbBiRel}, n::Int) = junctioned_mmerge(A, n; op=:times)
 
@@ -349,9 +356,9 @@ dagger(f::WiringDiagram{AbBiRel}) =
   functor(f, identity, dagger, contravariant=true)
 
 meet(f::WiringDiagram{AbBiRel}, g::WiringDiagram{AbBiRel}) =
-  compose(mcopy(dom(f)), otimes(f,g), mmerge(codom(f)))
+  compose(mcopy(dom(f)), oplus(f,g), mmerge(codom(f)))
 join(f::WiringDiagram{AbBiRel}, g::WiringDiagram{AbBiRel}) =
-  compose(coplus(dom(f)), otimes(f,g), plus(codom(f)))
+  compose(coplus(dom(f)), oplus(f,g), plus(codom(f)))
 top(A::Ports{AbBiRel}, B::Ports{AbBiRel}) = compose(delete(A), create(B))
 bottom(A::Ports{AbBiRel}, B::Ports{AbBiRel}) = compose(cozero(A), zero(B))
 
diff --git a/test/categorical_algebra/CategoricalAlgebra.jl b/test/categorical_algebra/CategoricalAlgebra.jl
index 2fd30eb20..238952afd 100644
--- a/test/categorical_algebra/CategoricalAlgebra.jl
+++ b/test/categorical_algebra/CategoricalAlgebra.jl
@@ -6,6 +6,10 @@ using Test
   include("ShapeDiagrams.jl")
 end
 
+@testset "Matrices" begin
+  include("Matrices.jl")
+end
+
 @testset "FinSets" begin
   include("FinSets.jl")
 end
diff --git a/test/categorical_algebra/Matrices.jl b/test/categorical_algebra/Matrices.jl
new file mode 100644
index 000000000..3dcc041e6
--- /dev/null
+++ b/test/categorical_algebra/Matrices.jl
@@ -0,0 +1,42 @@
+module TestMatrices
+using Test
+using SparseArrays
+
+using Catlab.CategoricalAlgebra.Matrices
+
+# Dense matrices
+################
+
+const IntMat = Matrix{Int}
+
+A, B, C = [1 2 3; 4 5 6], [1 -1; -1 2], [0 1; 1 0]
+@test dom(A) == MatrixDom{IntMat}(3)
+@test codom(A) == MatrixDom{IntMat}(2)
+@test A⋅B == B*A
+@test id(dom(A))⋅A == A
+@test A⋅id(codom(A)) == A
+
+@test A⊕(B⊕C) == (A⊕B)⊕C
+@test swap(dom(A),dom(B))⋅(B⊕A)⋅swap(codom(B),codom(A)) == A⊕B
+@test pair(B,C) == mcopy(dom(B))⋅(B⊕C)
+@test copair(A,B) == (A⊕B)⋅plus(codom(A))
+
+@test A⊗(B⊗C) == (A⊗B)⊗C
+@test braid(dom(A),dom(B))⋅(B⊗A)⋅braid(codom(B),codom(A)) == A⊗B
+
+# Sparse matrices
+#################
+
+const SparseIntMat = SparseMatrixCSC{Int,Int}
+
+A, B, C = sparse(A), sparse(B), sparse(C)
+@test dom(A) == MatrixDom{SparseIntMat}(3)
+@test codom(A) == MatrixDom{SparseIntMat}(2)
+@test A⋅B isa SparseIntMat
+@test A⊕B isa SparseIntMat
+@test A⊗B isa SparseIntMat
+@test A⋅B == B*A
+@test id(dom(A))⋅A == A
+@test A⋅id(codom(A)) == A
+
+end
diff --git a/test/linear_algebra/GLA.jl b/test/linear_algebra/GLA.jl
index 435263972..66acc94ab 100644
--- a/test/linear_algebra/GLA.jl
+++ b/test/linear_algebra/GLA.jl
@@ -37,7 +37,7 @@ x, y = [2, 1], [7, 3, 5]
 @test (f⋅f)*x == f*(f*x)
 @test (f⋅h)*x == h*(f*x)
 @test (f⊕g)*[x;y] == [f*x; g*y]
-@test braid(dom(f),dom(g)) * [x;y] == [y;x]
+@test swap(dom(f),dom(g)) * [x;y] == [y;x]
 
 @test mcopy(dom(f))*x == [x;x]
 @test delete(dom(f))*x == []
@@ -139,7 +139,7 @@ x, y = [2, 1], [7, 3, 5]
 @test (f⋅f)*x == f*(f*x)
 @test (f⋅h)*x == h*(f*x)
 @test (f⊕g)*[x;y] == [f*x; g*y]
-@test braid(dom(f),dom(g)) * [x;y] == [y;x]
+@test swap(dom(f),dom(g)) * [x;y] == [y;x]
 
 @test mcopy(dom(f))*x == [x;x]
 @test delete(dom(f))*x == []
diff --git a/test/theories/Monoidal.jl b/test/theories/Monoidal.jl
index 2ceebae52..645270d34 100644
--- a/test/theories/Monoidal.jl
+++ b/test/theories/Monoidal.jl
@@ -89,6 +89,15 @@ f, g = Hom(:f, A, B), Hom(:g, B, A)
 @test latex(mcopy(A)) == "\\Delta_{A}"
 @test latex(delete(A)) == "\\lozenge_{A}"
 
+# Biproduct category
+####################
+
+A, B = Ob(FreeBiproductCategory, :A, :B)
+
+# LaTeX notation
+@test latex(mmerge(A)) == "\\nabla_{A}"
+@test latex(create(A)) == "\\square_{A}"
+
 # Cartesian closed category
 ###########################
 
diff --git a/test/theories/AdditiveMonoidal.jl b/test/theories/MonoidalAdditive.jl
similarity index 74%
rename from test/theories/AdditiveMonoidal.jl
rename to test/theories/MonoidalAdditive.jl
index 65b2a3282..80b0f0da1 100644
--- a/test/theories/AdditiveMonoidal.jl
+++ b/test/theories/MonoidalAdditive.jl
@@ -3,17 +3,17 @@ using Test
 # Symmetric monoidal category
 #############################
 
-A, B = Ob(FreeAdditiveSymmetricMonoidalCategory, :A, :B)
+A, B = Ob(FreeSymmetricMonoidalCategoryAdditive, :A, :B)
 f, g = Hom(:f, A, B), Hom(:g, B, A)
 
 # Domains and codomains
 @test dom(oplus(f,g)) == oplus(dom(f),dom(g))
 @test codom(oplus(f,g)) == oplus(codom(f),codom(g))
-@test dom(braid(A,B)) == oplus(A,B)
-@test codom(braid(A,B)) == oplus(B,A)
+@test dom(swap(A,B)) == oplus(A,B)
+@test codom(swap(A,B)) == oplus(B,A)
 
 # Associativity and unit
-O = mzero(FreeAdditiveSymmetricMonoidalCategory.Ob)
+O = mzero(FreeSymmetricMonoidalCategoryAdditive.Ob)
 @test oplus(A,O) == A
 @test oplus(O,A) == A
 @test oplus(oplus(A,B),A) == oplus(A,oplus(B,A))
@@ -24,7 +24,7 @@ O = mzero(FreeAdditiveSymmetricMonoidalCategory.Ob)
 @test oplus([A,B,A]) == oplus(oplus(A,B),A)
 @test oplus(f,f,f) == oplus(oplus(f,f),f)
 @test oplus([f,f,f]) == oplus(oplus(f,f),f)
-@test oplus(FreeAdditiveSymmetricMonoidalCategory.Ob[]) == O
+@test oplus(FreeSymmetricMonoidalCategoryAdditive.Ob[]) == O
 @test_throws MethodError oplus([])
 @test A⊕B == oplus(A,B)
 @test f⊕g == oplus(f,g)
@@ -34,7 +34,7 @@ O = mzero(FreeAdditiveSymmetricMonoidalCategory.Ob)
 @test collect(A) == [A]
 @test collect(oplus(A,B)) == [A,B]
 @test collect(O) == []
-@test typeof(collect(O)) == Vector{FreeAdditiveSymmetricMonoidalCategory.Ob}
+@test typeof(collect(O)) == Vector{FreeSymmetricMonoidalCategoryAdditive.Ob}
 @test ndims(A) == 1
 @test ndims(oplus(A,B)) == 2
 @test ndims(O) == 0
@@ -64,8 +64,7 @@ O = mzero(FreeAdditiveSymmetricMonoidalCategory.Ob)
   "\\left(f \\oplus f\\right) \\cdot \\left(g \\oplus g\\right)"
 @test latex(oplus(compose(f,g),compose(g,f))) == 
   "\\left(f \\cdot g\\right) \\oplus \\left(g \\cdot f\\right)"
-@test latex(braid(A,B)) == "\\sigma_{A,B}"
-
+@test latex(swap(A,B)) == "\\sigma_{A,B}"
 
 # Cocartesian category
 ######################
@@ -74,16 +73,16 @@ A, B = Ob(FreeCocartesianCategory, :A, :B)
 f, g = Hom(:f, A, B), Hom(:g, B, A)
 
 # Domains and codomains
-@test dom(mmerge(A)) == oplus(A,A)
-@test codom(mmerge(A)) == A
-@test dom(create(A)) == O
-@test codom(create(A)) == A
+@test dom(plus(A)) == oplus(A,A)
+@test codom(plus(A)) == A
+@test dom(zero(A)) == O
+@test codom(zero(A)) == A
 
 # Derived syntax
-@test copair(f,f) == compose(oplus(f,f), mmerge(B))
-@test coproj1(A,B) == oplus(id(A), create(B))
-@test coproj2(A,B) == oplus(create(A), id(B))
+@test copair(f,f) == compose(oplus(f,f), plus(B))
+@test coproj1(A,B) == oplus(id(A), zero(B))
+@test coproj2(A,B) == oplus(zero(A), id(B))
 
 # LaTeX notation
-@test latex(mmerge(A)) == "\\nabla_{A}"
-@test latex(create(A)) == "\\square_{A}"
+@test latex(plus(A)) == "\\nabla_{A}"
+@test latex(zero(A)) == "0_{A}"
diff --git a/test/theories/Theories.jl b/test/theories/Theories.jl
index dc3522312..653a68700 100644
--- a/test/theories/Theories.jl
+++ b/test/theories/Theories.jl
@@ -14,7 +14,7 @@ end
 
 @testset "MonoidalCategories" begin
   include("Monoidal.jl")
-  include("AdditiveMonoidal.jl")
+  include("MonoidalAdditive.jl")
 end
 
 @testset "Preorders" begin