diff --git a/.gitignore b/.gitignore index a4a5a163f..94a39a3d4 100644 --- a/.gitignore +++ b/.gitignore @@ -50,6 +50,7 @@ web_modules/ # Optional npm cache directory .npm +.pnpm-store # Optional eslint cache .eslintcache diff --git a/dev-docs/README.md b/dev-docs/README.md index f091c169b..c25bca87b 100644 --- a/dev-docs/README.md +++ b/dev-docs/README.md @@ -13,4 +13,4 @@ To build this forest, you need to have a working installation of the following s To build the forest, then simply run `./forester build`. To view the forest, run `./serve.sh` and go to `http://localhost:8080/index.xml` in your web browser. Note that you will need python installed for `./serve.sh` to work properly. -If you have `inotifywait` installed, you can run `./watch.sh` to watch for changes to the `trees` directory and rebuild accordingly. +You can run `./watch.sh` to watch for changes to the `trees` directory and rebuild accordingly. diff --git a/dev-docs/trees/dbl-0001.tree b/dev-docs/trees/dbl-0001.tree index 767467206..d98192df8 100644 --- a/dev-docs/trees/dbl-0001.tree +++ b/dev-docs/trees/dbl-0001.tree @@ -4,4 +4,5 @@ \li{[[dbl-0002]]} \li{[[dbl-0008]]} \li{[[dbl-0005]]} +\li{[[dbl-000C]]} } diff --git a/dev-docs/trees/dbl-000B.tree b/dev-docs/trees/dbl-000B.tree new file mode 100644 index 000000000..428959044 --- /dev/null +++ b/dev-docs/trees/dbl-000B.tree @@ -0,0 +1,46 @@ +\title{Undesirable bimodules between multicategories} +\taxon{example} +\import{macros} + +\p{Consider a [multicategory](dct-000A) #{\cat{M}} as a model of the following theory:} +\transclude{thy-000A} +\p{The terminal multicategory \cat{1} has a single object #{\bullet} and a single multimorphism +#{(\bullet)^k\to \bullet} for each arity #{k}. + +A bimodule #{H: \cat{1} \proTo \cat{M}} contains, by definition, +spans #{H_p: 1^m\proto M_0^n} for each #{p:x^m\proto x^n} in #{\mathbb{T}_{\mathrm{pm}}}. For a \em{cartesian} bimodule #{H}, +these are all uniquely determined by the choices of +#{H_{\mu_m}:1^m\proto M_0}, and most of the action cells will be similarly +redundant. + +Taking this reduction into account, the only other data is the action +cells, fixing some #{p:\ell\proto m}, which we'll draw globularly as there are no nonstructural arrows in #{\mathbb{T}_{\mathrm{pm}}}: +} +\quiver{ + % https://q.uiver.app/#q=WzAsNCxbMCwwLCIxXlxcZWxsIl0sWzEsMCwiMV5tIl0sWzEsMSwiTV5uIl0sWzAsMSwiTV5tIl0sWzAsMywiSF97XFxlbGwsbX0iLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMywyLCJNX3ttLG59IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEsMiwiSF97bSxufSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFswLDEsIjFfe1xcZWxsLG19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzAsMiwiSF97XFxlbGwsbn0iLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSw4LCIiLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9fV0sWzMsOCwiIiwxLHsic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfX1dXQ== +\begin{tikzcd} + {1^\ell} & {1^m} \\ + {M^m} & {M} + \arrow["{1_{p}}", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["{H_{p}}"', "\shortmid"{marking}, from=1-1, to=2-1] + \arrow[""{name=0, anchor=center, inner sep=0}, "{H_{\mu_\ell}}"{description}, "\shortmid"{marking}, from=1-1, to=2-2] + \arrow["{H_{\mu_m}}", "\shortmid"{marking}, from=1-2, to=2-2] + \arrow["{M_{\mu_m}}"', "\shortmid"{marking}, from=2-1, to=2-2] + \arrow[shorten >=2pt, Rightarrow, from=1-2, to=0] + \arrow[shorten >=2pt, Rightarrow, from=2-1, to=0] +\end{tikzcd} +} +\p{We can thus think of #{H} as, first, equipping each object #{x:\cat{M}} with +a set of hetero-multimorphisms #{(\bullet)^k\to x} for each #{k\ge 0}. The +lower-left action cell says how to compose #{m} such heteromorphisms whose +codomain is a list #{(x_i)} with a morphism #{(x_i)\to y} in #{M}. +This much is a multifunctor from #{\cat{M}} into a multicategory +of #{\mathbb{N}}-graded sets corresponding to the monoidal product on +such sets in which #{(A\otimes B)_c=\sum_{a+b=c} A_a\times B_b}; this +is the \nlab{Day convolution} product for presheaves on the discrete monoidal +category #{\mathbb{N}}.} + +\p{The upper-right action cell shows how every map #{p:\ell\to m} in +the augmented simplex category produces a corresponding map from #{m}-ary +to #{\ell}-ary heteromorphisms into each object. This upgrades the +#{\mathbb N}-graded sets #{(X_m)} discussed above into augmented simplicial sets! That is, a bimodule out of \cat{1} is a multifunctor into augmented simplicial sets. This is cool, but probably a bit much for most purposes.} diff --git a/dev-docs/trees/dbl-000C.tree b/dev-docs/trees/dbl-000C.tree new file mode 100644 index 000000000..de504183e --- /dev/null +++ b/dev-docs/trees/dbl-000C.tree @@ -0,0 +1,366 @@ +\title{Modules over models of double theories} +\import{macros} + +\p{A \em{module} over a model of a double theory is a special kind of bimodule out of #{1}, the terminal model. Recall that bimodules are defined in ([Lambert & +Patterson 2024](cartesian-double-theories-2024), Definition 9.1). In loc. cit. the word "module" is used where we use "bimodule" here. Here we aim to define a notion of module that is to arbitrary bimodules as, in the case of categories (models of the terminal double theory), #{C}-sets and presheaves are to arbitrary profunctors.} + +\p{An extra constraint is needed to obtain such a definition for models of arbitrary double theories. For instance, in the case of multicategories we'd like to recover multifunctors into \Set, which are known to be a good notion of copresheaf. However, without any constraints, there are [[dbl-000B]]. To solve this problem, we make the following definition, using "instance" as a synonym for "module."} + +\subtree{ + \title{Instance of a model} + \taxon{definition} + + \p{Let \dbl{D} be a double theory and let \dbl{E} be a double category with a terminal object. An \define{instance} of a model #{X} of \dbl{D} in \dbl{E} is a bimodule #{H:1\proTo X} out of the terminal model #{1} of \dbl{D} in \dbl{E} such that "#{1} acts trivially on the left" in the sense that the action cells of the form below are isomorphisms: + \quiver{% https://q.uiver.app/#q=WzAsNSxbMCwwLCIxKHgpIl0sWzEsMCwiMSh5KSJdLFsyLDAsIlgoeikiXSxbMCwxLCIxKHgpIl0sWzIsMSwiWCh6KSJdLFswLDEsIjEobSkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSwyLCJIKG4pIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzMsNCwiSChtbikiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMCwzLCIiLDEseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyLDQsIiIsMSx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d +\begin{tikzcd} + {1(x)} & {1(y)} & {X(z)} \\ + {1(x)} && {X(z)} + \arrow["{1(m)}", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow[Rightarrow, no head, from=1-1, to=2-1] + \arrow["{H(n)}", "\shortmid"{marking}, from=1-2, to=1-3] + \arrow[Rightarrow, no head, from=1-3, to=2-3] + \arrow["{H(mn)}", "\shortmid"{marking}, from=2-1, to=2-3] +\end{tikzcd}} + } + + \p{A \define{co-instance} is a bimodule #{X\proTo 1} satisfying the dual conditions.} +} +\subtree{ + \taxon{Explanation} + \title{Explication of the definition of instance} + \p{ + Let us unfold this example using the definition cited above. Then we have: + \ul{ + \li{For each proarrow #{m:x\proto y} in \dbl{D}, a proarrow #{H(m):1\proto X(y)} in \dbl{E}.} + \li{For every cell as on the left below in \dbl{D}, a corresponding cell as on the right in \cat{E}: + \quiver{\begin{tikzcd} + x & y & 1 & Xy \\ + w & z & 1 & Xz + \arrow[""{name=0, anchor=center, inner sep=0}, "m", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["f"', from=1-1, to=2-1] + \arrow["g", from=1-2, to=2-2] + \arrow[""{name=1, anchor=center, inner sep=0}, "{H(m)}", "\shortmid"{marking}, from=1-3, to=1-4] + \arrow[from=1-3, to=2-3] + \arrow["Xg", from=1-4, to=2-4] + \arrow[""{name=2, anchor=center, inner sep=0}, "n"', "\shortmid"{marking}, from=2-1, to=2-2] + \arrow[""{name=3, anchor=center, inner sep=0}, "{H(n)}"', "\shortmid"{marking}, from=2-3, to=2-4] + \arrow["\alpha"{description}, draw=none, from=0, to=2] + \arrow["{H(\alpha)}"{description}, draw=none, from=1, to=3] + \end{tikzcd}} + } + \li{For every composable pair #{x \xproto{m} y \xproto{n} z} in \dbl{D}, action cells in \dbl{E} as below: + \quiver{% https://q.uiver.app/#q=WzAsMTAsWzAsMCwiMXgiXSxbMSwwLCIxeSJdLFsyLDAsIlh6Il0sWzAsMSwiMXgiXSxbMiwxLCJYeiJdLFszLDAsIjF4Il0sWzQsMCwiWHkiXSxbNSwwLCJYeiJdLFszLDEsIjF4Il0sWzUsMSwiWHoiXSxbMCwxLCIxbSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxLDIsIkhuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzMsNCwiSChtbikiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNSw2LCJIbSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs2LDcsIlhuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzgsOSwiSChtbikiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMCwzLCIiLDIseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyLDQsIiIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzUsOCwiIiwyLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNyw5LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxLDEyLCJIXlxcZWxsX3ttLG59IiwxLHsibGFiZWxfcG9zaXRpb24iOjMwLCJzaG9ydGVuIjp7InRhcmdldCI6MzB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNiwxNSwiSF5yX3ttLG59IiwxLHsibGFiZWxfcG9zaXRpb24iOjMwLCJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0= +\begin{tikzcd} + 1x & 1y & Xz & 1x & Xy & Xz \\ + 1x && Xz & 1x && Xz + \arrow["1m", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow[Rightarrow, no head, from=1-1, to=2-1] + \arrow["Hn", "\shortmid"{marking}, from=1-2, to=1-3] + \arrow[Rightarrow, no head, from=1-3, to=2-3] + \arrow["Hm", "\shortmid"{marking}, from=1-4, to=1-5] + \arrow[Rightarrow, no head, from=1-4, to=2-4] + \arrow["Xn", "\shortmid"{marking}, from=1-5, to=1-6] + \arrow[Rightarrow, no head, from=1-6, to=2-6] + \arrow[""{name=0, anchor=center, inner sep=0}, "{H(mn)}"', "\shortmid"{marking}, from=2-1, to=2-3] + \arrow[""{name=1, anchor=center, inner sep=0}, "{H(mn)}"', "\shortmid"{marking}, from=2-4, to=2-6] + \arrow["{H^\ell_{m,n}}"{description, pos=0.3}, draw=none, from=1-2, to=0] + \arrow["{H^r_{m,n}}"{description, pos=0.3}, draw=none, from=1-5, to=1] +\end{tikzcd}} + }} + Along with the various usual axioms of a bimodule, we have added the assumption that #{H^\ell_{m,n}} be invertible. + As an abuse of notation, probably justified by a coherence theorem if pressed, we shall write #{H^\ell_{m,n}} as an identity. + This leads to several reductions of structure, as follows:} +\ol{ + \li{First note that setting #{H^\ell} to the identity makes no sense unless we also assume that #{H(mn)=H(n)} + for all composable pairs #{m,n} of proarrows in \dbl{D}. In particular, #{H(m)=H(m\id_y)=H(\id_y)}, using strictness of \dbl{D}. + This means we can forget about + #{H(n)} except in case #{n=\id_x} for some object #{x} of \dbl{D}. We therefore shift notation and write #{H(x)} for #{H(\id_x)}.} + + + \li{Similarly, consider the condition of naturality of left actions, which says that given horizontally composable cells in \dbl{D}, we have the equality below: + \quiver{% https://q.uiver.app/#q=WzAsMjIsWzIsMCwieCJdLFszLDAsInkiXSxbMiwxLCJ4JyJdLFszLDEsInknIl0sWzQsMCwieiJdLFs0LDEsInonIl0sWzMsMywiPSJdLFswLDIsIjF4Il0sWzEsMiwiMXkiXSxbMiwyLCJYeiJdLFswLDMsIjF4JyJdLFsxLDMsIjF5JyJdLFsyLDMsIlh6JyJdLFswLDQsIjF4JyJdLFsyLDQsIlh6JyJdLFs0LDIsIjF4Il0sWzUsMiwiMXkiXSxbNiwyLCJYeiJdLFs0LDMsIjF4Il0sWzYsMywiWHoiXSxbNCw0LCIxeCciXSxbNiw0LCJYeiciXSxbMCwyLCJmIiwyXSxbMSwzLCJnIiwxXSxbMCwxLCJtIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzIsMywibSciLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSw0LCJuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzQsNSwiaCJdLFszLDUsIm4nIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzcsMTAsIjFmIiwyXSxbOSwxMiwiWGgiXSxbMTAsMTEsIjFtJyIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxMSwxMiwiSG4nIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzgsMTEsIjFnIiwxXSxbNyw4LCIxbSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs4LDksIkhuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEzLDE0LCJIKG0nbicpIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzE4LDIwLCIxZiIsMV0sWzE5LDIxLCJYaCIsMV0sWzIwLDIxLCJIKG0nbicpIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzE4LDE5LCJIKG1uKSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxNSwxNiwiMW0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTYsMTcsIkhuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEwLDEzLCIiLDEseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxMiwxNCwiIiwxLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMTUsMTgsIiIsMSx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzE3LDE5LCIiLDEseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyNCwyNSwiXFxhbHBoYSIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyNiwyOCwiXFxiZXRhIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzQwLDM5LCJIKFxcYWxwaGFcXGJldGEpIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzE2LDQwLCJIXlxcZWxsX3ttLG59IiwxLHsic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzExLDM2LCJIXlxcZWxsX3ttJyxuJ30iLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMzUsMzIsIkhcXGJldGEiLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMzQsMzEsIjFcXGFscGhhIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d +\begin{tikzcd} + && x & y & z \\ + && {x'} & {y'} & {z'} \\ + 1x & 1y & Xz && 1x & 1y & Xz \\ + {1x'} & {1y'} & {Xz'} & {=} & 1x && Xz \\ + {1x'} && {Xz'} && {1x'} && {Xz'} + \arrow[""{name=0, anchor=center, inner sep=0}, "m", "\shortmid"{marking}, from=1-3, to=1-4] + \arrow["f"', from=1-3, to=2-3] + \arrow[""{name=1, anchor=center, inner sep=0}, "n", "\shortmid"{marking}, from=1-4, to=1-5] + \arrow["g"{description}, from=1-4, to=2-4] + \arrow["h", from=1-5, to=2-5] + \arrow[""{name=2, anchor=center, inner sep=0}, "{m'}"', "\shortmid"{marking}, from=2-3, to=2-4] + \arrow[""{name=3, anchor=center, inner sep=0}, "{n'}"', "\shortmid"{marking}, from=2-4, to=2-5] + \arrow[""{name=4, anchor=center, inner sep=0}, "1m", "\shortmid"{marking}, from=3-1, to=3-2] + \arrow["1f"', from=3-1, to=4-1] + \arrow[""{name=5, anchor=center, inner sep=0}, "Hn", "\shortmid"{marking}, from=3-2, to=3-3] + \arrow["1g"{description}, from=3-2, to=4-2] + \arrow["Xh", from=3-3, to=4-3] + \arrow["1m", "\shortmid"{marking}, from=3-5, to=3-6] + \arrow[Rightarrow, no head, from=3-5, to=4-5] + \arrow["Hn", "\shortmid"{marking}, from=3-6, to=3-7] + \arrow[Rightarrow, no head, from=3-7, to=4-7] + \arrow[""{name=6, anchor=center, inner sep=0}, "{1m'}"', "\shortmid"{marking}, from=4-1, to=4-2] + \arrow[Rightarrow, no head, from=4-1, to=5-1] + \arrow[""{name=7, anchor=center, inner sep=0}, "{Hn'}"', "\shortmid"{marking}, from=4-2, to=4-3] + \arrow[Rightarrow, no head, from=4-3, to=5-3] + \arrow[""{name=8, anchor=center, inner sep=0}, "{H(mn)}"', "\shortmid"{marking}, from=4-5, to=4-7] + \arrow["1f"{description}, from=4-5, to=5-5] + \arrow["Xh"{description}, from=4-7, to=5-7] + \arrow[""{name=9, anchor=center, inner sep=0}, "{H(m'n')}"', "\shortmid"{marking}, from=5-1, to=5-3] + \arrow[""{name=10, anchor=center, inner sep=0}, "{H(m'n')}"', "\shortmid"{marking}, from=5-5, to=5-7] + \arrow["\alpha"{description}, draw=none, from=0, to=2] + \arrow["\beta"{description}, draw=none, from=1, to=3] + \arrow["{1\alpha}"{description}, draw=none, from=4, to=6] + \arrow["{H\beta}"{description}, draw=none, from=5, to=7] + \arrow["{H^\ell_{m,n}}"{description}, draw=none, from=3-6, to=8] + \arrow["{H^\ell_{m',n'}}"{description}, draw=none, from=4-2, to=9] + \arrow["{H(\alpha\beta)}"{description}, draw=none, from=8, to=10] +\end{tikzcd}} + Since #{1\alpha} and the #{H^\ell}s are all identities, this amounts to the condition that #{H\beta=H(\alpha\beta)} and in particular, #{H\alpha=H(\id_g)}. + We can again thus forget about #{H\alpha} except in the case #{\alpha=\id_f} for a tight morphism #{f}. + We therefore again shift notation and write #{H(f)} for #{H(\id_f)}. + } + + \li{Third, consider the compatibility of left and right actions, which says that the following equation holds for the triple #{w\xproto{m} x\xproto{n} y \xproto{p} z}:} + \quiver{ % https://q.uiver.app/#q=WzAsMTksWzAsMCwiMXgiXSxbMCwxLCIxeCJdLFswLDIsIjF4Il0sWzEsMCwiMXkiXSxbMiwwLCJYeSJdLFszLDAsIlh6Il0sWzMsMSwiWHoiXSxbMywyLCJYeiJdLFsyLDEsIlh5Il0sWzUsMCwiMXgiXSxbNSwxLCIxeCJdLFs1LDIsIjF4Il0sWzYsMCwiMXkiXSxbNywwLCJYeSJdLFs4LDAsIlh6Il0sWzgsMSwiWHoiXSxbOCwyLCJYeiJdLFs2LDEsIjF5Il0sWzQsMSwiPSJdLFswLDEsIj0iLDFdLFsxLDIsIj0iLDFdLFswLDMsIkZtIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzMsNCwiSHkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNCw1LCJYcCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs1LDYsIj0iLDFdLFs2LDcsIj0iLDFdLFs0LDgsIj0iLDFdLFs4LDYsIlhwIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEsOCwiSG09SHkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMiw3LCJIKG1wKT1IeiIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs5LDEwLCI9IiwxXSxbMTAsMTEsIj0iLDFdLFsxNCwxNSwiPSIsMV0sWzE1LDE2LCI9IiwxXSxbMTEsMTYsIkgoXFxpZF95cCk9SHoiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTIsMTcsIj0iLDFdLFsxNywxNSwiSHA9SHoiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbOSwxMiwiRm0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTIsMTMsIkh5IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEzLDE0LCJYcCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxMCwxNywiRm0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMjMsMjcsIlxcaWRfe1hfcH0iLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMywyOCwiSF5cXGVsbF97bSx5fSIsMSx7ImxhYmVsX3Bvc2l0aW9uIjo0MCwic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzgsMjksIkhecl97bVxcaWRfeSxwfT1IXnJfe20scH0iLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMTMsMzYsIkhecl97eSxwfSIsMSx7ImxhYmVsX3Bvc2l0aW9uIjo0MCwic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzM3LDQwLCJcXGlkX3tGbX0iLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMTcsMzQsIkheXFxlbGxfe20sXFxpZF95cH0iLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0= + \begin{tikzcd} + 1w & 1x & Xy & Xz && 1w & 1x & Xy & Xz \\ + 1w && Xy & Xz & {=} & 1w & 1x && Xz \\ + 1x &&& Xz && 1x &&& Xz + \arrow["1m", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["{=}"{description}, from=1-1, to=2-1] + \arrow["Hy", "\shortmid"{marking}, from=1-2, to=1-3] + \arrow[""{name=0, anchor=center, inner sep=0}, "Xp", "\shortmid"{marking}, from=1-3, to=1-4] + \arrow["{=}"{description}, from=1-3, to=2-3] + \arrow["{=}"{description}, from=1-4, to=2-4] + \arrow[""{name=1, anchor=center, inner sep=0}, "Fm", "\shortmid"{marking}, from=1-6, to=1-7] + \arrow["{=}"{description}, from=1-6, to=2-6] + \arrow["Hy", "\shortmid"{marking}, from=1-7, to=1-8] + \arrow["{=}"{description}, from=1-7, to=2-7] + \arrow["Xp", "\shortmid"{marking}, from=1-8, to=1-9] + \arrow["{=}"{description}, from=1-9, to=2-9] + \arrow[""{name=2, anchor=center, inner sep=0}, "{Hy}", "\shortmid"{marking}, from=2-1, to=2-3] + \arrow["{=}"{description}, from=2-1, to=3-1] + \arrow[""{name=3, anchor=center, inner sep=0}, "Xp", "\shortmid"{marking}, from=2-3, to=2-4] + \arrow["{=}"{description}, from=2-4, to=3-4] + \arrow[""{name=4, anchor=center, inner sep=0}, "Fm", "\shortmid"{marking}, from=2-6, to=2-7] + \arrow["{=}"{description}, from=2-6, to=3-6] + \arrow[""{name=5, anchor=center, inner sep=0}, "{Hz}", "\shortmid"{marking}, from=2-7, to=2-9] + \arrow["{=}"{description}, from=2-9, to=3-9] + \arrow[""{name=6, anchor=center, inner sep=0}, "{Hz}"', "\shortmid"{marking}, from=3-1, to=3-4] + \arrow[""{name=7, anchor=center, inner sep=0}, "{Hz}"', "\shortmid"{marking}, from=3-6, to=3-9] + \arrow["{H^\ell_{m,n}}"{description, pos=0.4}, draw=none, from=1-2, to=2] + \arrow["{\id_{X_p}}"{description}, draw=none, from=0, to=3] + \arrow["{\id_{Fm}}"{description}, draw=none, from=1, to=4] + \arrow["{H^r_{n,p}}"{description, pos=0.4}, draw=none, from=1-8, to=5] + \arrow["{H^r_{mn,p}}"{description}, draw=none, from=2-3, to=6] + \arrow["{H^\ell_{m,np}}"{description}, draw=none, from=2-7, to=7] + \end{tikzcd}} + \p{Since the #{H^\ell} are identities by assumption, this amounts to the condition that #{H^r_{mn,p}=H^r_{n,p}}. + In particular, #{H^r_{m,n}=H^r_{\id_y,n}} so that we may simply write #{Hn=H^r_{\id_y,n}} and forget about the other action cells.} +} + \p{This reduces the material of an instance as follows.} +} % end explication subtree + +\subtree{ + \title{Unpacked instances} + \taxon{definition} + \p{An \define{unpacked instance} #{H} of a model #{X:\dbl{D}\to\dbl{E}} of a double theory is given by} + \ul{ + \li{For each object #{x} of \dbl{D}, a proarrow #{Hx:1\proto Xx} in \dbl{E}.} + \li{For each tight morphism #{f:x\to y} of \dbl{D}, a cell of \dbl{E} as below: + \quiver{% https://q.uiver.app/#q=WzAsNCxbMCwwLCIxIl0sWzAsMSwiMSJdLFsxLDAsIlh4Il0sWzEsMSwiWHkiXSxbMCwxLCI9IiwxXSxbMCwyLCJIeCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsyLDMsIlhmIl0sWzEsMywiSHkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNSw3LCJIZiIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ== + \begin{tikzcd} + 1 & Xx \\ + 1 & Xy + \arrow[""{name=0, anchor=center, inner sep=0}, "Hx", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["{=}"{description}, from=1-1, to=2-1] + \arrow["Xf", from=1-2, to=2-2] + \arrow[""{name=1, anchor=center, inner sep=0}, "Hy", "\shortmid"{marking}, from=2-1, to=2-2] + \arrow["Hf"{description}, draw=none, from=0, to=1] + \end{tikzcd}} + } + \li{For each proarrow #{m:x\proto y} of \dbl{D}, an action cell as below: + \quiver{% https://q.uiver.app/#q=WzAsNSxbMCwwLCIxIl0sWzEsMCwiWHgiXSxbMiwwLCJYeSJdLFswLDEsIjEiXSxbMiwxLCJYeSJdLFswLDEsIkh4IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEsMiwiWG0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMCwzLCI9IiwxXSxbMiw0LCI9IiwxXSxbMyw0LCJIeSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxLDksIkhtIiwxLHsic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d + \begin{tikzcd} + 1 & Xx & Xy \\ + 1 && Xy + \arrow["Hx", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["{=}"{description}, from=1-1, to=2-1] + \arrow["Xm", "\shortmid"{marking}, from=1-2, to=1-3] + \arrow["{=}"{description}, from=1-3, to=2-3] + \arrow[""{name=0, anchor=center, inner sep=0}, "Hy"', "\shortmid"{marking}, from=2-1, to=2-3] + \arrow["Hm"{description}, draw=none, from=1-2, to=0] + \end{tikzcd}} + } + } + \p{These data are required to satisfy the following conditions:} + \ul{ + \li{Functoriality on arrows: #{H(f)H(g)=H(fg),H(\id_x)=\id_{Hx}.} + \li{Naturality of actions: + % https://q.uiver.app/#q=WzAsMjIsWzMsMCwieSJdLFszLDEsInknIl0sWzQsMCwieiJdLFs0LDEsInonIl0sWzMsMywiPSJdLFswLDIsIjF4Il0sWzEsMiwiWHkiXSxbMiwyLCJYeiJdLFswLDMsIjF4JyJdLFsxLDMsIlh5JyJdLFsyLDMsIlh6JyJdLFswLDQsIjF4JyJdLFsyLDQsIlh6JyJdLFs0LDIsIjF4Il0sWzUsMiwiWHkiXSxbNiwyLCJYeiJdLFs0LDMsIjF4Il0sWzYsMywiWHoiXSxbNCw0LCIxeCciXSxbNiw0LCJYeiciXSxbMiwxLCJ4JyJdLFsyLDAsIngiXSxbMCwxLCJnIiwxXSxbMCwyLCJtJyIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsyLDMsImgiXSxbMSwzLCJuJyIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs1LDgsIjFmIiwyXSxbOCwxMSwiPSIsMV0sWzcsMTAsIlhoIl0sWzEwLDEyLCI9IiwxXSxbOCw5LCJIeSciLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbOSwxMCwiWG4nIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzYsOSwiWGciLDFdLFs1LDYsIkh5IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzYsNywiWG4iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTEsMTIsIkh6JyIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxMywxNiwiPSIsMV0sWzE2LDE4LCIxZiIsMV0sWzE1LDE3LCI9IiwxXSxbMTcsMTksIlhoIiwxXSxbMTgsMTksIkh6JyIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxNiwxNywiSHoiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTMsMTQsIkh5IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzE0LDE1LCJYbiIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsyMCwxLCJuIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzIxLDIwLCJmIiwyXSxbMjEsMCwibSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsyMywyNSwiXFxiZXRhIiwxLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzQxLDQwLCJIaCIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxNCw0MSwiSG4iLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbOSwzNSwiSChtJ24nKSIsMSx7InNob3J0ZW4iOnsidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszNCwzMSwiWFxcYmV0YSIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszMywzMCwiSGciLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNDYsNDQsIlxcYWxwaGEiLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0= + \quiver{\begin{tikzcd} + && x & y & z \\ + && {x'} & {y'} & {z'} \\ + 1x & Xy & Xz && 1x & Xy & Xz \\ + {1x'} & {Xy'} & {Xz'} & {=} & 1x && Xz \\ + {1x'} && {Xz'} && {1x'} && {Xz'} + \arrow[""{name=0, anchor=center, inner sep=0}, "m", "\shortmid"{marking}, from=1-3, to=1-4] + \arrow["f"', from=1-3, to=2-3] + \arrow[""{name=1, anchor=center, inner sep=0}, "n", "\shortmid"{marking}, from=1-4, to=1-5] + \arrow["g"{description}, from=1-4, to=2-4] + \arrow["h", from=1-5, to=2-5] + \arrow[""{name=2, anchor=center, inner sep=0}, "{m'}"', "\shortmid"{marking}, from=2-3, to=2-4] + \arrow[""{name=3, anchor=center, inner sep=0}, "{n'}"', "\shortmid"{marking}, from=2-4, to=2-5] + \arrow[""{name=4, anchor=center, inner sep=0}, "Hy", "\shortmid"{marking}, from=3-1, to=3-2] + \arrow["1f"', from=3-1, to=4-1] + \arrow[""{name=5, anchor=center, inner sep=0}, "Xn", "\shortmid"{marking}, from=3-2, to=3-3] + \arrow["Xg"{description}, from=3-2, to=4-2] + \arrow["Xh", from=3-3, to=4-3] + \arrow["Hy", "\shortmid"{marking}, from=3-5, to=3-6] + \arrow["{=}"{description}, from=3-5, to=4-5] + \arrow["Xn", "\shortmid"{marking}, from=3-6, to=3-7] + \arrow["{=}"{description}, from=3-7, to=4-7] + \arrow[""{name=6, anchor=center, inner sep=0}, "{Hy'}"', "\shortmid"{marking}, from=4-1, to=4-2] + \arrow["{=}"{description}, from=4-1, to=5-1] + \arrow[""{name=7, anchor=center, inner sep=0}, "{Xn'}"', "\shortmid"{marking}, from=4-2, to=4-3] + \arrow["{=}"{description}, from=4-3, to=5-3] + \arrow[""{name=8, anchor=center, inner sep=0}, "Hz"', "\shortmid"{marking}, from=4-5, to=4-7] + \arrow["1f"{description}, from=4-5, to=5-5] + \arrow["Xh"{description}, from=4-7, to=5-7] + \arrow[""{name=9, anchor=center, inner sep=0}, "{Hz'}"', "\shortmid"{marking}, from=5-1, to=5-3] + \arrow[""{name=10, anchor=center, inner sep=0}, "{Hz'}"', "\shortmid"{marking}, from=5-5, to=5-7] + \arrow["\alpha"{description}, draw=none, from=0, to=2] + \arrow["\beta"{description}, draw=none, from=1, to=3] + \arrow["Hg"{description}, draw=none, from=4, to=6] + \arrow["{X\beta}"{description}, draw=none, from=5, to=7] + \arrow["Hn"{description}, draw=none, from=3-6, to=8] + \arrow["{H(n')}"{description}, draw=none, from=4-2, to=9] + \arrow["Hh"{description}, draw=none, from=8, to=10] + \end{tikzcd}}} + + \li{Associativity of actions: + % https://q.uiver.app/#q=WzAsMjIsWzMsMCwieCJdLFs0LDAsInkiXSxbNSwwLCJ6Il0sWzAsMSwiMXgiXSxbMSwxLCJYeCJdLFsyLDEsIlh5Il0sWzMsMSwiWHoiXSxbMCwyLCIxeCJdLFsyLDIsIlh5Il0sWzMsMiwiWHoiXSxbMCwzLCIxeCJdLFszLDMsIlh6Il0sWzQsMiwiPSJdLFs1LDEsIjF4Il0sWzUsMiwiMXgiXSxbNSwzLCIxeCJdLFs2LDEsIlh4Il0sWzcsMSwiWHkiXSxbOCwxLCJYeiJdLFs2LDIsIlh4Il0sWzgsMiwiWHoiXSxbOCwzLCJYeiJdLFszLDcsIj0iLDFdLFs3LDEwLCI9IiwxXSxbNSw4LCI9IiwxXSxbNiw5LCI9IiwxXSxbOSwxMSwiPSIsMV0sWzEzLDE0LCI9IiwxXSxbMTQsMTUsIj0iLDFdLFsxNiwxOSwiPSIsMV0sWzE4LDIwLCI9IiwxXSxbMjAsMjEsIj0iLDFdLFswLDEsIm0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSwyLCJuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzMsNCwiSHgiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNCw1LCJYbSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs1LDYsIlhuIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzcsOCwiSHkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbOCw5LCJYbiIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxMCwxMSwiSHoiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTMsMTYsIkh4IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzE2LDE3LCJYbSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxNywxOCwiWG4iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTQsMTksIkh4IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzE5LDIwLCJYKG1uKSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxNSwyMSwiSHoiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMTcsNDQsIlhfe20sbn0iLDEseyJsYWJlbF9wb3NpdGlvbiI6MzAsInNob3J0ZW4iOnsidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs0NCw0NSwiSChtbikiLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNCwzNywiSG0iLDEseyJsYWJlbF9wb3NpdGlvbiI6NDAsInNob3J0ZW4iOnsidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszOCwzOSwiSG4iLDEseyJsYWJlbF9wb3NpdGlvbiI6NzAsIm9mZnNldCI6NSwic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d + \quiver{\begin{tikzcd} + &&& x & y & z \\ + 1x & Xx & Xy & Xz && 1x & Xx & Xy & Xz \\ + 1x && Xy & Xz & {=} & 1x & Xx && Xz \\ + 1x &&& Xz && 1x &&& Xz + \arrow["m", "\shortmid"{marking}, from=1-4, to=1-5] + \arrow["n", "\shortmid"{marking}, from=1-5, to=1-6] + \arrow["Hx", "\shortmid"{marking}, from=2-1, to=2-2] + \arrow["{=}"{description}, from=2-1, to=3-1] + \arrow["Xm", "\shortmid"{marking}, from=2-2, to=2-3] + \arrow["Xn", "\shortmid"{marking}, from=2-3, to=2-4] + \arrow["{=}"{description}, from=2-3, to=3-3] + \arrow["{=}"{description}, from=2-4, to=3-4] + \arrow["Hx", "\shortmid"{marking}, from=2-6, to=2-7] + \arrow["{=}"{description}, from=2-6, to=3-6] + \arrow["Xm", "\shortmid"{marking}, from=2-7, to=2-8] + \arrow["{=}"{description}, from=2-7, to=3-7] + \arrow["Xn", "\shortmid"{marking}, from=2-8, to=2-9] + \arrow["{=}"{description}, from=2-9, to=3-9] + \arrow[""{name=0, anchor=center, inner sep=0}, "Hy", "\shortmid"{marking}, from=3-1, to=3-3] + \arrow["{=}"{description}, from=3-1, to=4-1] + \arrow[""{name=1, anchor=center, inner sep=0}, "Xn", "\shortmid"{marking}, from=3-3, to=3-4] + \arrow["{=}"{description}, from=3-4, to=4-4] + \arrow["Hx", "\shortmid"{marking}, from=3-6, to=3-7] + \arrow["{=}"{description}, from=3-6, to=4-6] + \arrow[""{name=2, anchor=center, inner sep=0}, "{X(mn)}", "\shortmid"{marking}, from=3-7, to=3-9] + \arrow["{=}"{description}, from=3-9, to=4-9] + \arrow[""{name=3, anchor=center, inner sep=0}, "Hz", "\shortmid"{marking}, from=4-1, to=4-4] + \arrow[""{name=4, anchor=center, inner sep=0}, "Hz", "\shortmid"{marking}, from=4-6, to=4-9] + \arrow["Hm"{description, pos=0.4}, draw=none, from=2-2, to=0] + \arrow["{X_{m,n}}"{description, pos=0.3}, draw=none, from=2-8, to=2] + \arrow["Hn"{description, pos=0.7}, shift right=5, draw=none, from=1, to=3] + \arrow["{H(mn)}"{description}, draw=none, from=2, to=4] + \end{tikzcd}}} + + \li{Unitality of actions: % https://q.uiver.app/#q=WzAsMTMsWzAsMCwiMXgiXSxbMCwxLCIxeCJdLFswLDIsIjF4Il0sWzEsMCwiWHgiXSxbMSwxLCJYeCJdLFsyLDAsIlh4Il0sWzIsMSwiWHgiXSxbMiwyLCJYeCJdLFszLDEsIj0iXSxbNCwwLCIxeCJdLFs0LDIsIjF4Il0sWzYsMCwiWHgiXSxbNiwyLCJYeCJdLFswLDEsIj0iLDFdLFsxLDIsIj0iLDFdLFszLDQsIj0iLDFdLFs1LDYsIj0iLDFdLFs2LDcsIj0iLDFdLFs5LDEwLCI9IiwxXSxbMTEsMTIsIj0iLDFdLFswLDMsIkh4IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzMsNSwiXFxpZF97WHh9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiYmFycmVkIn19fV0sWzEsNCwiSHgiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNCw2LCJYKFxcaWRfeCkiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMiw3LCJIeCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFs5LDExLCJIeCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsxMCwxMiwiSHgiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbNCwyNCwiSChcXGlkX3gpIiwxLHsibGFiZWxfcG9zaXRpb24iOjMwLCJzaG9ydGVuIjp7InRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMjEsMjMsIlhfeCIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ== + \quiver{\begin{tikzcd} + 1x & Xx & Xx && 1x && Xx \\ + 1x & Xx & Xx & {=} \\ + 1x && Xx && 1x && Xx + \arrow["Hx", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["{=}"{description}, from=1-1, to=2-1] + \arrow[""{name=0, anchor=center, inner sep=0}, "{\id_{Xx}}", "\shortmid"{marking}, from=1-2, to=1-3] + \arrow["{=}"{description}, from=1-2, to=2-2] + \arrow["{=}"{description}, from=1-3, to=2-3] + \arrow["Hx", "\shortmid"{marking}, from=1-5, to=1-7] + \arrow["{=}"{description}, from=1-5, to=3-5] + \arrow["{=}"{description}, from=1-7, to=3-7] + \arrow["Hx", "\shortmid"{marking}, from=2-1, to=2-2] + \arrow["{=}"{description}, from=2-1, to=3-1] + \arrow[""{name=1, anchor=center, inner sep=0}, "{X(\id_x)}", "\shortmid"{marking}, from=2-2, to=2-3] + \arrow["{=}"{description}, from=2-3, to=3-3] + \arrow[""{name=2, anchor=center, inner sep=0}, "Hx", "\shortmid"{marking}, from=3-1, to=3-3] + \arrow["Hx", "\shortmid"{marking}, from=3-5, to=3-7] + \arrow["{X_x}"{description}, draw=none, from=0, to=1] + \arrow["{H(\id_x)}"{description, pos=0.3}, draw=none, from=2-2, to=2] + \end{tikzcd}}} + } + } +} %end unpacked subtree + + +\subtree{ + \title{Instances of multicategories} + \taxon{example} + \p{An instance of a multicategory #{M}, viewed as a model of the [theory of promonoids](thy-000A) + in \Span, is a multifunctor #{M\to \Set}, because the invertibility of the action cells + means every heteromorphism span #{H_n:1^m\proto M_0} is isomorphic, and we can consider just + the unary heteromorphisms with their right action by #{M}; this is precisely a multifunctor. + Similarly, a co-instance over a multicategory is a multifunctor #{M^\op\to \Set}, noting + that #{M^\op} is not in fact a multi- but a co-multicategory.} +} + +\subtree{ + \title{Instances of categories} + \taxon{example} + \p{As has been suggested, an instance of a model of the terminal double theory is +a co-presheaf; respectively, a co-instance is a presheaf. Note that these are the same as bimodules from and to #{1} +in this case, as is true whenever the double theory being modeled lacks nontrivial proarrows.} +} + +\subtree{ + \title{Instances profunctors} + \taxon{example} +\p{For an example intermediate in complexity, consider the [theory of a proarrow](thy-0006). A bimodule +#{M:H\proTo K} looks like this: +\quiver{ + % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzEsMCwiWSJdLFswLDEsIloiXSxbMSwxLCJXIl0sWzAsMSwiSCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImJhcnJlZCJ9fX1dLFsyLDMsIksiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMCwyLCIiLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSwzLCIiLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMCwzLCIiLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJiYXJyZWQifX19XSxbMSw4LCIiLDEseyJzaG9ydGVuIjp7InRhcmdldCI6MjB9fV0sWzIsOCwiIiwxLHsic2hvcnRlbiI6eyJ0YXJnZXQiOjIwfX1dXQ== + \begin{tikzcd} + X & Y \\ + Z & W + \arrow["H", "\shortmid"{marking}, from=1-1, to=1-2] + \arrow["\shortmid"{marking}, from=1-1, to=2-1] + \arrow[""{name=0, anchor=center, inner sep=0}, "\shortmid"{marking}, from=1-1, to=2-2] + \arrow["\shortmid"{marking}, from=1-2, to=2-2] + \arrow["K", "\shortmid"{marking}, from=2-1, to=2-2] + \arrow[shorten >=2pt, Rightarrow, from=1-2, to=0] + \arrow[shorten >=2pt, Rightarrow, from=2-1, to=0] + \end{tikzcd} +} +If #{H=1} is trivial, then such a bimodule is a profunctor #{K:Z\proto W} together with +copresheaves #{Z',W'} on #{Z} and on #{W} and a morphism #{Z'K\To W'}, \em{plus} a mysterious endomorphism of #{W'}. +An instance of #{K} throws away precisely this unwanted endomorphism, +making an instance of #{K} into precisely a pair of instances of #{Z} and #{W} on which #{K} acts on either side, +which seems to be the right notion in this case.} +} + +\subtree{ + \title{Modules over monoidal categories} + \taxon{example} + \p{\strong{TODO}} +} + + +\subtree{ + \taxon{remark} + \p{There should be some sense in which the category of instances is the coslice of bimodules under #{1}. + Considering [Lambert & Patterson 2024](cartesian-double-theories-2024), Theory 6.3 and Theory 6.12, + it might be best to take this coslice at the \em{theory} level.} +} + diff --git a/dev-docs/trees/dct-000A.tree b/dev-docs/trees/dct-000A.tree new file mode 100644 index 000000000..ae516d1a4 --- /dev/null +++ b/dev-docs/trees/dct-000A.tree @@ -0,0 +1,13 @@ +\title{Multicategories} +\taxon{doctrine} +\import{macros} + +\p{A \nlab{multicategory}, also known as a \em{colored} or \em{typed operad}, is +a model of the following double theory.} + +\transclude{thy-000A} + +\p{A model #{M} of the theory of promonoids maps the object #{x} to the object +set #{M_0 \coloneqq M(x)} of the multicategory and maps the proarrow #{\mu_n} to +the span #{M_0^n\proto M_0} whose preimage at #{((x_i)_1^n,y)} is the set of +multimorphisms #{(x_i)_1^n \to y}.} diff --git a/dev-docs/trees/dev-0001.tree b/dev-docs/trees/dev-0001.tree index 93042f0ea..8308538a8 100644 --- a/dev-docs/trees/dev-0001.tree +++ b/dev-docs/trees/dev-0001.tree @@ -28,7 +28,7 @@ } \ul{ -\li{Additional doctrines: [[dct-0008]], [[dct-0009]]} +\li{Additional doctrines: [[dct-0008]], [[dct-0009]], [[dct-000A]]} \li{Mathematical background: [[dbl-0001]]} \li{[[bib-0001]]} } diff --git a/dev-docs/trees/macros.tree b/dev-docs/trees/macros.tree index b34128841..88c72d5b0 100644 --- a/dev-docs/trees/macros.tree +++ b/dev-docs/trees/macros.tree @@ -74,6 +74,9 @@ % Double category theory \def\proto{#{\mathrel{\mkern3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}}} +\def\xproto[label]{#{\overset{\label}{\proto}}} +\def\proTo{#{\mathrel{\mkern3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\Rightarrow}}}} + \def\tabulator[ob]{#{\top\ob}} diff --git a/dev-docs/trees/acsets-2022.tree b/dev-docs/trees/refs/acsets-2022.tree similarity index 100% rename from dev-docs/trees/acsets-2022.tree rename to dev-docs/trees/refs/acsets-2022.tree diff --git a/dev-docs/trees/refs/pisani-2024.tree b/dev-docs/trees/refs/pisani-2024.tree new file mode 100644 index 000000000..544574bac --- /dev/null +++ b/dev-docs/trees/refs/pisani-2024.tree @@ -0,0 +1,6 @@ +\title{Unbiased multicategory theory} +\author{Claudio Pisani} +\date{2024} +\taxon{reference} +\meta{doi}{10.48550/arXiv.2409.10150} +\meta{arxiv}{2409.10150} diff --git a/dev-docs/trees/thy-000A.tree b/dev-docs/trees/thy-000A.tree new file mode 100644 index 000000000..01108b8e6 --- /dev/null +++ b/dev-docs/trees/thy-000A.tree @@ -0,0 +1,15 @@ +\title{Promonoids} +\taxon{theory} +\import{macros} + +\p{The \define{theory of promonoids} #{\mathbb{T}_{\mathrm{pm}}} is the cartesian double theory generated by an object #{x} +equipped with proarrows #{\mu_2:x^2 \proto x,\mu_0:x^0\proto x}, subject to associativity and unitality conditions. In other words, there is a unique counary proarrow #{\mu_n:x^n \proto x} for every #{n \geq 0}. See ([Lambert & +Patterson 2024](cartesian-double-theories-2024), Theory 6.9).} + +\p{Arbitrary proarrows #{p:x^m\proto x^n} must then be a product of #{n} proarrows +#{\mu_{m_i}:x^{m_i}\proto x} for some partition #{m=m_1+\cdots +m_n} of #{m}. Thus the loose +category of #{\mathbb{T}_{\mathrm{pm}}} is the \nlab{augmented simplex category}, the category +of totally-ordered, possibly-empty finite sets and order-preserving maps between them. This +phenomenon is familiar from the fact that the augmented simplicial category is itself the +strict monoidal category freely generated by a monoid object. Compare [Pisani 2024](pisani-2024) for a theory of multicategories in which the proarrows are instead maps of sets with orders +on the fibers only, for better comparison with symmetric multicategories.} diff --git a/packages/frontend/package.json b/packages/frontend/package.json index be0c9263d..ca0800b78 100644 --- a/packages/frontend/package.json +++ b/packages/frontend/package.json @@ -36,6 +36,7 @@ "@viz-js/viz": "^3.7.0", "backend": "workspace:*", "catlog-wasm": "link:../catlog-wasm/pkg", + "computed-style-to-inline-style": "^4.0.0", "echarts": "^5.5.1", "echarts-solid": "^0.2.0", "lucide-solid": "^0.435.0", @@ -45,6 +46,7 @@ "prosemirror-state": "^1.4.3", "prosemirror-view": "^1.33.8", "solid-js": "^1.9.2", + "svg2png-wasm": "^1.4.1", "tiny-invariant": "^1.3.3", "ts-pattern": "^5.2.0", "uuid": "^10.0.0", diff --git a/packages/frontend/pnpm-lock.yaml b/packages/frontend/pnpm-lock.yaml index f742c886e..781d6206c 100644 --- a/packages/frontend/pnpm-lock.yaml +++ b/packages/frontend/pnpm-lock.yaml @@ -71,6 +71,9 @@ importers: catlog-wasm: specifier: link:../catlog-wasm/pkg version: link:../catlog-wasm/pkg + computed-style-to-inline-style: + specifier: ^4.0.0 + version: 4.0.0 echarts: specifier: ^5.5.1 version: 5.5.1 @@ -98,6 +101,9 @@ importers: solid-js: specifier: ^1.9.2 version: 1.9.2 + svg2png-wasm: + specifier: ^1.4.1 + version: 1.4.1 tiny-invariant: specifier: ^1.3.3 version: 1.3.3 @@ -1253,6 +1259,9 @@ packages: comma-separated-tokens@2.0.3: resolution: {integrity: sha512-Fu4hJdvzeylCfQPp9SGWidpzrMs7tTrlu6Vb8XGaRGck8QSNZJJp538Wrb60Lax4fPwR64ViY468OIUTbRlGZg==} + computed-style-to-inline-style@4.0.0: + resolution: {integrity: sha512-PwVJVqD1SZnDVbEJrshRARbKUq9JG2SlkkEY8NacLpRz98FemLfdZw3vjHndjP5gHvOruxg6Ywhcs2kqD2EmEw==} + concat-map@0.0.1: resolution: {integrity: sha512-/Srv4dswyQNBfohGpz9o6Yb3Gz3SrUDqBH5rTuhGR7ahtlbYKnVxw2bCFMRljaA7EXHaXZ8wsHdodFvbkhKmqg==} @@ -2103,6 +2112,9 @@ packages: resolution: {integrity: sha512-ot0WnXS9fgdkgIcePe6RHNk1WA8+muPa6cSjeR3V8K27q9BB1rTE3R1p7Hv0z1ZyAc8s6Vvv8DIyWf681MAt0w==} engines: {node: '>= 0.4'} + svg2png-wasm@1.4.1: + resolution: {integrity: sha512-ZFy1NtwZVAsslaTQoI+/QqX2sg0vjmgJ/jGAuLZZvYcRlndI54hLPiwLC9JzXlFBerfxN5JiS7kpEUG0mrXS3Q==} + tar@6.2.1: resolution: {integrity: sha512-DZ4yORTwrbTj/7MZYq2w+/ZFdI6OZ/f9SFHR+71gIVUZhOQPHzVCLpvRnPgyaMpfWxxk/4ONva3GQSyNIKRv6A==} engines: {node: '>=10'} @@ -3451,6 +3463,8 @@ snapshots: comma-separated-tokens@2.0.3: {} + computed-style-to-inline-style@4.0.0: {} + concat-map@0.0.1: {} convert-source-map@2.0.0: {} @@ -4587,6 +4601,8 @@ snapshots: supports-preserve-symlinks-flag@1.0.0: {} + svg2png-wasm@1.4.1: {} + tar@6.2.1: dependencies: chownr: 2.0.0 diff --git a/packages/frontend/src/document/analysis_document_editor.tsx b/packages/frontend/src/document/analysis_document_editor.tsx index 6944d24cb..c7b129ae1 100644 --- a/packages/frontend/src/document/analysis_document_editor.tsx +++ b/packages/frontend/src/document/analysis_document_editor.tsx @@ -29,8 +29,10 @@ import type { ModelAnalysisMeta } from "../theory"; import { type LiveModelDocument, ModelPane, enlivenModelDocument } from "./model_document_editor"; import type { AnalysisDocument, ModelDocument } from "./types"; +import { Download } from "lucide-solid"; import PanelRight from "lucide-solid/icons/panel-right"; import PanelRightClose from "lucide-solid/icons/panel-right-close"; +import { handleExportSVG } from "../visualization"; /** An analysis document "live" for editing. */ @@ -232,7 +234,12 @@ export function AnalysisDocumentEditor(props: { onExpand={() => setSidePanelOpen(true)} >
-

Analysis

+
+

Analysis

+ + + +
diff --git a/packages/frontend/src/document/model_document_editor.css b/packages/frontend/src/document/model_document_editor.css index fe3914df1..c42dd3ac9 100644 --- a/packages/frontend/src/document/model_document_editor.css +++ b/packages/frontend/src/document/model_document_editor.css @@ -20,3 +20,22 @@ .model-theory select:invalid { color: darkgray; } + +.export-button { + font-family: var(--main-font); + padding: 4px; + font-weight: 600; + cursor: pointer; + margin: 10px; + border: none; +} + +.export-button:hover { + color: #53b6b2; + background-color: #dff1f0; +} + +#analysis-nav { + display: flex; + flex-direction: row; +} diff --git a/packages/frontend/src/index.css b/packages/frontend/src/index.css index c2facf181..bc284b4f3 100644 --- a/packages/frontend/src/index.css +++ b/packages/frontend/src/index.css @@ -66,10 +66,11 @@ h3 { flex-grow: 1; } -.content-panel { - overflow: hidden; -} - .side-panel { background: #f8f8f8; } + +.content-panel { + overflow-x: scroll; + overflow-y: hidden; +} diff --git a/packages/frontend/src/visualization/export_visualization.tsx b/packages/frontend/src/visualization/export_visualization.tsx new file mode 100644 index 000000000..a4a7db1f9 --- /dev/null +++ b/packages/frontend/src/visualization/export_visualization.tsx @@ -0,0 +1,37 @@ +/** +Get a handle to SVG DOM element once Solid has constructed it (using the ref mechanism) +Use XMLSerializer to write that DOM node to a stringhttps://statmodeling.stat.columbia.edu/ +Save that string as a file + */ +import computedStyleToInlineStyle from "computed-style-to-inline-style"; + + +export function exportVisualizationSVG(visualization: HTMLDivElement) { + computedStyleToInlineStyle(visualization, { recursive: true }); + + // ref equivalent of get document element by ID + const serializer = new XMLSerializer(); + let source = serializer.serializeToString(visualization); + // Add name spaces + if (!source.match(/^]*?\sxmlns=(['"`])https?\:\/\/www\.w3\.org\/2000\/svg\1/)) { + source = source.replace(/^]*?\sxmlns:xlink=(['"`])http\:\/\/www\.w3\.org\/1999\/xlink\1/)) { + source = source.replace(/^\r\n${source}`; + + // Convert SVG source to URI data scheme + const url = `data:image/svg+xml;charset=utf-8,${encodeURIComponent(source)}`; + + const link = document.createElement("a"); + link.href = url; + link.download = "visualization.svg"; + + document.body.appendChild(link); + link.click(); + document.body.removeChild(link); + + console.log("SVG file download initiated"); +} diff --git a/packages/frontend/src/visualization/graphviz_svg.tsx b/packages/frontend/src/visualization/graphviz_svg.tsx index cf92c5dcd..43e34c88a 100644 --- a/packages/frontend/src/visualization/graphviz_svg.tsx +++ b/packages/frontend/src/visualization/graphviz_svg.tsx @@ -1,6 +1,7 @@ import type * as Viz from "@viz-js/viz"; import { type JSX, Suspense, createResource } from "solid-js"; +import { exportVisualizationSVG } from "./export_visualization"; import { GraphSVG } from "./graph_svg"; import { loadViz, parseGraphvizJSON, vizRenderJSON0 } from "./graphviz"; import type * as GraphvizJSON from "./graphviz_json"; @@ -35,8 +36,18 @@ function GraphvizOutputSVG(props: { graph?: GraphvizJSON.Graph; }) { return ( -
+
); } + +// Create a ref for the visualization container +let visualizationRef: HTMLDivElement | undefined; + +// export handling +export const handleExportSVG = () => { + if (visualizationRef) { + exportVisualizationSVG(visualizationRef); + } +}; diff --git a/packages/frontend/vite.config.ts b/packages/frontend/vite.config.ts index 7d7af7cb5..6f8927c5f 100644 --- a/packages/frontend/vite.config.ts +++ b/packages/frontend/vite.config.ts @@ -38,5 +38,8 @@ export default defineConfig({ rewrite: (path) => path.replace(/^\/api/, ""), }, }, + watch: { + usePolling: true, // polling may be more reliable within the container + }, }, });