From f79b42171cfcbed908abb75400f8f9f29bfe12c3 Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Fri, 9 Jul 2021 20:20:16 -0700
Subject: [PATCH 1/7] ENH: Cartesian monoidal structure for Set and FinSet.

---
 src/categorical_algebra/Sets.jl  | 35 +++++++++++++++++++++++++++-----
 test/categorical_algebra/Sets.jl |  7 +++++++
 2 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/src/categorical_algebra/Sets.jl b/src/categorical_algebra/Sets.jl
index f10d6c072..874f99f06 100644
--- a/src/categorical_algebra/Sets.jl
+++ b/src/categorical_algebra/Sets.jl
@@ -5,10 +5,12 @@ export SetOb, TypeSet, PredicatedSet, SetFunction, ConstantFunction
 
 using AutoHashEquals
 using FunctionWrappers: FunctionWrapper
+using StaticArrays: SVector
 
 using ...GAT, ..FreeDiagrams, ..Limits
-using ...Theories: Category
-import ...Theories: dom, codom, id, compose, ⋅, ∘
+using ...Theories: CartesianCategory
+import ...Theories: dom, codom, id, compose, ⋅, ∘, otimes, ⊗, munit, braid, σ,
+  mcopy, delete, pair, proj1, proj2, Δ, ◊
 import ..Limits: limit, universal
 
 # Data types
@@ -140,12 +142,14 @@ function (f::PredicatedFunction{T,T′})(x::T)::T′ where {T,T′}
   y
 end
 
-# Category of sets
-##################
+# Cartesian category of sets
+############################
 
 """ Category of sets and functions.
 """
-@instance Category{SetOb, SetFunction} begin
+@instance CartesianCategory{SetOb, SetFunction} begin
+  @import munit, delete, pair
+
   dom(f::SetFunction) = f.dom
   codom(f::SetFunction) = f.codom
 
@@ -156,6 +160,18 @@ end
       error("Domain mismatch in composition: $(codom(f)) != $(dom(g))")
     compose_maybe_id(f, g)
   end
+
+  otimes(A::SetOb, B::SetOb) = otimes(SVector(A, B))
+  otimes(f::SetFunction, g::SetFunction) = otimes(SVector(f, g))
+
+  function braid(A::SetOb, B::SetOb)
+    AB, BA = product(A, B), product(B, A)
+    pair(BA, proj2(AB), proj1(AB))
+  end
+
+  mcopy(A::SetOb) = pair(id(A),id(A))
+  proj1(A::SetOb, B::SetOb) = proj1(product(A, B))
+  proj2(A::SetOb, B::SetOb) = proj2(product(A, B))
 end
 
 @inline compose_maybe_id(f::SetFunction, g::SetFunction) = compose_impl(f, g)
@@ -173,6 +189,15 @@ compose_impl(c::ConstantFunction, f::SetFunction) =
 compose_impl(c::ConstantFunction, d::ConstantFunction) =
   ConstantFunction(d.value, dom(c), codom(d))
 
+otimes(As::AbstractVector{<:SetOb}) = ob(product(As))
+
+function otimes(fs::AbstractVector{<:SetFunction})
+  Π, Π′ = product(map(dom, fs)), product(map(codom, fs))
+  pair(Π′, map(compose, legs(Π), fs))
+end
+
+munit(::Type{S}) where S <: SetOb = ob(terminal(S))
+
 # Limits
 ########
 
diff --git a/test/categorical_algebra/Sets.jl b/test/categorical_algebra/Sets.jl
index 8e731b920..da5cde97b 100644
--- a/test/categorical_algebra/Sets.jl
+++ b/test/categorical_algebra/Sets.jl
@@ -63,17 +63,24 @@ plus_two_to_odd = compose(plus_one_to_odd, plus_one_to_even)
 # Terminal object.
 @test ob(terminal(TypeSet)) == TypeSet(Nothing)
 @test delete(terminal(TypeSet), TypeSet(Int))(3) == nothing
+@test munit(TypeSet) == TypeSet(Nothing)
 
 # Binary product.
 lim = product(TypeSet(Int), TypeSet(String))
 @test ob(lim) == TypeSet(Tuple{Int,String})
 π1, π2 = lim
 @test (π1((1,"foo")), π2((1,"foo"))) == (1,"foo")
+@test TypeSet(Int) ⊗ TypeSet(String) == TypeSet(Tuple{Int,String})
+@test σ(TypeSet(Int), TypeSet(String))((1,"foo")) == ("foo",1)
 
 f = SetFunction(length, TypeSet(Vector{String}), TypeSet(Int))
 g = SetFunction(v -> sprint(join, v), TypeSet(Vector{String}), TypeSet(String))
 @test pair(lim, f, g)(["foo", "bar", "baz"]) == (3, "foobarbaz")
 
+@test (f⊗g)((["foo"], ["bar", "baz"])) == (1, "barbaz")
+@test Δ(TypeSet(Int))(2) == (2,2)
+@test ◊(TypeSet(Int))(1) == nothing
+
 # N-ary product.
 lim = product(fill(TypeSet(Int), 3))
 @test ob(lim) == TypeSet(Tuple{Int,Int,Int})

From 56af9fc82f0d56143bb9a4448d55a7125674df91 Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Fri, 9 Jul 2021 22:33:05 -0700
Subject: [PATCH 2/7] BUG: Overly strict types for vector-based constructors in
 Theories.

---
 src/theories/Category.jl         | 2 +-
 src/theories/HigherCategory.jl   | 4 ++--
 src/theories/Monoidal.jl         | 3 ++-
 src/theories/MonoidalAdditive.jl | 2 +-
 4 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/theories/Category.jl b/src/theories/Category.jl
index c0868b86c..e379df11d 100644
--- a/src/theories/Category.jl
+++ b/src/theories/Category.jl
@@ -44,7 +44,7 @@ We use symbol ⋅ (\\cdot) for diagrammatic composition: f⋅g = compose(f,g).
 end
 
 # Convenience constructors
-compose(fs::Vector) = foldl(compose, fs)
+compose(fs::AbstractVector) = foldl(compose, fs)
 compose(f, g, h, fs...) = compose([f, g, h, fs...])
 
 @syntax FreeCategory{ObExpr,HomExpr} Category begin
diff --git a/src/theories/HigherCategory.jl b/src/theories/HigherCategory.jl
index ac071ef4b..825414183 100644
--- a/src/theories/HigherCategory.jl
+++ b/src/theories/HigherCategory.jl
@@ -32,7 +32,7 @@ abstract type HomHExpr{T} <: CategoryExpr{T} end
 end
 
 # Convenience constructors
-composeH(αs::Vector) = foldl(composeH, αs)
+composeH(αs::AbstractVector) = foldl(composeH, αs)
 composeH(α, β, γ, αs...) = composeH([α, β, γ, αs...])
 
 """ Syntax for a 2-category.
@@ -119,7 +119,7 @@ end
 end
 
 # Convenience constructors
-composeV(αs::Vector) = foldl(composeV, αs)
+composeV(αs::AbstractVector) = foldl(composeV, αs)
 composeV(α, β, γ, αs...) = composeV([α, β, γ, αs...])
 
 """ Syntax for a double category.
diff --git a/src/theories/Monoidal.jl b/src/theories/Monoidal.jl
index 50ba76bca..a297f1465 100644
--- a/src/theories/Monoidal.jl
+++ b/src/theories/Monoidal.jl
@@ -52,7 +52,8 @@ theory for weak monoidal categories later.
 end
 
 # Convenience constructors
-otimes(xs::Vector{T}) where T = isempty(xs) ? munit(T) : foldl(otimes, xs)
+otimes(xs::AbstractVector{T}) where T =
+  isempty(xs) ? munit(T) : foldl(otimes, xs)
 otimes(x, y, z, xs...) = otimes([x, y, z, xs...])
 
 """ Collect generators of object in monoidal category as a vector.
diff --git a/src/theories/MonoidalAdditive.jl b/src/theories/MonoidalAdditive.jl
index 0e419fad2..7e1423779 100644
--- a/src/theories/MonoidalAdditive.jl
+++ b/src/theories/MonoidalAdditive.jl
@@ -25,7 +25,7 @@ notation.
 end
 
 # Convenience constructors
-oplus(xs::Vector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
+oplus(xs::AbstractVector{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.

From aa9f676f782a92235398f3fece5ab49f7c444933 Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Fri, 9 Jul 2021 22:36:28 -0700
Subject: [PATCH 3/7] BUG: Don't generate Julia functions for Unicode aliases
 of GAT types.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These functions did not work. More importantly, they do not make sense,
e.g., `→(:f,A,B)` is not a good alternative to `Hom(:f,A,B)`.
---
 src/core/GAT.jl  | 7 ++-----
 test/core/GAT.jl | 5 +----
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/src/core/GAT.jl b/src/core/GAT.jl
index f33179fd5..7d1305f30 100644
--- a/src/core/GAT.jl
+++ b/src/core/GAT.jl
@@ -634,15 +634,12 @@ end
 """ Julia functions for term and type aliases of GAT.
 """
 function alias_functions(theory::Theory)::Vector{JuliaFunction}
-  # collect all of the types and terms from the theory
-  terms_types = [theory.types; theory.terms]
-  # iterate over the specified aliases
   collect(Iterators.flatten(map(collect(theory.aliases)) do alias
     # collect all of the destination function definitions to alias
     # allows an alias to overite all the type definitions of a function
-    dests = filter(i -> i.name == last(alias), map(x -> x, terms_types))
+    dests = filter(term -> term.name == last(alias), theory.terms)
     # If there are no matching functions, throw a parse error
-    if isempty(dests)
+    if isempty(dests) && !any(type.name == last(alias) for type in theory.types)
       throw(ParseError("Cannot alias undefined type or term $alias"))
     end
     # For each destination, create a Julia function
diff --git a/test/core/GAT.jl b/test/core/GAT.jl
index 8b0a24e35..66c08ed81 100644
--- a/test/core/GAT.jl
+++ b/test/core/GAT.jl
@@ -192,10 +192,7 @@ accessors = [ GAT.JuliaFunction(:(dom(::Hom)), :Ob),
               GAT.JuliaFunction(:(codom(::Hom)), :Ob) ]
 constructors = [ GAT.JuliaFunction(:(id(X::Ob)), :Hom),
                  GAT.JuliaFunction(:(compose(f::Hom, g::Hom)), :Hom) ]
-alias_functions = [
-  GAT.JuliaFunction(:(⋅(f::Hom, g::Hom)), :Hom, :(compose(f, g))),
-  GAT.JuliaFunction(:(→(dom::Ob, codom::Ob)), :Hom, :(Hom(dom, codom))),
-]
+alias_functions = [ GAT.JuliaFunction(:(⋅(f::Hom, g::Hom)), :Hom, :(compose(f, g))) ]
 theory = GAT.theory(Category)
 @test GAT.accessors(theory) == accessors
 @test GAT.constructors(theory) == constructors

From fa179e8a93b652be8b68635004ce7157c817ab98 Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Fri, 9 Jul 2021 22:43:25 -0700
Subject: [PATCH 4/7] ENH: Macro to define `CartesianCategory` instance using
 products.

---
 src/categorical_algebra/Limits.jl | 45 +++++++++++++++++++++++++++++++
 src/categorical_algebra/Sets.jl   | 35 +++++-------------------
 test/categorical_algebra/Sets.jl  |  2 ++
 3 files changed, 53 insertions(+), 29 deletions(-)

diff --git a/src/categorical_algebra/Limits.jl b/src/categorical_algebra/Limits.jl
index f69bf8632..290d88ef5 100644
--- a/src/categorical_algebra/Limits.jl
+++ b/src/categorical_algebra/Limits.jl
@@ -11,6 +11,7 @@ export AbstractLimit, AbstractColimit, Limit, Colimit,
   BinaryCoproduct, Coproduct, coproduct, coproj1, coproj2, copair,
   BinaryPushout, Pushout, pushout,
   BinaryCoequalizer, Coequalizer, coequalizer, proj,
+  @cartesian_monoidal_from_limits,
   ComposeProductEqualizer, ComposeCoproductCoequalizer
 
 using AutoHashEquals
@@ -258,6 +259,50 @@ define the method `universal(::Coequalizer{T}, ::SMulticospan{1,T})`.
 factorize(lim::Equalizer, h) = universal(lim, SMultispan{1}(h))
 factorize(colim::Coequalizer, h) = universal(colim, SMulticospan{1}(h))
 
+# (Co)cartesian monoidal categories
+###################################
+
+""" Define cartesian monoidal structure using limits.
+
+Implements an instance of [`CartesianCategory`](@ref) assuming that finite
+products have been implemented following the limits interface.
+"""
+macro cartesian_monoidal_from_limits(Ob, Hom)
+  esc(quote
+    import Catlab.Theories: CartesianCategory, otimes, ⊗, munit, braid, σ,
+      mcopy, delete, pair, proj1, proj2, Δ, ◊
+
+    @instance CartesianCategory{$Ob, $Hom} begin
+      @import dom, codom, compose, ⋅, id, munit, delete, pair
+
+      otimes(A::$Ob, B::$Ob) = ob(product(A, B))
+
+      function otimes(f::$Hom, g::$Hom)
+        π1, π2 = product(dom(f), dom(g))
+        pair(product(codom(f), codom(g)), π1⋅f, π2⋅g)
+      end
+
+      function braid(A::$Ob, B::$Ob)
+        AB, BA = product(A, B), product(B, A)
+        pair(BA, proj2(AB), proj1(AB))
+      end
+
+      mcopy(A::$Ob) = pair(id(A),id(A))
+      proj1(A::SetOb, B::SetOb) = proj1(product(A, B))
+      proj2(A::SetOb, B::SetOb) = proj2(product(A, B))
+    end
+
+    otimes(As::AbstractVector{<:$Ob}) = ob(product(As))
+
+    function otimes(fs::AbstractVector{<:$Hom})
+      Π, Π′ = product(map(dom, fs)), product(map(codom, fs))
+      pair(Π′, map(compose, legs(Π), fs))
+    end
+
+    munit(::Type{T}) where T <: $Ob = ob(terminal(T))
+  end)
+end
+
 # Composite (co)limits
 ######################
 
diff --git a/src/categorical_algebra/Sets.jl b/src/categorical_algebra/Sets.jl
index 874f99f06..5986d4b86 100644
--- a/src/categorical_algebra/Sets.jl
+++ b/src/categorical_algebra/Sets.jl
@@ -5,12 +5,10 @@ export SetOb, TypeSet, PredicatedSet, SetFunction, ConstantFunction
 
 using AutoHashEquals
 using FunctionWrappers: FunctionWrapper
-using StaticArrays: SVector
 
 using ...GAT, ..FreeDiagrams, ..Limits
-using ...Theories: CartesianCategory
-import ...Theories: dom, codom, id, compose, ⋅, ∘, otimes, ⊗, munit, braid, σ,
-  mcopy, delete, pair, proj1, proj2, Δ, ◊
+using ...Theories: Category
+import ...Theories: dom, codom, id, compose, ⋅, ∘
 import ..Limits: limit, universal
 
 # Data types
@@ -142,14 +140,12 @@ function (f::PredicatedFunction{T,T′})(x::T)::T′ where {T,T′}
   y
 end
 
-# Cartesian category of sets
-############################
+# Category of sets
+##################
 
 """ Category of sets and functions.
 """
-@instance CartesianCategory{SetOb, SetFunction} begin
-  @import munit, delete, pair
-
+@instance Category{SetOb, SetFunction} begin
   dom(f::SetFunction) = f.dom
   codom(f::SetFunction) = f.codom
 
@@ -160,18 +156,6 @@ end
       error("Domain mismatch in composition: $(codom(f)) != $(dom(g))")
     compose_maybe_id(f, g)
   end
-
-  otimes(A::SetOb, B::SetOb) = otimes(SVector(A, B))
-  otimes(f::SetFunction, g::SetFunction) = otimes(SVector(f, g))
-
-  function braid(A::SetOb, B::SetOb)
-    AB, BA = product(A, B), product(B, A)
-    pair(BA, proj2(AB), proj1(AB))
-  end
-
-  mcopy(A::SetOb) = pair(id(A),id(A))
-  proj1(A::SetOb, B::SetOb) = proj1(product(A, B))
-  proj2(A::SetOb, B::SetOb) = proj2(product(A, B))
 end
 
 @inline compose_maybe_id(f::SetFunction, g::SetFunction) = compose_impl(f, g)
@@ -189,14 +173,7 @@ compose_impl(c::ConstantFunction, f::SetFunction) =
 compose_impl(c::ConstantFunction, d::ConstantFunction) =
   ConstantFunction(d.value, dom(c), codom(d))
 
-otimes(As::AbstractVector{<:SetOb}) = ob(product(As))
-
-function otimes(fs::AbstractVector{<:SetFunction})
-  Π, Π′ = product(map(dom, fs)), product(map(codom, fs))
-  pair(Π′, map(compose, legs(Π), fs))
-end
-
-munit(::Type{S}) where S <: SetOb = ob(terminal(S))
+@cartesian_monoidal_from_limits SetOb SetFunction
 
 # Limits
 ########
diff --git a/test/categorical_algebra/Sets.jl b/test/categorical_algebra/Sets.jl
index da5cde97b..1d8a6bcfe 100644
--- a/test/categorical_algebra/Sets.jl
+++ b/test/categorical_algebra/Sets.jl
@@ -86,8 +86,10 @@ lim = product(fill(TypeSet(Int), 3))
 @test ob(lim) == TypeSet(Tuple{Int,Int,Int})
 π1, π2, π3 = lim
 @test (π1((1,2,3)), π2((1,2,3)), π3((1,2,3))) == (1,2,3)
+@test otimes(fill(TypeSet(Int), 3)) == TypeSet(Tuple{Int,Int,Int})
 
 fs = [ SetFunction(x -> x+i, TypeSet(Int), TypeSet(Int)) for i in 1:3 ]
 @test pair(lim, fs)(3) == (4,5,6)
+@test otimes(fs)((1,5,10)) == (2,7,13)
 
 end

From 17895f4b9662b773f7dd00cc3b2ecc6ac021c673 Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Fri, 9 Jul 2021 23:18:01 -0700
Subject: [PATCH 5/7] ENH: Macro to define `CocartesianCategory` instance using
 coproducts.

---
 src/categorical_algebra/FinSets.jl  |  7 +++-
 src/categorical_algebra/Limits.jl   | 50 ++++++++++++++++++++++++++---
 src/categorical_algebra/Sets.jl     |  2 +-
 src/wiring_diagrams/Undirected.jl   |  7 +---
 test/categorical_algebra/FinSets.jl |  4 +++
 5 files changed, 58 insertions(+), 12 deletions(-)

diff --git a/src/categorical_algebra/FinSets.jl b/src/categorical_algebra/FinSets.jl
index 09c8ffb3f..f7e8de87f 100644
--- a/src/categorical_algebra/FinSets.jl
+++ b/src/categorical_algebra/FinSets.jl
@@ -13,7 +13,8 @@ import StaticArrays
 using StaticArrays: StaticVector, SVector, SizedVector, similar_type
 
 @reexport using ..Sets
-using ...Theories, ...CSetDataStructures, ...Graphs, ..FreeDiagrams, ..Limits
+using ...GAT, ...Theories
+using ...CSetDataStructures, ...Graphs, ..FreeDiagrams, ..Limits
 import ...Theories: dom, codom
 import ..Limits: limit, colimit, universal
 using ..Sets: SetFunctionCallable, SetFunctionIdentity
@@ -146,6 +147,10 @@ Base.show(io::IO, f::FinFunctionVector) =
 Sets.compose_impl(f::FinFunctionVector, g::FinDomFunctionVector) =
   FinDomFunctionVector(g.func[f.func], codom(g))
 
+# Note: Cartesian monoidal structure is implemented generically for Set but
+# cocartesian only for FinSet.
+@cocartesian_monoidal_instance FinSet FinFunction
+
 # Indexed functions
 #------------------
 
diff --git a/src/categorical_algebra/Limits.jl b/src/categorical_algebra/Limits.jl
index 290d88ef5..8297a5c99 100644
--- a/src/categorical_algebra/Limits.jl
+++ b/src/categorical_algebra/Limits.jl
@@ -11,7 +11,7 @@ export AbstractLimit, AbstractColimit, Limit, Colimit,
   BinaryCoproduct, Coproduct, coproduct, coproj1, coproj2, copair,
   BinaryPushout, Pushout, pushout,
   BinaryCoequalizer, Coequalizer, coequalizer, proj,
-  @cartesian_monoidal_from_limits,
+  @cartesian_monoidal_instance, @cocartesian_monoidal_instance,
   ComposeProductEqualizer, ComposeCoproductCoequalizer
 
 using AutoHashEquals
@@ -267,7 +267,7 @@ factorize(colim::Coequalizer, h) = universal(colim, SMulticospan{1}(h))
 Implements an instance of [`CartesianCategory`](@ref) assuming that finite
 products have been implemented following the limits interface.
 """
-macro cartesian_monoidal_from_limits(Ob, Hom)
+macro cartesian_monoidal_instance(Ob, Hom)
   esc(quote
     import Catlab.Theories: CartesianCategory, otimes, ⊗, munit, braid, σ,
       mcopy, delete, pair, proj1, proj2, Δ, ◊
@@ -288,8 +288,8 @@ macro cartesian_monoidal_from_limits(Ob, Hom)
       end
 
       mcopy(A::$Ob) = pair(id(A),id(A))
-      proj1(A::SetOb, B::SetOb) = proj1(product(A, B))
-      proj2(A::SetOb, B::SetOb) = proj2(product(A, B))
+      proj1(A::$Ob, B::$Ob) = proj1(product(A, B))
+      proj2(A::$Ob, B::$Ob) = proj2(product(A, B))
     end
 
     otimes(As::AbstractVector{<:$Ob}) = ob(product(As))
@@ -303,6 +303,48 @@ macro cartesian_monoidal_from_limits(Ob, Hom)
   end)
 end
 
+""" Define cocartesian monoidal structure using colimits.
+
+Implements an instance of [`CocartesianCategory`](@ref) assuming that finite
+coproducts have been implemented following the colimits interface.
+"""
+macro cocartesian_monoidal_instance(Ob, Hom)
+  esc(quote
+    import Catlab.Theories: CocartesianCategory, oplus, ⊕, mzero, swap,
+      plus, zero, copair, coproj1, coproj2
+
+    @instance CocartesianCategory{$Ob, $Hom} begin
+      @import dom, codom, compose, ⋅, id, mzero, copair
+
+      oplus(A::$Ob, B::$Ob) = ob(coproduct(A, B))
+
+      function oplus(f::$Hom, g::$Hom)
+        ι1, ι2 = coproduct(codom(f), codom(g))
+        copair(coproduct(dom(f), dom(g)), f⋅ι1, g⋅ι2)
+      end
+
+      function swap(A::$Ob, B::$Ob)
+        AB, BA = coproduct(A, B), coproduct(B, A)
+        copair(AB, coproj2(BA), coproj1(BA))
+      end
+
+      plus(A::$Ob) = copair(id(A),id(A))
+      zero(A::$Ob) = create(A)
+      coproj1(A::$Ob, B::$Ob) = coproj1(coproduct(A, B))
+      coproj2(A::$Ob, B::$Ob) = coproj2(coproduct(A, B))
+    end
+
+    oplus(As::AbstractVector{<:$Ob}) = ob(coproduct(As))
+
+    function oplus(fs::AbstractVector{<:$Hom})
+      ⊔, ⊔′ = coproduct(map(dom, fs)), coproduct(map(codom, fs))
+      copair(⊔, map(compose, fs, legs(⊔′)))
+    end
+
+    mzero(::Type{T}) where T <: $Ob = ob(initial(T))
+  end)
+end
+
 # Composite (co)limits
 ######################
 
diff --git a/src/categorical_algebra/Sets.jl b/src/categorical_algebra/Sets.jl
index 5986d4b86..c67b65e4e 100644
--- a/src/categorical_algebra/Sets.jl
+++ b/src/categorical_algebra/Sets.jl
@@ -173,7 +173,7 @@ compose_impl(c::ConstantFunction, f::SetFunction) =
 compose_impl(c::ConstantFunction, d::ConstantFunction) =
   ConstantFunction(d.value, dom(c), codom(d))
 
-@cartesian_monoidal_from_limits SetOb SetFunction
+@cartesian_monoidal_instance SetOb SetFunction
 
 # Limits
 ########
diff --git a/src/wiring_diagrams/Undirected.jl b/src/wiring_diagrams/Undirected.jl
index bb46ff46b..f9c2b1e44 100644
--- a/src/wiring_diagrams/Undirected.jl
+++ b/src/wiring_diagrams/Undirected.jl
@@ -10,7 +10,7 @@ export UndirectedWiringDiagram, UntypedUWD, TypedUWD,
 
 using ...Present, ...CategoricalAlgebra.CSets, ...CategoricalAlgebra.Limits
 using ...CategoricalAlgebra.FinSets: FinSet, FinFunction
-using ...Theories: dom, codom, compose, ⋅, id
+using ...Theories: dom, codom, compose, ⋅, id, oplus
 import ..DirectedWiringDiagrams: box, boxes, nboxes, add_box!, add_wire!,
   add_wires!, singleton_diagram, ocompose, substitute
 
@@ -305,9 +305,4 @@ end
 flat(x) = reduce(vcat, x, init=Int[])
 flatmap(f, xs...) = mapreduce(f, vcat, xs..., init=Int[])
 
-# FIXME: Should be defined in FinSets.
-function oplus(fs::AbstractVector{<:FinFunction})
-  copair(coproduct(map(dom, fs)), map(compose, fs, coproduct(map(codom, fs))))
-end
-
 end
diff --git a/test/categorical_algebra/FinSets.jl b/test/categorical_algebra/FinSets.jl
index 51a1d23af..7c0ce8b43 100644
--- a/test/categorical_algebra/FinSets.jl
+++ b/test/categorical_algebra/FinSets.jl
@@ -258,16 +258,20 @@ lim = π1, π2 = limit(d)
 # Initial object.
 @test ob(initial(FinSet{Int})) == FinSet(0)
 @test create(initial(FinSet{Int}), FinSet(3)) == FinFunction(Int[], 3)
+@test mzero(FinSet{Int}) == FinSet(0)
 
 # Binary coproduct.
 colim = coproduct(FinSet(2), FinSet(3))
 @test ob(colim) == FinSet(5)
 @test coproj1(colim) == FinFunction([1,2], 5)
 @test coproj2(colim) == FinFunction([3,4,5], 5)
+@test FinSet(2)⊕FinSet(3) == FinSet(5)
 
 f, g = FinFunction([3,5], 5), FinFunction([1,2,3], 5)
 @test force(coproj1(colim) ⋅ copair(colim,f,g)) == f
 @test force(coproj2(colim) ⋅ copair(colim,f,g)) == g
+@test f⊕g == FinFunction([3,5,6,7,8], 10)
+@test swap(FinSet(2), FinSet(3)) == FinFunction([4,5,1,2,3])
 
 # N-ary coproduct.
 colim = coproduct([FinSet(2), FinSet(3)])

From 44e02bd05c0f0abb875d37d7aee5a07991872f7b Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Mon, 12 Jul 2021 10:06:21 -0700
Subject: [PATCH 6/7] TST: Missing tests for (co)cartesian monoidal struct from
 (co)limits.

---
 test/categorical_algebra/FinSets.jl | 14 ++++++++++----
 test/categorical_algebra/Sets.jl    | 22 ++++++++++++++--------
 2 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/test/categorical_algebra/FinSets.jl b/test/categorical_algebra/FinSets.jl
index 7c0ce8b43..5f932239e 100644
--- a/test/categorical_algebra/FinSets.jl
+++ b/test/categorical_algebra/FinSets.jl
@@ -258,20 +258,16 @@ lim = π1, π2 = limit(d)
 # Initial object.
 @test ob(initial(FinSet{Int})) == FinSet(0)
 @test create(initial(FinSet{Int}), FinSet(3)) == FinFunction(Int[], 3)
-@test mzero(FinSet{Int}) == FinSet(0)
 
 # Binary coproduct.
 colim = coproduct(FinSet(2), FinSet(3))
 @test ob(colim) == FinSet(5)
 @test coproj1(colim) == FinFunction([1,2], 5)
 @test coproj2(colim) == FinFunction([3,4,5], 5)
-@test FinSet(2)⊕FinSet(3) == FinSet(5)
 
 f, g = FinFunction([3,5], 5), FinFunction([1,2,3], 5)
 @test force(coproj1(colim) ⋅ copair(colim,f,g)) == f
 @test force(coproj2(colim) ⋅ copair(colim,f,g)) == g
-@test f⊕g == FinFunction([3,5,6,7,8], 10)
-@test swap(FinSet(2), FinSet(3)) == FinFunction([4,5,1,2,3])
 
 # N-ary coproduct.
 colim = coproduct([FinSet(2), FinSet(3)])
@@ -282,6 +278,16 @@ colim = coproduct([FinSet(2), FinSet(3)])
 @test force(first(legs(colim)) ⋅ copair(colim,[f,g])) == f
 @test force(last(legs(colim)) ⋅ copair(colim,[f,g])) == g
 
+# Cocartesian monoidal structure.
+@test FinSet(2)⊕FinSet(3) == FinSet(5)
+@test oplus([FinSet(2), FinSet(3), FinSet(4)]) == FinSet(9)
+@test f⊕g == FinFunction([3,5,6,7,8], 10)
+@test mzero(FinSet{Int}) == FinSet(0)
+@test swap(FinSet(2), FinSet(3)) == FinFunction([4,5,1,2,3])
+ι1, ι2 = coproj1(FinSet(2),FinSet(3)), coproj2(FinSet(2),FinSet(3))
+@test ι1 == FinFunction([1,2], 5)
+@test ι2 == FinFunction([3,4,5], 5)
+
 # Coequalizers
 #-------------
 
diff --git a/test/categorical_algebra/Sets.jl b/test/categorical_algebra/Sets.jl
index 1d8a6bcfe..ec6b8e8f3 100644
--- a/test/categorical_algebra/Sets.jl
+++ b/test/categorical_algebra/Sets.jl
@@ -63,33 +63,39 @@ plus_two_to_odd = compose(plus_one_to_odd, plus_one_to_even)
 # Terminal object.
 @test ob(terminal(TypeSet)) == TypeSet(Nothing)
 @test delete(terminal(TypeSet), TypeSet(Int))(3) == nothing
-@test munit(TypeSet) == TypeSet(Nothing)
 
 # Binary product.
 lim = product(TypeSet(Int), TypeSet(String))
 @test ob(lim) == TypeSet(Tuple{Int,String})
 π1, π2 = lim
 @test (π1((1,"foo")), π2((1,"foo"))) == (1,"foo")
-@test TypeSet(Int) ⊗ TypeSet(String) == TypeSet(Tuple{Int,String})
-@test σ(TypeSet(Int), TypeSet(String))((1,"foo")) == ("foo",1)
 
 f = SetFunction(length, TypeSet(Vector{String}), TypeSet(Int))
 g = SetFunction(v -> sprint(join, v), TypeSet(Vector{String}), TypeSet(String))
 @test pair(lim, f, g)(["foo", "bar", "baz"]) == (3, "foobarbaz")
 
-@test (f⊗g)((["foo"], ["bar", "baz"])) == (1, "barbaz")
-@test Δ(TypeSet(Int))(2) == (2,2)
-@test ◊(TypeSet(Int))(1) == nothing
-
 # N-ary product.
 lim = product(fill(TypeSet(Int), 3))
 @test ob(lim) == TypeSet(Tuple{Int,Int,Int})
 π1, π2, π3 = lim
 @test (π1((1,2,3)), π2((1,2,3)), π3((1,2,3))) == (1,2,3)
-@test otimes(fill(TypeSet(Int), 3)) == TypeSet(Tuple{Int,Int,Int})
 
 fs = [ SetFunction(x -> x+i, TypeSet(Int), TypeSet(Int)) for i in 1:3 ]
 @test pair(lim, fs)(3) == (4,5,6)
+
+# Cartesian monoidal structure.
+@test TypeSet(Int) ⊗ TypeSet(String) == TypeSet(Tuple{Int,String})
+@test munit(TypeSet) == TypeSet(Nothing)
+@test σ(TypeSet(Int), TypeSet(String))((1,"foo")) == ("foo",1)
+π1 = proj1(TypeSet(Int), TypeSet(String))
+π2 = proj2(TypeSet(Int), TypeSet(String))
+@test (π1((1,"foo")), π2((1,"foo"))) == (1,"foo")
+
+@test (f⊗g)((["foo"], ["bar", "baz"])) == (1, "barbaz")
+@test Δ(TypeSet(Int))(2) == (2,2)
+@test ◊(TypeSet(Int))(1) == nothing
+
+@test otimes(fill(TypeSet(Int), 3)) == TypeSet(Tuple{Int,Int,Int})
 @test otimes(fs)((1,5,10)) == (2,7,13)
 
 end

From fa26ddc40039c02b3f623c166acadde5bd23314d Mon Sep 17 00:00:00 2001
From: Evan Patterson <evan@epatters.org>
Date: Mon, 12 Jul 2021 13:45:58 -0700
Subject: [PATCH 7/7] ENH: Instances of ACSets as (co)cartesian monoidal
 categories.

---
 src/categorical_algebra/CSets.jl  | 8 ++++++--
 test/categorical_algebra/CSets.jl | 4 ++--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 80fd4b28d..80339b251 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -437,6 +437,9 @@ end
 
 fin_sets(X::ACSet) = map(table -> FinSet(length(table)), tables(X))
 
+@cartesian_monoidal_instance CSet CSetTransformation
+@cocartesian_monoidal_instance ACSet ACSetTransformation
+
 # Limits and colimits
 #####################
 
@@ -585,8 +588,9 @@ cocone_objects(diagram::BipartiteFreeDiagram) = ob₂(diagram)
 cocone_objects(span::Multispan) = feet(span)
 cocone_objects(para::ParallelMorphisms) = SVector(codom(para))
 
-# Serialization and Deserialization of ACSets
-#############################################
+# Serialization
+###############
+
 """ Serialize an ACSet object to a JSON string
 """
 function generate_json_acset(x::T) where T <: AbstractACSet
diff --git a/test/categorical_algebra/CSets.jl b/test/categorical_algebra/CSets.jl
index 2a9acf96d..0313de196 100644
--- a/test/categorical_algebra/CSets.jl
+++ b/test/categorical_algebra/CSets.jl
@@ -342,8 +342,8 @@ h = cycle_graph(LabeledGraph{Symbol}, 4, V=(label=[:c,:d,:a,:b],))
 h = cycle_graph(LabeledGraph{Symbol}, 4, V=(label=[:a,:b,:d,:c],))
 @test !is_homomorphic(g, h)
 
-# Serialization and Deserialization of ACSets
-#############################################
+# Serialization
+###############
 
 @present TheoryDDS(FreeSchema) begin
   X::Ob