This is a companion discussion topic for the original entry at http://brunogavranovic.com/posts/2023-02-12-two-kinds-of-prisms.html
The place I have seen “prisms as opposite lenses” get the most use is for Spivakian wiring diagrams. A wiring diagram is a prism in the category of (perhaps labelled) finite sets.
I make the argument in the first chapter of my book that these are not really prisms at all, but rather lenses in free cartesian categories. The information flow is determined in exactly the lens way, and since the cartesian categories are free this information flow is purely reshuffling, duplicating, and forgetting of variables. In other words, I see lens-op prisms as really just lenses in free cartesian categories.
In general, I take the point of view that for a doctrine of processes or information flow, the appropriate diagrams are free processes — which is to say, processes occuring in free models of the doctrine. Diagrams get their combinatorial character (which allows us to draw them) from the particular combinatorial presentation of free models of the doctrine.
For example, for relational information flow where a process is a span in some category with pullbacks, the diagrams are the spans in free categories with pullbacks — these are cospans of finite sets. Similarly, where a process is a combinatorial object itself which is composed through the gluing of subobjects — that is, a cospan composed by pushouts — the diagrams are cospans in free categories with pushouts. These are also cospans of finite sets. In both cases, we recover the bubble diagrams given by cospans of finite sets, and find that the categories of processes are hypergraph categories understood as cospan-algebras.
3 Likes
Hi David,
Glad to hear that I’m not the only one with this stance. Unfortunately Spivak’s wiring diagrams is not the only place I heard this: people often refer to this in the context of optics, and use as a justification that the problem of dependent prisms (and more generally, dependent optics (Def. 3.3)) is solved.
Also - what do you mean by Lens(C^op) being lenses in free cartesian categories? I’m not sure how the jump from C^op to free cartesian categories instead of cocartesian categories was made.
So my take is that it’s not \text{Lens}(C^{\text{op}}), but rather simply \text{Lens}(F(C)) where F(C) is the free cartesian category on C. This can be explicitly constructed as objects pairs (I, c : I \to C) of a finite set I and an I-indexed family c of objects in C, and where a morphism (I, c) \to (J, c') is a pair (r : J \to I, f : (j \in J) \to c(r(j)) \to c'(j)). The product is defined by (I, c) \times (J, c') := \left(I + J, \begin{cases} c \\ c' \end{cases} : I + J \to C \right) In particular, note that F(1) is just the opposite of the category of finite sets.
So a lens in F(1) is a prism of finite sets, and in general a lens in F(C) is “prism-like”.
Another way to describe F(C) is as the opposite of the category of Spivak/functor lenses for the indexed category C^{(-)} : \text{FinSet}^{\text{op}} \to \text{Cat}.