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.
Jules Hedges (Apr 05 2020 at 13:26):In any case, I shall repeat my standard challenge for people working on proof assistants. State and prove the Joyal-Street coherence theorem, ie. that the free monoidal category on a signature is equivalent to the monoidal category of string diagrams modulo planar isotopy. This isn't an advanced result, it's an absolutely basic one that I rely on pretty much every day. I'm happy to be proved wrong, but I believe this is far out of reach of current proof assistant technology
(=_=) (Apr 05 2020 at 13:29):Jules Hedges said:
In any case, I shall repeat my standard challenge for people working on proof assistants.
None of them are here, they're on the other server. :sweat_smile:
Maybe retweet your challenge, that should get some attention.
Daniel Geisler (Apr 05 2020 at 13:30):The world champion Go player is a computer. AI is now making yearly advancements. So yes, I think we will see exponential growth in what computers can do in math.
James Wood (Apr 05 2020 at 13:31):Is this actually the theorem you want? How do you define planar isotopy, and do you prove things according to those definitions every day?
Jules Hedges (Apr 05 2020 at 13:32):That's the theorem that says that proof by pictures is actually sound
James Wood (Apr 05 2020 at 13:32):Daniel Geisler said:
The world champion Go player is a computer. AI is now making yearly advancements. So yes, I think we will see exponential growth in what computers can do in math.
I'm not convinced that this is relevant. Problems with proof assistants are largely about the interface between the human and the computer.
James Wood (Apr 05 2020 at 13:33):Yeah, but I think when you draw the pictures, you're not really doing all the real analysis you claim to be doing.
Jules Hedges (Apr 05 2020 at 13:33):Generally you prove that 2 things are equal by drawing them as string diagrams and eyeballing them to see that they're evidently isotopic
(=_=) (Apr 05 2020 at 13:33):James Wood said:
Daniel Geisler said:
The world champion Go player is a computer. AI is now making yearly advancements. So yes, I think we will see exponential growth in what computers can do in math.
I'm not convinced that this is relevant. Problems with proof assistants are largely about the interface between the human and the computer.
I'm somewhat hopeful that we can improve that interface. AI/ML is still going to play a part though.
(=_=) (Apr 05 2020 at 13:34):Of course, it may require a few more abstraction layers. But I'm tired of people saying, "You are not going to make me write proofs in HoTT". Sure, and nobody is building websites in C.
James Wood (Apr 05 2020 at 13:35):People don't write websites in AI, though.
(=_=) (Apr 05 2020 at 13:37):James Wood said:
People don't write websites in AI, though.
AI is the back-end. It'd probably be needed for the NLP component. The (utopian) end-state is that you can feed the machine papers written in human style, and it'd digest that for you. Maybe even teach you the results.
(=_=) (Apr 05 2020 at 13:38):Also, this.
(=_=) (Apr 05 2020 at 13:41):Mohan Ganesalingam, co-founder of what3words, wrote his thesis on the grammar of mathematics written in a natural language a while ago. Tim Gowers helped him do a demo. I thought that was pretty impressive at the time, and NLP has moved on quite a bit since then.
Reid Barton (Apr 05 2020 at 13:46):Jules Hedges said:
Generally you prove that 2 things are equal by drawing them as string diagrams and eyeballing them to see that they're evidently isotopic
While I think the Joyal-Street theorem would be a great challenge for formalization, if you wanted to actually prove that two concrete things are equal in a theorem prover, it would be a lot easier to just give the algebraic argument than to exhibit the isotopy in a way that would satisfy the prover. From a practical perspective the most useful thing to do would be to hook up Globular to your proof assistant.
Jules Hedges (Apr 05 2020 at 13:52):Here's an example from one of my papers where I used this exact method (with the corresponding coherence theorem for the free traced cartesian monoidal category), one of the morphisms looked like this: (https://categorytheory.zulipchat.com/user_uploads/21317/JdDRlbknE4ks668LN-YLekLI/Untitled.jpg)
Reid Barton (Apr 05 2020 at 13:53):Paul Blain Levy said:
Reid Barton said:
Paul Blain Levy said:
Some people are put off category theory by the size issues. And I can hardly blame them. The issues are more serious than many category theorists are willing to admit.
Since we ended up talking about some size issues anyways I'm curious to hear about what kind of issues you have in mind here.
The basic problem is that the most important category of all, viz. the category of sets, doesn't exist. None of the proposed workarounds is entirely satisfactory. (I learnt a lot on this subject from Mike Shulman's paper "Set theory for category theory.")
"Just use universes" is (or should be) the standard solution, and yes it leaves unaddressed some questions about whether or not some universal properties are invariant of the choice of ambient universe, but this is mostly a question about how you apply category theory to other areas (say commutative algebra), and where you really need it, you can check it by hand.
Reid Barton (Apr 05 2020 at 13:53):and where's the formula for the isotopy?
Jules Hedges (Apr 05 2020 at 13:53):The formula for isotopy is in the reader's visual cortex
Jules Hedges (Apr 05 2020 at 13:54):Giving the isotopy explicitly means going back to the stone age, where these things take 1000 times longer and are pretty much impossible to read
Reid Barton (Apr 05 2020 at 13:55):But the theorem prover doesn't know how to formalize any of that, so from a practical perspective, having the Joyal-Street theorem formalized in your theorem prover doesn't help.
Andre Knispel (Apr 05 2020 at 13:55):Jules Hedges said:
The formula for isotopy is in the reader's visual cortex
So I guess what you want is an automated system that looks at two diagrams and then gives you the isotopy
Andre Knispel (Apr 05 2020 at 13:55):And from there you plug that into the theorem and you're done
Reid Barton (Apr 05 2020 at 13:56):now we're in the area of guessing, but it's also probably easier for that automated system to construct a globular-style proof
Reid Barton (Apr 05 2020 at 13:56):rather than something that really involves the theorem prover's internal notion of the real numbers
Reid Barton (Apr 05 2020 at 13:56):which are what would appear in the Joyal-Street theorem.
Reid Barton (Apr 05 2020 at 13:57):But maybe you can get by with rational numbers, piecewise linear paths, etc. I don't know.
Andre Knispel (Apr 05 2020 at 13:57):So I think if you have properly formalized the notions of "diagram" and "isotopy", proving the theorem itself should more or less be a standard exercise, and then you just have to hook it up to that system that generates isotopies
Morgan Rogers (he/him) (Apr 05 2020 at 13:57):Jules Hedges said:
Here's an example from one of my papers where I used this exact method (with the corresponding coherence theorem for the free traced cartesian monoidal category), one of the morphisms looked like this: (https://categorytheory.zulipchat.com/user_uploads/21317/JdDRlbknE4ks668LN-YLekLI/Untitled.jpg)
Nice diagram, Jules :heart_eyes:
Andre Knispel (Apr 05 2020 at 13:59):Reid Barton said:
But maybe you can get by with rational numbers, piecewise linear paths, etc. I don't know.
I guess piecewise linear on a grid would be the easiest to work with
Andre Knispel (Apr 05 2020 at 14:00):And that shouldn't be any restriction
James Wood (Apr 05 2020 at 14:02):To be fair, the Joyal-Street theorem might be useful if you happen to want to prove some isotopies.
Jules Hedges (Apr 05 2020 at 14:03):Now you're all cheating by assuming the Joyal-Street theorem and building a new proof assistant around it. If you haven't formalised the proof in a proof assistant and instead rely on the proof in Joyal and Steet's paper, how do you know your new proof assistant is sound? (Nb. I'm playing devil's advocate here)
Andre Knispel (Apr 05 2020 at 14:05):Jules Hedges said:
Now you're all cheating by assuming the Joyal-Street theorem and building a new proof assistant around it. If you haven't formalised the proof in a proof assistant and instead rely on the proof in Joyal and Steet's paper, how do you know your new proof assistant is sound? (Nb. I'm playing devil's advocate here)
I'm not sure where I'm assuming that
Jules Hedges (Apr 05 2020 at 14:05):This is potentially important because many corresponding theorems for different classes of monoidal category haven't been proven, or have only been proven for special cases. I've knowingly relied on coherence theorems that haven't been proved, because I'd rather get some useful work done than spend forever down in the foundations
Reid Barton (Apr 05 2020 at 14:06):No, so to be clear what I suggest is: Work in your favorite off-the-shelf theorem proving system; develop enough category theory in it so that you can state the kinds of theorems you'd like to prove using Globular; now figure out how to export Globular constructions to proofs in your system--this part will be by an unverified translation, but in each specific instance (and you seem mainly interested in specific instances) the original theorem prover will verify that the exported proof is correct.
Jules Hedges (Apr 05 2020 at 14:07):Ah, I see. So you still need to prove the theorem, I guess
Reid Barton (Apr 05 2020 at 14:07):You need to write down the algorithm which is effectively the proof of the theorem, but you don't need to prove that you've written down the algorithm correctly. It's just that if you wrote it down wrong, then your export step will fail (but you'll find out when you try to verify the exported proof).
Reid Barton (Apr 05 2020 at 14:08):And in fact there is no way to prove that your translation will always succeed unless you also formalized Globular (or equivalent) inside your original theorem prover.
Andre Knispel (Apr 05 2020 at 14:08):I'm not sure where the issue with the theorem would be, if you formalize notions that are decent to work with
Andre Knispel (Apr 05 2020 at 14:09):If you really want isotopies on the real plane, sure, but just use some discrete approximation
Andre Knispel (Apr 05 2020 at 14:10):That gives you a special case that works in all applications
Jules Hedges (Apr 05 2020 at 14:11):Yes, my original claim is that formalising the actual proof contained in Joyal and Street's paper is in practice beyond current ability. It's a reasonably long proof and mostly geometric, by recursive subdivision of the plane and then a lot of fiddling around
Jules Hedges (Apr 05 2020 at 14:12):You could cheat by defining diagrams combinatorially. I guess that the equivalence between the geometric definition and combinatorial definition of diagrams probably contains most of the difficulty of the original proof
Andre Knispel (Apr 05 2020 at 14:12):I see, so the challenge is to actually do this
Andre Knispel (Apr 05 2020 at 14:15):What you could do about this is really to formalize a system such as globular in the proof assistant. That way you implicitly prove the theorem as a by-product
Andre Knispel (Apr 05 2020 at 14:15):(a discrete version of the theorem)
Jules Hedges (Apr 05 2020 at 14:16):In practice the world has largely moved on to "officially" defining diagrams combinatorially, but then we still draw pictures and reason graphically
Andre Knispel (Apr 05 2020 at 14:17):Yeah, but that's ok. If you draw them in software they look like a picture but they really are combinatorial anyways
Morgan Rogers (he/him) (Apr 05 2020 at 14:24):Andre Knispel said:
What you could do about this is really to formalize a system such as globular in the proof assistant. That way you implicitly prove the theorem as a by-product
It feels like there's a meta-level of reasoning being collapsed here. Joyal-Street is a statement about all diagrams of a certain form; a formalisation in globular of the sort you're describing would allow you to construct the isotopies between such diagrams and convert them into algebraic proofs; but we only know that the isotopies always exist by Joyal-Street. I suspect this is just my ignorance of how proof assistants work, though; would the combinatorial formalism you were describing earlier actually let you argue "for all diagrams with property X, conclusion Y"?
Andre Knispel (Apr 05 2020 at 14:27):It depends on the actual implementation. If the system converts the diagrams into proof terms then you only end up with proofs for the diagrams you constructed. But if the system converts them into actual proofs, you get the proper theorem
James Wood (Apr 05 2020 at 14:28):In practice, I think formalising Globular would entail proving this “for all diagrams” theorem somewhat directly. In particular, you'd probably never introduce real numbers, and thus not really prove the Joyal-Street theorem.
James Wood (Apr 05 2020 at 14:29):But you also don't rely on the Joyal-Street theorem for the correctness of your proofs.
Andre Knispel (Apr 05 2020 at 14:30):Yeah, as I said above, you'd get a discrete version
Fabrizio Genovese (Apr 05 2020 at 14:52):What I think it would be really useful is a diagrammatic assistant for proof systems. Let me explain: At least in what we do, a lot of pain in proving things is when you have to manually rewrite terms into each other. This comes with a lot of bookkeeping, and when this happens you end up with some code that is barely readable, and progress is super slow
Fabrizio Genovese (Apr 05 2020 at 14:53):But term rewriting can be visualized. It would be super nice to have some form of editor that visualizes a term for you, lets you isolate bits of it and rewrite them, and produces the code for you as a result. We used string diagram quite heavily to represent idris terms when we had to prove some things about permutations that involved crazy rewrites
Fabrizio Genovese (Apr 05 2020 at 14:54):So there's that on one hand, and the other big obstacle is that a lot of interesting stuff in maths does not have a corresponding inductive data structure representing it. Most notably, this is true for free SMCs.
Fabrizio Genovese (Apr 05 2020 at 14:55):When you don't have such data structures life becomes a mess, you can't pattern match, you can't do anything, and proving things just becomes a succession of tricks which make everything even more complicated at each step
Andre Knispel (Apr 05 2020 at 15:05):Fabrizio Genovese said:
What I think it would be really useful is a diagrammatic assistant for proof systems. Let me explain: At least in what we do, a lot of pain in proving things is when you have to manually rewrite terms into each other. This comes with a lot of bookkeeping, and when this happens you end up with some code that is barely readable, and progress is super slow
Yes, but it's probably not worth the effort right now. There are many techniques that have a bigger ROI at this point than such a system, in particular if you're working with Idris, but even in Coq or Agda.
Andre Knispel (Apr 05 2020 at 15:11):In particular, in Coq you can already get some powerful automation. I haven't checked them out in the context of diagrams specifically, but I wouldn't be surprised if there were some tactics that do rewriting for diagrams in monoidal categories automatically
Fabrizio Genovese (Apr 05 2020 at 15:14):Yes, I was thinking about this while reading through the discussion. For what it's the current state of the art our best shot would probably be writing an awful amount of tactics to make things bearable
Verity Scheel (Apr 05 2020 at 18:35):@Fabrizio Genovese I started working on a web program recently to take apart and rewrite expressions, is this kind of what you were thinking of? https://monoidmusician.github.io/dhall-purescript/pontifex.html (It's a very rough sketch and I don't have instructions yet, but you can set some axioms at the beginning, and the click the button to manipulate magmas in • by clicking on (sub)expressions and selecting relevant equations to apply to them, then click on the next subexpression to continue rewriting.)
Verity Scheel (Apr 05 2020 at 18:38):I hope to make it into a toy dependent type theory eventually, but obviously that's a lot more work. Right now it's just a little bit of logic with a simple syntax for magmas.
Fabrizio Genovese (Apr 05 2020 at 18:38):More or less, yes.So something similar happens in a theorem prover, with the difference that there is definitely a lot of bookkeeping to do which, in many circumnstances, could be automated
Fabrizio Genovese (Apr 05 2020 at 18:38):But what I mean is really having something to manipulate terms _within_ a proof in, say Idris or COQ
Fabrizio Genovese (Apr 05 2020 at 18:39):There are two layers here: terms in the proof assistant --> terms in the theory you are using the proof assistant on. I'd like to have such an editor for the first layer, more than for the second :slight_smile:
Verity Scheel (Apr 05 2020 at 18:44):Hmm I'm not quite sure what the distinction in, but ideally it could work for both. To be clear, working on magmas is just the initial prototype, but in theory it could work for Coq, Lean, Idris, Agda syntax, once I develop the theory.
Verity Scheel (Apr 05 2020 at 18:45):In the distant future, this would be just one kind of pluggable interface for the proof assistant :)
Andre Knispel (Apr 05 2020 at 19:56):This is cool, but in Coq you can actually do automated rewriting already. You can focus on smaller terms and do some rewriting on them, and then you can also give it a bunch of rules for rewriting and just automatically rewrite "as much as possible". So I'd say this is more of a nice graphical frontend, but it doesn't make things easier really
Andre Knispel (Apr 05 2020 at 19:58):I think what @Fabrizio Genovese wants already exists in Coq
Andre Knispel (Apr 05 2020 at 19:59):(other than that doing it graphically might be a little bit nicer)
Andre Knispel (Apr 05 2020 at 20:00):And actually it also exists in Agda and Idris, but to a lesser extent
David Michael Roberts (Apr 07 2020 at 00:17):Reid Barton said:
"Just use universes" is (or should be) the standard solution, and yes it leaves unaddressed some questions about whether or not some universal properties are invariant of the choice of ambient universe, but this is mostly a question about how you apply category theory to other areas (say commutative algebra), and where you really need it, you can check it by hand.
Zhen Lin Low wrote a paper about this: https://arxiv.org/abs/1304.5227
David Michael Roberts (Apr 07 2020 at 00:17):The Grothendieck universe axiom asserts that every set is a member of some set-theoretic universe U that is itself a set. One can then work with entities like the category of all U-sets or even the category of all locally U-small categories, where U is an "arbitrary but fixed" universe, all without worrying about which set-theoretic operations one may legitimately apply to these entities. Unfortunately, as soon as one allows the possibility of changing U, one also has to face the fact that universal constructions such as limits or adjoints or Kan extensions could, in principle, depend on the parameter U. We will prove this is not the case for adjoints of accessible functors between locally presentable categories (and hence, limits and Kan extensions), making explicit the idea that "bounded" constructions do not depend on the choice of U.