the free cartesian category generated by a single object X
objects: X, the generic object, and for any finite set I, an I-fold power XI of X
{XI∣I a finite set}
morphisms: f∗:XI→XJ for any function f:J→I
composition: defined by g∗∘f∗:=(f∘g)∗
identity: id:=id∗
cartesian product: given in terms of index sets, by XI×XJ=XI+J
Proposition: Arity is isomorphic to the opposite of the category finite sets
Arity≅FinSetop
how it express the algebra of shuffling, copying, and deleteing variables?
we think of elements of XI as finite lists of variable XI=(xi∣i∈I) indexed by set I
for any reindexing function f:J→I , f∗ tells us how J-variables are assigned I-variables
eg the map f∗:X2→X3, given by function f:3→2, looks like
(x1,x2)↦(x1,x1,x2), in function notation
morphism X2→X0, given by the initial function !′:0→2
(x1,x2)↦()
duplication morphism: !∗:X→X2, given by !:2→1
(x1)↦(x1,x1)
swap morphism: swap∗:X2→X2, given by swap:2→2
(x1,x2)↦(x2,x1)
projection morphism: 1∗:X2→X1, given by 1:1→2
picking the first element
projection morphism: 2∗:X2→X1, given by 2:1→2
picking the second element
composition is given by composing functions in the opposite direction
the category WD of wiring diagrams is defined to be the category of lenses in the category of arities Arity:
WD:=LensArity
we consider WD as a monoidal category in the same way we consider LensArity 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 Arity
that Arity the free cartesian category generated by a single objects means it satisifes a very useful universal property:
for any cartesian category C and object C∈C, there is a cartesian functor evC:Arity→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 Arity as variables of type C
Proposition: interpreting wiring diagram as a lens in C
let C∈C be an object of a cartesian category, then there is a strong monoidal functor
(evCevC):WD→LensC
which interprets a wiring diagram as a lens in 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.