You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
This comment from @Matteo Capucci (he/him) brought to mind this talk by Paré on double categories. On slide 6, Paré gives a list of cases in which, presumably, there are two kinds of 1-morphism related by a 2-cell which might be suitably modeled double-categorically. I say "presumably" because I can't quite see how to fill in the details of most of these myself, or what Paré might have had in mind. Here's the list:
See also this MathOverflow question seeking the same thing. As noted there, some of these are more or less discernible: partial and total maps, lax and oplax monoidal functors, horizontal and vertical morphisms generally. But I can't quite see the rest. Can anyone help? Was this list just speculating on cases in which double categories might be useful?
For both total/partial and determinstic/stochastic the general pattern is that given a monad you can make a double category whose proarrows are kleisli arrows and vertical arrows are morphisms of the underlying category. (Probably classical/quantum and classical/intuitionistic can fit that pattern as well)
I think I understand what he is getting at with quantum/classical. Spans of finite sets is equivalent to matrices over the natural numbers. So regarded as a double category, the tight maps are functions... which are the things that can be copied by the comonoid induced from the choice of basis. And the loose maps are general relations. Now matrices over the natural numbers embeds in complex matrices which is equivalent to finite dimensional Hilbert spaces. The unit for the compact closed structure is transported to what is interpreted as the maximally mixed state along this embedding. So in double category land, quantum entanglement comes from the proarrow equipment. There is probably some notion of double category of matrices, but I'm not sure. It would be cool if there is a double category of C*-algebras
Cole Comfort said:
I think I understand what he is getting at with quantum/classical. Spans of finite sets is equivalent to matrices over the natural numbers. So regarded as a double category, the tight maps are functions... which are the things that can be copied by the comonoid induced from the choice of basis. And the loose maps are general relations. Now matrices over the natural numbers embeds in complex matrices which is equivalent to finite dimensional Hilbert spaces. The unit for the compact closed structure is transported to what is interpreted as the maximally mixed state along this embedding. So in double category land, quantum entanglement comes from the proarrow equipment. There is probably some notion of double category of matrices, but I'm not sure. It would be cool if there is a double category of C*-algebras
I think this also explains deterministsic/possibilistic if you take the double category of relations. Or deterministic/equiprobable in the case of spans.
More generally, whenever you have a functor you can make a double category whose objects are those of , whose vertical arrows are those of , whose horizontal arrows are those of between objects in the image of , and whose 2-cells are commutative squares in that have applied on the left and the right. More generally, if is a 2-category you can take the 2-cells to be 2-cells in .
These were all helpful, thanks! The putative case that's still unclear to me, though, is the classical/intuitionistic. The first thing that came to mind is this. View a first-order intuitionistic structure as a poset-indexed collection of first-order structures (satisfying a suitable monotonicity property, so a presheaf of structures), . Then the 'classical' maps are maps of -bundles , i.e. a choice of morphism for each$ $p \in P$$ compatible with the ordering of $P$. And the 'intuitionistic' maps would be more general bundle maps , (where is a map of the Kripke frame, not just a monotone map). I think (modulo some fiddling) that this way, classical satisfiability is preserved vertically and intuitionistic satisfiability is preserved horizontally.