category Arity

• capture precisely the algebra of copying, deleting, and shuffling around variables
• wiring diagram are interpreted as lenses in the category of arities, which are the free cartesian categories
• Definition: category \(\mathbf{Arity}\)
  • the free cartesian category generated by a single object \(\mathbf{X}\)
  • objects: \(X\), the generic object, and for any finite set \(I\), an \(I\)-fold power \(X^{I}\) of \(X\)
    • \(\{X^{I} | I \text{ a finite set}\}\)
  • morphisms: \(f^{*}: X^{I} \to X^{J}\) for any function \(f: J \to I\)
  • composition: defined by \(g^{*} \circ f^{*} := (f \circ g)^{*}\)
  • identity: \(id:= id^{*}\)
  • cartesian product: given in terms of index sets, by \(X^{I} \times X^{J} = X^{I + J}\)
• Proposition: \(\mathbf{Arity}\) is isomorphic to the opposite of the category finite sets
  • \(\mathbf{Arity} \cong \mathbf{FinSet}^{op}\)
• how it express the algebra of shuffling, copying, and deleteing variables?
  • we think of elements of \(X^{I}\) as finite lists of variable \(X^{I} = (x_{i}\ |\ i \in I)\) indexed by set \(I\)
  • for any reindexing function \(f: J \to I\) , \(f^{*}\) tells us how \(J\)-variables are assigned \(I\)-variables
    • eg the map \(f^{*}: X^{2} \to X^{3}\), given by function \(f: 3 \to 2\), looks like
      • \((x_{1}, x_{2}) \mapsto (x_{1}, x_{1}, x_{2})\), in function notation
    • morphism \(X^{2} \to X^{0}\), given by the initial function \(!': 0 \to 2\)
      • \((x_{1}, x_{2}) \mapsto ()\)
    • duplication morphism: \(!^{*}: X \to X^{2}\), given by \(!: 2 \to 1\)
      • \((x_{1}) \mapsto (x_{1}, x_{1})\)
    • swap morphism: \(\text{swap}^{*}: X^{2} \to X^{2}\), given by \(\text{swap}: 2 \to 2\)
      • \((x_{1}, x_{2}) \mapsto (x_{2}, x_{1})\)
    • projection morphism: \(1^{*}: X^{2} \to X^{1}\), given by \(1: 1 \to 2\)
      • picking the first element
    • projection morphism: \(2^{*}: X^{2} \to X^{1}\), given by \(2: 1 \to 2\)
      • picking the second element
  • composition is given by composing functions in the opposite direction
• the category \(\mathbf{WD}\) of wiring diagrams is defined to be the category of lenses in the category of arities \(\mathbf{Arity}\):
  • \(\mathbf{WD} := \mathbf{Lens}_{\mathbf{Arity}}\)
  • we consider \(\mathbf{WD}\) as a monoidal category in the same way we consider \(\mathbf{Lens}_{\mathbf{Arity}}\) as a monoidal category
  • We can read any wiring diagram as a lens in Arity in the following way:
    • ... (1.3.5 of Categorical System Theory)
• universal property of \(\mathbf{Arity}\)
  • that \(\mathbf{Arity}\) the free cartesian category generated by a single objects means it satisifes a very useful universal property:
  • for any cartesian category \(\mathcal{C}\) and object \(C \in \mathcal{C}\), there is a cartesian functor \(\mathbf{ev}_{\mathcal{C}} : \mathbf{Arity} \to \mathcal{C}\) which sends \(X\) to \(C\)
  • this functor is unique up to a unique natural isomorphism
  • we can think that the functor tells us how to interpret the abstract variables in \(\mathbf{Arity}\) as variables of type \(\mathcal{C}\)
• Proposition: interpreting wiring diagram as a lens in \(\mathcal{C}\)
  • let \(C \in \mathcal{C}\) be an object of a cartesian category, then there is a strong monoidal functor
    • \(\begin{pmatrix} \mathbf{ev}_{C} \\ \mathbf{ev}_{C}\end{pmatrix} : \text{WD} \to \mathbf{Lens}_{\mathcal{C}}\)
  • which interprets a wiring diagram as a lens in \(\mathcal{C}\) with values in \(C\) flowing along its wires.
  • we may interpret a wiring diagram as a lens in whatever cartesian category we are working in
  • if there exists many different types of signal flowing along the wires, we can use typed arities to only allow connecting wires that carry the same type of signal
    • definition 1.3.3.9
    • we can define the category of typed wiring diagrams to be the category of lenses in the category of typed arities.