{
"cells": [
{
"cell_type": "markdown",
"source": [
"# Wiring diagrams and syntactic expressions\n",
"\n",
"\n",
"Morphisms in a monoidal category can be represented as syntactic expressions,\n",
"such as $f \\cdot g$ and $f \\otimes g$, and also as [wiring\n",
"diagrams](@ref wiring_diagram_basics), aka *string diagrams*. Catlab provides\n",
"facilities for transforming between these two representations."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "show_diagram (generic function with 1 method)"
},
"metadata": {},
"execution_count": 1
}
],
"cell_type": "code",
"source": [
"using Catlab.Theories, Catlab.WiringDiagrams\n",
"using Catlab.Graphics\n",
"\n",
"function show_diagram(d::WiringDiagram)\n",
" to_graphviz(d, orientation=LeftToRight, labels=false)\n",
"end"
],
"metadata": {},
"execution_count": 1
},
{
"cell_type": "markdown",
"source": [
"## Expressions to diagrams\n",
"\n",
"Converting a morphism expression to a wiring diagram is conceptually and\n",
"algorithmically simple, because every expression determines a unique diagram.\n",
"\n",
"As a simple example, here is the monoidal product of two generators, $f$ and\n",
"$g$, first as an expression (displayed using LaTeX) and then as a wiring\n",
"diagram (displayed using Graphviz)."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "f⊗g: A⊗B → B⊗C",
"text/latex": "$f \\otimes g : A \\otimes B \\to B \\otimes C$"
},
"metadata": {},
"execution_count": 2
}
],
"cell_type": "code",
"source": [
"A, B, C, D, E = Ob(FreeCartesianCategory, :A, :B, :C, :D, :E)\n",
"f = Hom(:f, A, B)\n",
"g = Hom(:g, B, C)\n",
"\n",
"expr = f ⊗ g"
],
"metadata": {},
"execution_count": 2
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"f\", :fillcolor => \"white\", :id => \"n1\", :label => Catlab.Graphics.Graphviz.Html(\"
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"g\", :fillcolor => \"white\", :id => \"n2\", :label => Catlab.Graphics.Graphviz.Html(\"\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e4\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))",
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
]
},
"metadata": {},
"execution_count": 3
}
],
"cell_type": "code",
"source": [
"show_diagram(to_wiring_diagram(expr))"
],
"metadata": {},
"execution_count": 3
},
{
"cell_type": "markdown",
"source": [
"Here is a monoidal product of compositions:"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E",
"text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$"
},
"metadata": {},
"execution_count": 4
}
],
"cell_type": "code",
"source": [
"h = Hom(:h, C, D)\n",
"k = Hom(:k, D, E)\n",
"\n",
"expr = (f ⋅ g) ⊗ (h ⋅ k)"
],
"metadata": {},
"execution_count": 4
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"f\", :fillcolor => \"white\", :id => \"n1\", :label => Catlab.Graphics.Graphviz.Html(\"\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"g\", :fillcolor => \"white\", :id => \"n2\", :label => Catlab.Graphics.Graphviz.Html(\"\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n3\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"h\", :fillcolor => \"white\", :id => \"n3\", :label => Catlab.Graphics.Graphviz.Html(\"\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n4\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"k\", :fillcolor => \"white\", :id => \"n4\", :label => Catlab.Graphics.Graphviz.Html(\"\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n3\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n3\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n4\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"D\", :id => \"e4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e5\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n4\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"E\", :id => \"e6\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))",
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
]
},
"metadata": {},
"execution_count": 5
}
],
"cell_type": "code",
"source": [
"show_diagram(to_wiring_diagram(expr))"
],
"metadata": {},
"execution_count": 5
},
{
"cell_type": "markdown",
"source": [
"## Diagrams to expressions\n",
"\n",
"Converting a wiring diagram to a syntactic expression is algorithmically more\n",
"challenging, due to the fact that a single wiring diagram generally admits\n",
"many different representations as an expression. Thus, a particular expression\n",
"must be singled out.\n",
"\n",
"To bring this out, we define a function that round-trips a morphism expression\n",
"to a wiring diagram and then back to an expression."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "roundtrip_expr (generic function with 1 method)"
},
"metadata": {},
"execution_count": 6
}
],
"cell_type": "code",
"source": [
"function roundtrip_expr(expr::FreeCartesianCategory.Hom)\n",
" d = to_wiring_diagram(expr)\n",
" to_hom_expr(FreeCartesianCategory, d)\n",
"end"
],
"metadata": {},
"execution_count": 6
},
{
"cell_type": "markdown",
"source": [
"We can recover the expression just considered above:"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E",
"text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$"
},
"metadata": {},
"execution_count": 7
}
],
"cell_type": "code",
"source": [
"roundtrip_expr((f ⋅ g) ⊗ (h ⋅ k))"
],
"metadata": {},
"execution_count": 7
},
{
"cell_type": "markdown",
"source": [
"But here is a different expression that round-trips to the same thing:"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E",
"text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$"
},
"metadata": {},
"execution_count": 8
}
],
"cell_type": "code",
"source": [
"roundtrip_expr((f ⊗ h) ⋅ (g ⊗ k))"
],
"metadata": {},
"execution_count": 8
},
{
"cell_type": "markdown",
"source": [
"The equality of these two expressions,\n",
"\n",
"$$\n",
"(f \\cdot g) \\otimes (h \\cdot k) = (f \\otimes h) \\cdot (g \\otimes k),\n",
"$$\n",
"\n",
"is the *interchange law* in a monoidal category. It says that composition and\n",
"monoidal products can be interchanged. As this example shows, the conversion\n",
"algorithm in Catlab favors products over composition, placing products towards\n",
"the root of the expression tree wherever possible.\n",
"Other laws can be discovered by this procedure. Since we are working in a\n",
"[cartesian monoidal\n",
"category](https://ncatlab.org/nlab/show/cartesian+monoidal+category),\n",
"operations of copying, $\\Delta_A: A \\to A \\otimes A$, and deleting,\n",
"$\\lozenge_A: A \\to I$, are available.\n",
"\n",
"Consider the operation of copying the product $A \\otimes B$."
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "mcopy{A⊗B}: A⊗B → A⊗B⊗A⊗B",
"text/latex": "$\\Delta_{A \\otimes B} : A \\otimes B \\to A \\otimes B \\otimes A \\otimes B$"
},
"metadata": {},
"execution_count": 9
}
],
"cell_type": "code",
"source": [
"expr = mcopy(A ⊗ B)"
],
"metadata": {},
"execution_count": 9
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Node(\"n0out3\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out3\")), Catlab.Graphics.Graphviz.Node(\"n0out4\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out3\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out4\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"junction\", :fillcolor => \"black\", :height => \"0.05\", :id => \"n1\", :label => \"\", :shape => \"circle\", :style => \"filled\", :width => \"0.05\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"junction\", :fillcolor => \"black\", :height => \"0.05\", :id => \"n2\", :label => \"\", :shape => \"circle\", :style => \"filled\", :width => \"0.05\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out3\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e5\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out4\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e6\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))",
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
]
},
"metadata": {},
"execution_count": 10
}
],
"cell_type": "code",
"source": [
"show_diagram(add_junctions!(to_wiring_diagram(expr)))"
],
"metadata": {},
"execution_count": 10
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "(mcopy{A}⊗mcopy{B})⋅(id{A}⊗(AσB)⊗id{B}): A⊗B → A⊗B⊗A⊗B",
"text/latex": "$\\left(\\Delta_{A} \\otimes \\Delta_{B}\\right) \\cdot \\left(\\mathrm{id}_{A} \\otimes \\sigma_{A,B} \\otimes \\mathrm{id}_{B}\\right) : A \\otimes B \\to A \\otimes B \\otimes A \\otimes B$"
},
"metadata": {},
"execution_count": 11
}
],
"cell_type": "code",
"source": [
"roundtrip_expr(expr)"
],
"metadata": {},
"execution_count": 11
},
{
"cell_type": "markdown",
"source": [
"The equation just witnessed,\n",
"\n",
"$$\n",
"\\Delta_{A \\otimes B} = (\\Delta_A \\otimes \\Delta_B) \\cdot (1_A \\otimes \\sigma_{A,B} \\otimes 1_B),\n",
"$$\n",
"\n",
"is one of the *coherence laws* for cartesian products\n",
"([arXiv:0908.3347](https://arxiv.org/abs/0908.3347), Table 7). Another\n",
"coherence law for products is\n",
"\n",
"$$\n",
"\\lozenge_{A \\otimes B} = \\lozenge_A \\otimes \\lozenge_B.\n",
"$$"
],
"metadata": {}
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "delete{A⊗B}: A⊗B → I",
"text/latex": "$\\lozenge_{A \\otimes B} : A \\otimes B \\to I$"
},
"metadata": {},
"execution_count": 12
}
],
"cell_type": "code",
"source": [
"expr = delete(A ⊗ B)"
],
"metadata": {},
"execution_count": 12
},
{
"outputs": [
{
"output_type": "execute_result",
"data": {
"text/plain": "delete{A}⊗delete{B}: A⊗B → I",
"text/latex": "$\\lozenge_{A} \\otimes \\lozenge_{B} : A \\otimes B \\to I$"
},
"metadata": {},
"execution_count": 13
}
],
"cell_type": "code",
"source": [
"roundtrip_expr(expr)"
],
"metadata": {},
"execution_count": 13
}
],
"nbformat_minor": 3,
"metadata": {
"language_info": {
"file_extension": ".jl",
"mimetype": "application/julia",
"name": "julia",
"version": "1.7.3"
},
"kernelspec": {
"name": "julia-1.7",
"display_name": "Julia 1.7.3",
"language": "julia"
}
},
"nbformat": 4
}