• 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.