Dev docs on free models of double theories

dev-docs/trees/dbl-0001.tree

@@ -1,8 +1,16 @@
-\title{Double category theory}
+\title{Background on double categories}
 
+\p{General double category theory:
 \ul{
 \li{[[dbl-0002]]}
+}
+}
+
+\p{Double theories and models:
+\ul{
 \li{[[dbl-0008]]}
-\li{[[dbl-0005]]}
+\li{[Discrete models](dbl-0005)}
+\li{[Free models](dbl-000D)}
 \li{[[dbl-000C]]}
 }
+}

dev-docs/trees/dbl-000C.tree

@@ -1,7 +1,7 @@
-\title{Modules over models of double theories}
+\title{Instances of models}
 \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 &
+\p{A \em{module} over a model of a double theory, also called an \em{instance} of the model, 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."}

dev-docs/trees/dbl-000D.tree

@@ -0,0 +1,72 @@
+\title{Free models of double theories}
+\import{macros}
+
+\p{The \em{free} models of a double theory are often singled out in
+applications. For example, free [signed categories](dct-0002) can be interpreted
+as causal loop diagrams or regulatory networks, depending on the application.
+Here we seek a definition of a free model of an arbitrary double theory. We will
+recover the familiar free-forgetful adjunction between graphs and categories
+when the theory is specialized to the [trivial double theory](thy-0001).}
+
+\p{Our strategy is to use a forgetful 2-functor from double categories to
+"double graphs," as defined below. I (Evan) don't have a reference for the
+following but I've used it before in my unpublished notes on pull-push
+formalism.}
+
+\transclude{dbl-000E}
+
+\p{More generally, we define:}
+
+\transclude{dbl-000F}
+
+\p{Taking the 2-category #{\twocat{K} = \Cat} in this definition, we obtain a
+2-category of double graphs, call it \twocat{DblGph}. For any choice of maps
+between double categories, there is a 2-functor
+
+##{U: \twocat{Dbl} \to \twocat{DblGph}}
+
+that forgets the external composition and identities in a double category
+(pseudocategory in \Cat). When applied to pseudo, lax, or colax double functors,
+it also forgets the composition and identity comparisons. Crucially, these
+comparisons are what make models of double theories (span-valued lax double
+functors) into categorical structures, i.e., structures with composition and
+identities.}
+
+\p{All of this extends to cartesian double categories and "cartesian double
+graphs," as defined below.}
+
+\transclude{dbl-000G}
+
+\p{There is a 2-category of cartesian double graphs, cartesian morphisms between
+them, and cells between those (with no extra conditions). As before, for any
+choice morphisms between cartesian double categories, we obtain a forgetful
+2-functor
+
+##{U: \twocat{CartDbl} \to \twocat{CartDblGph}.}
+
+}
+
+\p{The data that generates a free model we will provisionally call a "network"
+since it will encompass familiar concepts such as graphs and Petri nets.}
+
+\transclude{dbl-000H}
+
+\subtree{
+\title{Examples of networks over double theories}
+\taxon{example}
+
+\ul{
+\li{A network over the [trivial double theory](thy-0001) is a graph}
+
+\li{A network over the [theory of signed categories](thy-0002) is a
+\define{signed graph}: a graph with each edge weighted by a plus or minus sign.}
+
+\li{A network over the theory of commutative monoids, such that the monoids of
+objects and of arrows are both free, is a \define{Petri net}: a pair of sets
+#{S} and #{T} together with a pair of maps #{T \rightrightarrows \N[S]}, where
+#{\N[S]} is the free commutative monoid on #{S} (see, for example, [Baez and
+Pollard 2017](baez-pollard-2017)).}}
+
+}
+
+\transclude{dbl-000I}

dev-docs/trees/dbl-000E.tree

@@ -0,0 +1,6 @@
+\title{Double graph}
+\taxon{definition}
+\import{macros}
+
+\p{A \define{double graph} is a graph object \dbl{G} in \Cat, i.e., an endospan
+#{\dbl{G}_0 \xfrom{s} \dbl{G}_1 \xto{t} \dbl{G}_0} of categories.}

dev-docs/trees/dbl-000F.tree

@@ -0,0 +1,24 @@
+\title{Graphs in a 2-category}
+\taxon{definition}
+\import{macros}
+
+\p{Let \twocat{K} be a 2-category. In the \define{2-category of graphs in
+\twocat{K},}
+
+\ul{
+
+\li{an object \dbl{G} is a graph object #{s,t: \dbl{G}_1 \rightrightarrows
+\dbl{G}_0} in \twocat{K}, where #{s} is called the \define{source} map and #{t}
+is called the \define{target} map;}
+
+\li{a morphism #{F: \dbl{G} \to \dbl{H}} is a pair of morphisms #{F_i: \dbl{G}_i
+\to \dbl{H}_i}, for #{i = 0,1}, in \twocat{K} that commute with the source and
+target maps; and}
+
+\li{a cell #{\alpha: F \To G} is a pair of cells #{\alpha_i: F_i \To G_i}, for
+#{i = 0,1}, in \twocat{K} that commute with whiskering by the source and target
+maps.}
+
+}
+
+Composition in this 2-category is inherited componentwise from \twocat{K}.}

dev-docs/trees/dbl-000G.tree

@@ -0,0 +1,18 @@
+\title{Cartesian double graph}
+\taxon{definition}
+\import{macros}
+
+\p{A [double graph](dbl-000E) \dbl{G} is \define{cartesian} when either of the
+following equivalent conditions hold:
+
+\ul{
+
+\li{\dbl{G} is a \nlab{cartesian object} in the [2-category of double
+graphs](dbl-000F).}
+
+\li{The underlying categories #{\dbl{G}_0} and #{\dbl{G}_1} have finite
+products, which are preserved by the source and target functors #{s,t: \dbl{G}_1
+\rightrightarrows \dbl{G}_0}.}
+
+}
+}

dev-docs/trees/dbl-000H.tree

@@ -0,0 +1,14 @@
+\title{Network over a double theory}
+\taxon{definition}
+\import{macros}
+
+\p{Let #{\dbl{T}} be a simple or cartesian double theory. A \define{network over
+\dbl{T}}, or \define{\dbl{T}-network}, is a morphism of (cartesian) double
+graphs
+
+##{N: U(\dbl{T}) \to \Span,}
+
+where #{U} is the forgetful 2-functor and, by a harmless abuse of notation,
+\Span also denotes the (cartesian) double graph of spans.
+
+}

dev-docs/trees/dbl-000I.tree

@@ -0,0 +1,20 @@
+\title{Free model functor}
+\taxon{definition}
+\import{macros}
+
+\p{The \define{free model functor} for a simple double theory \dbl{T}, denoted
+
+##{F: \cat{Net}_{\dbl{T}} \to \cat{Mod}_{\dbl{T}},}
+
+is the left adjoint to the forgetful functor
+
+##{
+\cat{Mod}_{\dbl{T}} \coloneqq
+\twocat{Dbl}_{\mathrm{lax}}(\dbl{T}, \Span) \xto{U}
+\twocat{DblGraph}(U(\dbl{T}), \Span)
+\eqqcolon \cat{Net}_{\dbl{T}}
+}
+
+given by applying the forgetful 2-functor #{U: \twocat{Dbl}_{\mathrm{lax}} \to
+\twocat{DblGph}}. The \define{free model functor} for a cartesian double theory
+is defined similarly, inserting the modifier "cartesian" where appropriate.}

dev-docs/trees/macros.tree

@@ -57,6 +57,7 @@
 \def\op{#{\mathrm{op}}}
 
 \def\xto[label]{#{\xrightarrow{\label}}}
+\def\xfrom[label]{#{\xleftarrow{\label}}}
 \def\To{#{\Rightarrow}}
 \def\hetto{#{\dashrightarrow}}
 
@@ -69,6 +70,7 @@
 
 % 2-category theory
 
+\def\twocat[name]{#{\mathbf{\name}}}
 \def\Cat{#{\mathbf{Cat}}}
 
 % Double category theory
@@ -77,7 +79,6 @@
 \def\xproto[label]{#{\overset{\label}{\proto}}}
 \def\proTo{#{\mathrel{\mkern3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\Rightarrow}}}}
 
-
 \def\tabulator[ob]{#{\top\ob}}
 
 \def\dbl[name]{#{\mathbb{\name}}}

dev-docs/trees/refs/baez-pollard-2017.tree

@@ -0,0 +1,7 @@
+\title{A compositional framework for reaction networks}
+\author{John Baez}
+\author{Blake Pollard}
+\date{2017}
+\taxon{reference}
+\meta{arxiv}{1704.02051}
+\meta{doi}{10.1142/S0129055X17500283}