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.
Paolo Perrone (Jul 01 2020 at 20:48):Hello all! This is the thread of discussion for the talk of Tarmo Uustalu, Niccolò Veltri and Noam Zeilberger, "Proof Theory of Partially Normal Skew Monoidal Categories".
Date and time: Thursday July 9, 12:10 UTC.
Zoom meeting: https://mit.zoom.us/j/7055345747
YouTube live stream: https://www.youtube.com/watch?v=aXpjE82yy-8&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q
Tarmo Uustalu (Jul 09 2020 at 11:36):Here's our paper:
https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACT2020:60
Paolo Perrone (Jul 09 2020 at 11:55):15 minutes to start.
James Wood (Jul 09 2020 at 12:31):Do you have any natural examples of partially normal SMCs?
Tarmo Uustalu (Jul 09 2020 at 12:33):Yes, we do. Already the functor category example that Niccolò showed gives examples of each sort of partial normality.
Tarmo Uustalu (Jul 09 2020 at 12:34):Remember we had, \J, \C categories, J : \J \to \C a fixed functor.
Then the skew monoidal category was ([\J, \C], I, \otimes) where I = J, F \otimes G = Lan_J F . G.
Tarmo Uustalu (Jul 09 2020 at 12:36):Now this is generally just fully skew.
But \rho is invertible if and only if J is fully-faithful.
\lambda is invertible if and only if J is dense (ie the nerve of J is fully-faithful).
And there is also a characterization of when \alpha is invertible in terms of a property on J.
James Wood (Jul 09 2020 at 12:37):Aah, okay, these sound good as examples. Thanks!
Tarmo Uustalu (Jul 09 2020 at 12:37):Partial normality actually occurs quite often, so it's not an artificial idea.
James Wood (Jul 09 2020 at 12:39):A separate question: given that you have your formalisation of this work, have you tried turning it into a solver for skew-monoidal categories (of various normality)?
Tarmo Uustalu (Jul 09 2020 at 12:39):There are also some curiosities. Eg if you take the free skew-closed category generated by a set of objects, then it is also left-normal.
(But that's of course not true about arbitrary skew-closed categories.)
Jules Hedges (Jul 09 2020 at 12:40):(Tarmo, you can write latex by wrapping in double dollar signs)
Tarmo Uustalu (Jul 09 2020 at 12:41):Yes, thanks! It is a solver in fact!
Given two maps in the free partially normal skew-monoidal category, our completeness proof (of the sequent calculus) turns them into sequent calculus derivations, focusing further focuses these derivations and then one just has to compare the the focused derivations.
Tarmo Uustalu (Jul 09 2020 at 12:44):You can also exhaustively and duplicate-freely enumerate all maps in any homset in the free partially-normal skew-monoidal category:
given a domain and codomain, find all focused derivations, of course they are a special case of general sequent derivations and then our soundness proof (of the sequent calculus) turns them into (representatives of) maps of the free partially-normal skew-monoidal category.
Tarmo Uustalu (Jul 09 2020 at 12:46):(Thanks, Jules, a useful hint!)
James Wood (Jul 09 2020 at 12:48):Nice, this is good to hear. I think I'll have a look at one of the formalisations, and see how I can use this.
Niccolò Veltri (Jul 09 2020 at 12:54):Hi James, thanks for the nice questions.
Here are also the slides of the talk.
uvz-act20-slides.pdf
James Wood (Jul 09 2020 at 12:59):I'm interested in the solver partially because, IIUC, the solver you'd derive for (fully normal) monoidal categories would be different to the usual one, based on normalising the objects.
Tarmo Uustalu (Jul 09 2020 at 12:59):That's correct!
Tarmo Uustalu (Jul 09 2020 at 13:03):When I first looked at skew-monoidal categories I used normalization of objects, but you don't get a general coherence theorem then but only one for homsets from A to B where B is an object in normal form - there's exactly one map when B is the normal form of A and no maps when it is not. (That's different from monoidal categories where from this observation you can further conclude a statement about general homsets from A to B: there exactly one map when the normal forms of A and B coincide and no maps otherwise.)
Tarmo Uustalu (Jul 09 2020 at 13:03):Focussing does something different and works for all homsets.
Tarmo Uustalu (Jul 09 2020 at 13:07):But then in some unpublished work with Exe Rivas we found yet another coherence proof for skew monoidal categories where sequent calculus is not used, you work directly on (representations of) the free skew monoidal maps and focus there. This is more complicated than in the sequent calculus, but it's possible. This means normalization of maps rather than objects.
Tarmo Uustalu (Jul 09 2020 at 13:09):The sequent calculus focusing idea came from Noam - he did it first - for the free skew semigroup category (= the Tamari order).
Niccolò Veltri (Jul 09 2020 at 13:11):Tarmo Uustalu said:
But then in some unpublished work with Exe Rivas we found yet another coherence proof for skew monoidal categories where sequent calculus is not used, you work directly on (representations of) the free skew monoidal maps and focus there. This is more complicated than in the sequent calculus, but it's possible. This means normalization of maps rather than objects.
This construction works (so far!) only in the free skew semigroup category, which is the case where there is no unit, and the only structural morphism is the associator .
Tarmo Uustalu (Jul 09 2020 at 13:12):Indeed, sorry for the mistake in the statement.
Paolo Perrone (Jul 09 2020 at 17:27):Video here!
https://www.youtube.com/watch?v=UdZleN5L0TA&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI
