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.
Mike Shulman (Jan 28 2021 at 01:48):Ok, let's inaugurate this stream. The idea was for people to share something in personal threads about what they're working on right now, following on what @John Baez did in another stream. So here's what I'm working on right now research-wise:
Finish The univalence principle with Benedikt Ahrens and Paige North, a much longer elaboration of A Higher Structure Identity Principle.
<redacted>
Revise and submit All (∞,1)-toposes have strict univalent universes for publication.
Revise Constructing symmetric monoidal bicategories functorially (with Linde Wester Hansen), Linear logic for constructive mathematics, and A practical type theory for symmetric monoidal categories based on referee reports.
Expand my categorical logic notes into a textbook.
Various less-well-defined pending projects about HoTT and its semantics, including modal dependent type theory (with Dan Licata and Mitchell Riley), modeling HITs, modeling cubical type theories, modeling HoTT in elementary/realizability (∞,1)-toposes, stack semantics of 1-toposes, and impredicative constructions of HITs.
A couple of unfinished projects involving -autonomous categories.
John Baez (Jan 28 2021 at 02:16):Do I dare ask where you're publishing "Constructing symmetric monoidal bicategories functorially"?
This is a paper I've been using lately...
John Baez (Jan 28 2021 at 02:16):Textbook on categorical logic? Cool!
Mike Shulman (Jan 28 2021 at 03:35):John Baez said:
Do I dare ask where you're publishing "Constructing symmetric monoidal bicategories functorially"?
I don't know; do you? (-;
We submitted it to Compositionality, and we got one of those annoying referee reports that almost makes me wish they had just rejected it out of hand, basically saying "This is a nice paper, but I wish you had written a different one, so would you please go write the paper I wanted to read instead?" At least with a clean rejection you can submit it somewhere else immediately without feeling guilty.
If the referee (or editor) happens to be reading this, don't take it personally! I'm sure I've written plenty of referee reports in my time that the authors found annoying. And often it's the annoying reports that turn out to improve the paper the most... after you get over your annoyance and sit down to do something about them. (-:
Mike Shulman (Jan 28 2021 at 03:39):The textbook on categorical logic was supposed to be my sabbatical project for this year. But I got so caught up in <redacted> that I haven't even started it yet.
Fawzi Hreiki (Jan 28 2021 at 10:22):Will the textbook be primarily on type theory (as the notes are) or do you plan to have some model-theoretic stuff in there too?
Ivan Di Liberti (Jan 28 2021 at 12:17):Mike Shulman said:
- Expand my categorical logic notes into a textbook.
Hello Mike,
This is something I have been thinking for a long time, and even considering to start writing such a thing. Yet, I consider this as a very hard project. Categorical logic is many things, and more importantly it is a collection of point of views (type theory, universal algebra, functorial semantics, axiomatizations of categories of structures), it is also "many communities" to pay tribute to (https://diliberti.github.io/Read/Read.html#cl)... my honest opinion is that in a way, we need more a Handbook of Categorical Logic then a book whose title is "Categorical Logic". In both cases, I would love to collaborate to such a project.
Nathanael Arkor (Jan 28 2021 at 15:05):On a similar note, I am very fond of categorical logic and type theory and have found existing textbooks to be dissatifying (tending to be too narrow in focus, be insufficiently thorough, or be simply not up to date with modern developments). I read through your notes a while ago, and enjoyed the presentation. I would be happy to volunteer to proof read drafts of the new/updated sections.
Mike Shulman (Jan 28 2021 at 15:43):Thanks for the offer, @Nathanael Arkor!
Mike Shulman (Jan 28 2021 at 15:46):@Ivan Di Liberti I totally agree that categorical logic is a collection of points of views. My notes and hoped-for textbook were explicitly designed to present one point of view that I felt was lacking from the literature -- hence, in fact, why the working title is "Categorical logic from a categorical point of view"! I'm doing my best to respect and mention other points of view, but I want the presentation to be coherent from a particular one, which the reader can then contrast themselves with other presentations by other authors who are more qualified to present other points of view. For the same reason, though I appreciate the offer of help, this is one project that I want to do all on my own, because I have a fairly coherent point of view and I don't want to have to compromise it. However, I totally agree that a "Handbook of Categorical Logic" would also be a useful thing, if someone else (hint, hint) wanted to organize it.
Mike Shulman (Jan 28 2021 at 15:48):@Fawzi Hreiki I'm not quite sure what you mean by "model-theoretic stuff". The notes are already focused on the categorical models of type theory rather than the syntax. If you mean the subject that's traditionally called model theory, then no, I'm not going to write about that.
Mike Shulman (Jan 28 2021 at 15:50):Mike Shulman said:
And often it's the annoying reports that turn out to improve the paper the most... after you get over your annoyance and sit down to do something about them. (-:
By the way, since I mentioned it, this is one of the reasons I still believe in single-blind peer review: it makes it easier to give "annoying" but helpful/necessary reviews.
Fawzi Hreiki (Jan 28 2021 at 16:07):Well I guess the way I understand it, there are two notions or layers of model theory in categorical logic.
There’s the question of presenting certain kinds of categories syntactically (via generators and relations) and reasoning internal to them (using deduction rules).
So, like how we can present and reason in CCCs using lambda calculus.
There’s also the question of studying what the corresponding categories of models look like (by homming into sets or some other ‘big’ category).
A lot has been done on the model theory of ‘lower strength’ logics (e.g. propositional, algebraic, predicate) but I haven’t really seen much on the model theory of higher or dependent types.
Fawzi Hreiki (Jan 28 2021 at 16:11):A classical example is of course Stone duality for propositional logic, or Gabriel-Ulmer duality for essentially algebraic logic.
Fawzi Hreiki (Jan 28 2021 at 16:12):But maybe as we go up in the strength hierarchy, the categories of models become less interesting than what the syntactic categories themselves look like (since the syntactic categories are becoming ‘bigger’ and the categories of models ‘smaller’)
Mike Shulman (Jan 28 2021 at 16:38):Ah yes. I don't think I have an opinion on whether that kind of model theory is interesting, but it's not what I was planning to write about.
Ivan Di Liberti (Jan 28 2021 at 16:50):Mike Shulman said:
Ivan Di Liberti I totally agree that categorical logic is a collection of points of views. My notes and hoped-for textbook were explicitly designed to present one point of view that I felt was lacking from the literature -- hence, in fact, why the working title is "Categorical logic from a categorical point of view"! I'm doing my best to respect and mention other points of view, but I want the presentation to be coherent from a particular one, which the reader can then contrast themselves with other presentations by other authors who are more qualified to present other points of view. For the same reason, though I appreciate the offer of help, this is one project that I want to do all on my own, because I have a fairly coherent point of view and I don't want to have to compromise it. However, I totally agree that a "Handbook of Categorical Logic" would also be a useful thing, if someone else (hint, hint) wanted to organize it.
I totally see your point. CatLog from a categorical point of view is definitely missing in the panorama!
Simon Burton (Jan 28 2021 at 23:45):Mike Shulman said:
A practical type theory for symmetric monoidal categories
I'd really like to understand this better... have you done a talk on it?
The example equation "tr(fg)=...=tr(gf)" on page 4: it looks like it goes in the reverse order to the string diagram calculation in Figure 1. Is that right? If so maybe you should change the order so that it agrees with Figure 1.
Mike Shulman (Jan 29 2021 at 04:20):@Simon Burton You're right, thanks. I'll change Figure 1 instead, since the incomprehensible proof is also in the tr(fg)=...=tr(gf) order. I haven't given any talks about this paper, unfortunately.
Mike Shulman (Mar 07 2021 at 16:10):Here's an update on what I'm working on, now without content-related spoilers.
D.G. Berry (Mar 07 2021 at 16:17):Back in December I read your paper on LL for constructive Mathematics, and found it most interesting. I am working on developing a computational interpretation of it as personal side-project.
Mike Shulman (Mar 07 2021 at 21:41):Cool! I'd be interested to hear what you're thinking about.
D.G. Berry (Mar 08 2021 at 12:15):It struck me at the time that it bears a similarity to the Dual Calculus (a la Wadler) however with a different interaction between terms and coterms. I am working on formulating a (co)term structure for it (which will not be "complete" (in some sense of the word) in the first instance) to investigate its reduction properties. The Chu construction could likely serve as a syntactic translation from the putative calculus into the STLC. I have not done much yet as I have been solidifying my understanding of the various basic properties and proofs of the STLC. From a more categorical perspective I have been thinking about how it could be modelled but I am less clear on the details on this side of things.
Mike Shulman (Mar 08 2021 at 16:37):Thanks! I look forward to seeing it.
D.G. Berry (Mar 08 2021 at 19:14):I am only a MSc student so it is unlikely to go anywhere (and it is not directly related to my proposed PhD research topic).
James Wood (Mar 08 2021 at 20:22):@D.G. Berry I'm interested in similar things at the moment (both Mike's work and dual calculus/μ̃μ/L). When you have a dual calculus, what's the motivation for translating it into (pairs of) STLC?
D.G. Berry (Mar 08 2021 at 21:18):This only very briefly occurred to me when writing out my earlier message so I have not thought about it much. Dual calculi have been interpreted using CPS translations; and, my thinking was that the Chu construction might correspond to something similar. My putative calculus appears to not be pre-evidently linear but does appear to have linear-like properties (I believe that this is down to the infinitely-contraposable nature of implication). This linear-like structure could somehow bear on the nature of this translation compared to the classical CPS translations.
James Wood (Mar 08 2021 at 22:13):My vision of the Chu-Shulman translation (if that's what we're to call it) is as one of these translations that isn't often used directly, but rather we frequently work in its image. Other examples are the Gödel-Gentzen translation (showing a way of weakening statements in intuitionistic logic) and the translation from extensional to intensional type theory that gives us setoids. I'd like to see other uses, though!
James Wood (Mar 08 2021 at 22:21):At least the Chu-Shulman translation has the advantage that its source theory is both expressive and well behaved, which gives it a better chance of being used directly than the other two I mentioned.
Mike Shulman (Mar 09 2021 at 00:08):At the moment I'm favoring the term "antithesis translation/interpretation".
Mike Shulman (Mar 09 2021 at 00:09):The idea being that each proposition is translated to an assertion together with its antithesis (polar opposite).
Valeria de Paiva (Mar 09 2021 at 15:21):Mike Shulman said:
The idea being that each proposition is translated to an assertion together with its antithesis (polar opposite).
well, I thought this (thinking of assertion+anti-assertions) was more like Dialectica than Chu, as one of the differences between the constructions is exactly that the relations in Dialectica allow you to negate, as oppose to simply transpose, the matrix of truth-values.
But indeed very interesting the idea of connecting this idea to the Herbelin's calculus.
Mike Shulman (Mar 09 2021 at 16:44):I'm using "antithesis" to refer specifically to the Chu construction where the dualizing object is absurdity. In that case, transposition really is a form of negation.
Valeria de Paiva (Mar 09 2021 at 21:20):Mike Shulman said:
I'm using "antithesis" to refer specifically to the Chu construction where the dualizing object is absurdity. In that case, transposition really is a form of negation.
Note that I still haven't found the different emojis to say "I heard you, thanks for replying" as opposed to "I heard you and agree with you, thanks".
Mike Shulman (Mar 09 2021 at 22:43):Thankfully, some clever person a while ago invented language, so we aren't restricted to the meanings we can express with pictures.
D.G. Berry (Mar 09 2021 at 23:48):Are you suggesting that emojis are some kind of ......... regression???
Mike Shulman (Mar 10 2021 at 01:46):Yes.
Mike Shulman (Mar 10 2021 at 01:47):Along with all the other pictograms that now infect the Internet in place of words.
Jason Erbele (Mar 10 2021 at 02:21):My cell phone understands this intuitively: when receiving text messages, the entire message regresses to an unintelligible jumble of old-school cartoon swearword replacements whenever emoji are included in the message.
David Michael Roberts (Mar 11 2021 at 00:02):Mine is an old-style phone that renders each emjoi as a pair of squares. I got a message response yesterday that was just eight squares in a row. I assumed it was a positive reaction :-)
Matteo Capucci (he/him) (Mar 11 2021 at 08:44):but did the squares commute? :grinning_face_with_smiling_eyes:
Mike Shulman (Apr 12 2021 at 19:39):On that note, here's another update on my work:
Fawzi Hreiki (Apr 12 2021 at 19:45):Will there be slides (or notes) for the talk on large cardinals?
Nathanael Arkor (Apr 12 2021 at 19:49):Fawzi Hreiki said:
Will there be slides (or notes) for the talk on large cardinals?
Even better, the seminar is public (and in ~40 minutes).
Notification Bot (Apr 12 2021 at 21:44):This topic was moved by Nathanael Arkor to #general: off-topic > emoji
Mike Shulman (Apr 13 2021 at 00:02):http://home.sandiego.edu/~shulman/papers/wisconsin-lgcard.pdf
Mike Shulman (Apr 13 2021 at 00:04):There's also a recording and slides posted at the seminar page.
Nick Smith (Jun 08 2021 at 05:42):@Mike Shulman Is your categorical logic book still likely to happen this year? I’m very interested in studying both multicategories and type theories so I’ve been excited for it 🙂
Mike Shulman (Jun 08 2021 at 12:32):No, sorry. I ended up spending the year on other projects.
Nick Smith (Jun 08 2021 at 22:23):Ah, that’s a shame. Fair enough!
Mike Shulman (Jun 09 2021 at 00:24):The more charitable version is that I spent (some of) the year doing groundwork for some of the remaining chapters. For instance, working on a polycategorical version of linear logic with exponentials (soon to appear, I hope), tying up HoTT with the stack semantics of an elementary topos, etc. (-:
Nick Smith (Jun 09 2021 at 04:05):Well, when you put it that way, I’m now even MORE excited for the eventual book. Looking forward to 2022! 😉
Henry Story (Jun 10 2021 at 14:09):Perhaps you could put up a reading list for people to prepare (if they have spare time) for the book :-)
Mike Shulman (Jun 30 2021 at 05:05):Henry Story said:
Perhaps you could put up a reading list for people to prepare (if they have spare time) for the book :-)
Well, now that https://arxiv.org/abs/2106.15042 is out, you can read that. I expect it will greatly influence the unwritten chapter 3 of the book. Possibly https://arxiv.org/abs/1911.00818 will too.
David Michael Roberts (Jul 01 2021 at 01:49):This is a slight sidetrack, but maybe there's a link: In Affine logic for constructive mathematics https://arxiv.org/abs/1805.07518 you talk about "affine sets", which turn out to be something rather interesting. Have you ever thought about what "relevant sets" would be? That is, you lose weakening, but add contraction, in the underlying logic? I have been fooling around with monoidal categories with diagonals for various reasons, and these should give semantics for certain relevance logics (variations on https://ncatlab.org/nlab/show/relevance+monoidal+category, with possibly fewer assumptions, based on the flavour of relevance logic), but I can't exactly say what a "relevant set" is. Possibly this is a big and gnarly topic, but do you have any intuition (hah)?
Valeria de Paiva (Jul 01 2021 at 03:56):David, are you aware of Masaru Shirahata's phd thesis, written under Grisha Mints?https://www.semanticscholar.org/paper/Linear-set-theory-Shirahata/c6fb6ed5fc0f43b7e18fbc852c3170e11056745b
David Michael Roberts (Jul 01 2021 at 04:04):@Valeria de Paiva no, I'm not! I haven't done an exhaustive literature search, since it's not a big project, and I was originally just happy having examples of categories with certain properties. But I really do need contraction, so linear logic is not quite the thing I need!
Mike Shulman (Jul 01 2021 at 14:28):Well, you can perform the same construction that I did to get "affine sets" on any linear hyperdoctrine, including any "relevance" one. As to where a relevance hyperdoctrine might come from, I have fewer ideas. I don't know of an obvious instance of a Chu or Dialectica construction that would end up being relevance, but I guess you could take the canonical indexing of a relevance monoidal category like over Set.
Mike Shulman (Sep 07 2021 at 17:09):Our semester just started and I've been pretty busy with teaching and bureaucracy. When I have a chance to work, my to-do list looks like:
Leopold Schlicht (Sep 07 2021 at 17:24):Will your talk be recorded? Which flavor of type theory does your proof assistant implement and how does it differ from existing proof assistants?
Mike Shulman (Sep 07 2021 at 17:42):The JMM is planned to be in person. I don't know whether there are any plans to record talks.
Nathanael Arkor (Sep 07 2021 at 18:33):
- Writing my own proof assistant.
I am excited to see what you come up with (and look forward to hearing some more details).
Mike Shulman (Sep 07 2021 at 19:54):Well, it's been a very educational experience. I kind of want to recommend that everyone interested in type theory should try writing their own toy proof assistant at some point. (I probably wouldn't recommend trying to implement higher-order unification, though. Ugh.)
Mike Shulman (Sep 07 2021 at 19:55):Personally, I started because I was inventing a new type theory that I wanted to play around with in a proof assistant, and I wasn't able to find any existing tool that would let me do that. (Which doesn't necessarily mean there aren't any -- the conversation after @Florian Rabe's colloquium made me think that I should give MMT another try.)
Mike Shulman (Sep 07 2021 at 19:58):Since I've been in this situation several times before, of wanting to play around with a new type theory but not having any way to do it, I decided to try to implement something a bit more general that could be used as a framework library to implement multiple different object languages.
Mike Shulman (Sep 07 2021 at 19:59):So the underlying framework type theory is, at the moment, a plain dependent type theory, but playing the role of a logical framework in which to implement object theories with specified typechecking and reduction behavior.
Mike Shulman (Sep 07 2021 at 20:01):This idea is similar to various other extant frameworks like Isabelle, Andromeda, Dedukti, Lambdapi, MMT, and I'm sure others. But I wasn't able to make any of these that I tried do exactly what I wanted.
Nick Hu (Sep 07 2021 at 20:15):Will you share any tidbits about how you're going to implement it? :grinning:
Nathanael Arkor (Sep 07 2021 at 20:22):Personally, I started because I was inventing a new type theory that I wanted to play around with in a proof assistant, and I wasn't able to find any existing tool that would let me do that.
Yes, I think there's a fast-growing need for such a tool. I wanted to do something similar a couple of years ago, and wrote a type-checker/interpreter whose metatheory was based on a higher-order version of generalised algebraic theories with rewrites, but it becomes obvious very quickly how much work is required to move from "type-checker" to "proof assistant".
Nathanael Arkor (Sep 07 2021 at 20:22):There does seem to be a trend in that direction recently, but I also feel none of them quite caters to what I'm looking for.
John Baez (Sep 07 2021 at 21:22):Mike Shulman said:
Since I've been in this situation several times before, of wanting to play around with a new type theory but not having any way to do it, I decided to try to implement something a bit more general that could be used as a framework library to implement multiple different object languages.
Typical category theorist move. :upside_down:
Mike Shulman (Sep 07 2021 at 22:39):John Baez said:
Typical category theorist move. :upside_down:
I'm glad someone else said that and not me. I was definitely thinking it.
Mike Shulman (Sep 07 2021 at 22:41):The main thing I was missing in the existing tools was more flexibility in specifying my normalization algorithm. In particular, I wanted to specify "rewriting" or "reduction" rules that none of the existing tools I tried would accept as fitting into their rigid notion of what a "rewrite" is. So my system allows the implementer of an object theory to write more or less arbitrary code to specify the result of a reduction on an object-language symbol.
Mike Shulman (Sep 07 2021 at 22:49):Also I generally prefer Coq-like tactic proofs to Agda-style hole-filling development, but it seems that the former is generally underrepresented in proof assistants, and especially in general frameworks.
David Michael Roberts (Sep 07 2021 at 23:50):So it's something morally like Metamath but for type theories? ;-)
Mike Shulman (Sep 08 2021 at 00:03):I'm not really familiar with metamath, but perhaps.
David Michael Roberts (Sep 08 2021 at 00:20):In the sense that it's more of a framework to do things, like set.mm is (roughly) a ZFC proof assistant, but there are other, less extensive projects, like NF, HOL, IZF, all built in Metamath.
Mike Shulman (Sep 08 2021 at 13:21):Ok sure, and I think that's also the idea of the other generic projects like Isabelle, Andromeda, MMT, etc.
Jacques Carette (Sep 08 2021 at 14:04):Isabelle lets you use arbitrary ML code; MMT lets you use Scala instead. That ends up making a difference (I tried doing things with MMT, but I really don't like the code style that Scala forces on me, and abandoned that direction). It's too bad that Andromeda development seems stalled right now, as it was quite promising.
Henry Story (Sep 08 2021 at 15:19):Scala3 has a much stronger formal underpinning (see this more recent paper). I wonder if that is going to make a difference to MMT.
Mike Shulman (Sep 08 2021 at 15:20):Interesting, thanks for the report. My current plan will involve arbitrary OCaml code. I don't fully understand Isabelle, but insofar as I do, I am tempted to describe Platt (the working title for my proof assistant) as "like Isabelle but with dependent types".
Mike Shulman (Sep 08 2021 at 15:21):Andromeda also looked very promising to me. But when I tried actually using it I got stuck, not just because it's unfinished, but also because despite the fact that it "supports" arbitrary equality rules in theory, to make something usable in practice it seems you're mostly restricted to equalities that fit within the supplied equality-checking algorithm, and mine didn't.
Mike Shulman (Sep 08 2021 at 15:22):Also Andromeda is (currently) restricted to a single sort ("type"), whereas I'm often interested in type theories with more than one sort.
Jacques Carette (Sep 08 2021 at 15:35):@Henry Story I expect that it will make no difference whatsoever in day-to-day use, just some meta-level increased confidence. Scala is great, and I make a point of exposing many students to it when I teach my grad PL semantics class. I just personally don't like its style. [The same way Mike prefers tactic-style over hole-style; it is exactly that, a stylistic preference.]
Henry Story (Sep 08 2021 at 15:37):fair enough. I am using Scala and quite happy to program web servers and clients with it; and it is what dissolve my preconceptions that category theory was abstract nonsense. :-)
But I would love to have something like Agda that compiles to Scala, so I could do proofs and code.
Mike Shulman (Sep 08 2021 at 15:38):Well, I actually think that tactic-style has objective advantages over hole-style. But, of course, others may have other opinions. (-:
Valery Isaev (Sep 08 2021 at 15:41):Mike Shulman said:
Well, I actually think that tactic-style has objective advantages over hole-style. But, of course, others may have other opinions. (-:
Do you mind sharing them?
Mike Shulman (Sep 08 2021 at 15:49):The main one is that it records the process by which the proof term was constructed, so that it can be read, replayed, and modified.
Mike Shulman (Sep 08 2021 at 15:50):Of course there's also the potential to write fancy tactics, all the way up to ssreflect and Chlipala style; I don't tend to like tactics like that, but the potential power is there. Agda has reflection, but I don't think it can achieve quite that level.
Mike Shulman (Sep 08 2021 at 15:51):Recently a student and I have been looking at "equational reasoning" style proofs in Agda, and even with all the tricks you can play to make them as convenient as possible, in my book they just don't approach the ease of rewrite associativity in Coq.
Valery Isaev (Sep 08 2021 at 15:52):Mike Shulman said:
Of course there's also the potential to write fancy tactics, all the way up to ssreflect and Chlipala style; I don't tend to like tactics like that, but the potential power is there. Agda has reflection, but I don't think it can achieve quite that level.
I don't see why it couldn't.
Nathanael Arkor (Sep 08 2021 at 15:54):Mike Shulman said:
Recently a student and I have been looking at "equational reasoning" style proofs in Agda, and even with all the tricks you can play to make them as convenient as possible, in my book they just don't approach the ease of
rewrite associativityin Coq.
This seems more a complaint about Agda, rather than the philosophy behind the style of proof in Agda.
Nathanael Arkor (Sep 08 2021 at 15:56):In terms of ease of use, languages like Isabelle and Coq have a large advantage over Agda in that they're much more mature.
Henry Story (Sep 08 2021 at 15:57):Does Lean not also use Reflection for its tactics?
(But they don't have Cubical)
Nathanael Arkor (Sep 08 2021 at 15:57):Which is not to make a point in either one's favour, but rather to point out that comparing the philosophy of proof styles by making direct comparison to implementations is not particularly representatitive.
Jacques Carette (Sep 08 2021 at 16:06):There are indeed many different 'tactic' styles. The styles that hide a lot of computation in an unobservable medium annoy me - it's all black magic that does not provide much explanation. Proofs should have explanatory power (they do in normal mathematics). Proofs whose contents is merely "it's true, really, I've checked, you don't need to worry about it" feel rather unsatisfying. PVS's grind is perhaps the worst offender!
Even though I have published a lot of papers on meta-programming, somehow the MTAC language as a means to give instructions on how to build my proofs doesn't really resonate with me. I agree 100% that Agda hides that part, because that is mostly done in an invisible way in the IDE (the equivalent of 'intro' and 'intros' and 'case split' and ... all exist in Agda too, but they are IDE "gestures" rather that residuated in the proof).
As it turns out, for the kinds of results that I'm interested in, the explicit proof terms are very important to me. So I like seeing them, Agda/Idris style. Whether it's PL meta-theory or category theory in a constructive setting, I like to be forced to do explicit equational proofs. One huge advantage: when doing n-category theory, one can immediately see what will be hard work in (n+1)-category theory. This is also a huge disadvantage if you have no intention of going there! It's a similar issue with strict/weak, for that matter.
Note that, for the exact example of associativity, that can be done in Agda, in multiple ways.
Personally, I'm very happy for the proliferation of systems. The design space is huge, and it should be well explored. And I don't think there is a global optimum, just local ones, that cater to different styles.
Jacques Carette (Sep 08 2021 at 16:10):As to using reflection (in Agda): it is indeed extremely powerful, and people have just started exploring. The one thing it can't do is to create new top-level bindings, and that was exactly the kind of meta-programming I was looking for... But as far as proof-level meta-programming, as far as I can tell, it's merely a matter of effort to program it all, there are no issues with the implementation that would block things.
Mike Shulman (Sep 08 2021 at 16:40):Tactics don't make proof terms invisible. You always have the option to write them out explicitly, or to print them after you've constructed them with tactics.
Mike Shulman (Sep 08 2021 at 16:41):Andrej Bauer likes to point out that in no usable proof assistant do you actually write "proof terms" in the actual underlying formal system; there is always a computation step even if it's just elaboration and unification. Given that, why not give the user full access to that computational level?
Mike Shulman (Sep 08 2021 at 16:44):I don't think even a reflection-style proof in Agda, no matter how fancy it can get, can be "replayed" in the same way you can step through a tactic proof in Coq or Lean. This is a big advantage because simply reading a proof assistant file, whether it's a tactic proof script or a proof term, is very hard to understand directly, especially for a working mathematician. Stepping through it and seeing the givens and goals at each stage is much closer to the way mathematicians think when they read or write a proof. Yes, this is a stylistic issue, but just as a large enough quantitative difference becomes qualitative, a large enough stylistic difference becomes objective.
Mike Shulman (Sep 08 2021 at 16:47):Perhaps you can claim that the only reason Coq has many more big formalization projects (the odd order theorem, the four-color theorem, CompCert, FIat Crypto) is that it's older and more mature. But I think it's also significant that Lean, which is also tactic-based and much younger than Agda, has already had an astonishing degree of uptake among "working" mathematicians.
Mike Shulman (Sep 08 2021 at 16:47):Anyway, you asked. (-:
Mike Shulman (Sep 08 2021 at 16:59):Nathanael Arkor said:
Which is not to make a point in either one's favour, but rather to point out that comparing the philosophy of proof styles by making direct comparison to implementations is not particularly representatitive.
Well, the available implementations are all we have to talk about. If someone claims that the disadvantages of hole-style proofs are not intrinsic to that style, then I would say it's incumbent on them to prove it by exhibiting an implementation that avoids them. (-:
Jacques Carette (Sep 08 2021 at 17:04):I "learned" the same lesson from Andrej as well. He is indeed correct. And I agree that having first-class access to elaboration is an excellent idea. [Idris pioneered that, BTW. Tactics a la LCF didn't quite go that far.
And you are correct on the next point as well: Agda-style proofs cannot be replayed. The end result is that I feel like I can read my Agda proofs directly, while for Coq proofs, one is more-or-less obligated to interactively replay them.
It is also impossible to deny the success (size-wise) of Coq and Lean. Lean has the huge advantage of having core developers (on the language side) who have actively learned from the pros/cons of its predecessors, as well as having the enormous advantage of breaking backwards compatibility (4 times...). Coq keeps losing people when they do the same - different communities react differently. (One can see the same in MathOverflow vs StackOverflow.)
One still has to be careful. This debate has much in common with the OO vs functional debate. The debate is healthy when it is being held by people who have genuinely tried the alternatives and made a choice, evil when it's done by a 'fan'.
Nick Hu (Sep 08 2021 at 17:10):Lean also has the benefit of an aggressive guerilla marketing campaign
Mike Shulman (Sep 08 2021 at 17:15):I don't see why any given proof assistant has to restrict itself to one style. The comparison to OO vs functional programming is a propos -- some of the nicest (IMHO) modern languages, like Scala and OCaml, incorporate both OO and functional features, allowing the user to choose which is most appropriate for their particular situation or stylistic preference.
Mike Shulman (Sep 08 2021 at 17:17):For the record, I have used Agda myself -- not as extensively as Coq, but for several fairly substantial projects -- and there are definitely situations in which it shines comparatively. For instance, working with large families of mutual inductive or inductive-inductive types is much more pleasant/possible in Agda. Of course a tactic-based proof assistant could provide better support for such things than Coq does, but I suspect there are some intrinsic advantages to hole-style in that situation.
Kenji Maillard (Sep 08 2021 at 17:22):Talking about varieties of styles to write down proofs in a proof assistant, Coq has at least 5 quite distinct tactic languages/metalanguages (Ltac, Ltac2, MtacX, Elpi, Gallina through Metacoq's plugin). And you can get closer to agda style program/proof writing with Equations.
Mike Shulman (Sep 08 2021 at 17:25):Ideally, I would like Platt to support both styles. I also have an idea for a sort of intermediate style that works with proof terms and holes but records the sequence of hole-filling, so that with proper tool support you can view the context and type of each hole along with the term that filled it. The idea is that if you write just f ? a, then ? is a hole that's reported to the user with its context and type. But when you "fill" it with a term like g a b, instead of that term replacing the hole to get f (g a b) a, it comes after it delimited by a semicolon (or something): f ? a ; g a b. Semantically this means the stame as f (g a b) a, so the semicolon is sort of a backwards let-binding akin to let ? = g a b in f ? a. The difference is that the type of ? is still inferred from its use point in f ? a, with the term g a b being checked against that type. Multiple holes can also be chained, with the same term being obtainable as f ? a ; g ? b ; a or f ? ? ; g a b ; a; the question-marks "go onto a queue" as they are encountered and semicolons fill them in order.
Mike Shulman (Sep 08 2021 at 17:26):Then in the process of checking the proof, the proof assistant knows the types of each ? and can display them to the user with a suitable interface. I did some experiments with this, using an emacs mode with commands to move around between the ?s in a completed term and show their types, and I found it quite pleasant.
Mike Shulman (Feb 06 2022 at 01:57):It's been a long time since I posted an update on my work, because fall semester happened. But I'm teaching less this semester, so I'm hoping to make some progress on my to-do list:
David Michael Roberts (Feb 06 2022 at 02:09):@Mike Shulman do you know if your JMM talk will be recorded and made available?
Mike Shulman (Feb 06 2022 at 18:01):I haven't heard anything one way or the other.
Mike Shulman (Apr 07 2022 at 03:42):Something was said about recordings of the JMM talks being available later, so we'll see. In the meantime here are my slides.
Mike Shulman (Apr 07 2022 at 03:44):The title for my HoTTEST talks is "Towards Third-Generation HOTT", and the abstract is on the HoTTEST page. This is the project that I've been posting as "<redacted>" all this time, because I wasn't sure it would come to anything. But although it's still not quite finished, I'm now confident enough that the unresolved details will work out one way or another.
John Baez (Apr 07 2022 at 04:00):Can you say anything about what "third-generation" means here, or is it still top secret?
John Baez (Apr 07 2022 at 04:00):Something vague would suffice, no need to give away your tricks.
John Baez (Apr 07 2022 at 04:01):Oh yeah, and what's "second-generation" HoTT?
Mike Shulman (Apr 07 2022 at 04:09):I'm thinking of Book HoTT as "first-generation" and cubical type theories as "second-generation". So the new formalism we're working on, which I sketched in the abstract, would be a third generation.
Zhen Lin Low (Apr 07 2022 at 04:31):I like this programming metaphor very much!
Zhen Lin Low (Apr 07 2022 at 04:32):Incidentally I think Thomas Forster talks about mainstream set theory as the "study of wellfoundedness", in contrast to the non-wellfounded set theory he likes to think about.
David Michael Roberts (Apr 07 2022 at 04:57):The difference between HoTT and HOTT is ... not confusing at all ? :-P
Jacques Carette (Apr 07 2022 at 11:53):Just read your JMM slides - I thoroughly enjoyed them. You make an extremely convincing argument.
Tim Hosgood (Apr 07 2022 at 11:57):oh no, i've barely worked through the HoTT book, so i'm already two generations behind before having even properly started! :expressionless:
Mike Shulman (Apr 07 2022 at 14:36):Fortunately, one of the goals of HOTT is to be easier to work with than either of the first two generations, so if it works out, a newcomer should just be able to start there. But it'll probably be a while before anyone writes a third generation HOTT Book, so for now the first gen one is perfectly good.
Mike Shulman (Apr 07 2022 at 14:36):David Michael Roberts said:
The difference between HoTT and HOTT is ... not confusing at all ? :-P
Well, the not-so-secret goal is to take over the whole subject. (-:
Mike Shulman (Apr 07 2022 at 14:39):Zhen Lin Low said:
Incidentally I think Thomas Forster talks about mainstream set theory as the "study of wellfoundedness", in contrast to the non-wellfounded set theory he likes to think about.
Yes, this certainly isn't an original suggestion of mine. Another reference was suggested by one of the audience after the talk, Mathias I think.
John Baez (Apr 07 2022 at 16:24):After HoTT and HOTT there will be HÖTT - the heavy metal version.
Mike Shulman (Apr 07 2022 at 16:28):Or maybe HΩTT?
Zhen Lin Low (Apr 07 2022 at 16:29):Mike Shulman said:
Zhen Lin Low said:
Incidentally I think Thomas Forster talks about mainstream set theory as the "study of wellfoundedness", in contrast to the non-wellfounded set theory he likes to think about.
Yes, this certainly isn't an original suggestion of mine. Another reference was suggested by one of the audience after the talk, Mathias I think.
Interesting. Adrian Mathias was Thomas's advisor. It makes sense.
Jon Sterling (Apr 07 2022 at 16:59):@Mike Shulman Love your opening slides!
Mike Shulman (Apr 07 2022 at 16:59):I'm not surprised all the computer scientists like it when I say that math is like programming...
Jon Sterling (Apr 07 2022 at 17:07):Hahaha :) Well, the part I especially liked was "A bug in the compiler can be fixed, and most code is fine". I think that for reasons of publicity and trying to find a way to communicate the value of our work to outsiders, it has become very common for us to make mountains out of molehills of bugs and mistakes, and try and convince people they should give us a million dollars to decrease the "trusted base" of our tool or whatever, but the reality is that this basically never matters in practice. What matters is ergonomics, and making sure that the tool reflects the mental model of the mathematician.
John Baez (Apr 07 2022 at 18:00):Mike Shulman said:
Or maybe HΩTT?
You should save that one for last: "ultimate HoTT".
Jacques Carette (Apr 08 2022 at 12:57):Mike Shulman said:
I'm not surprised all the computer scientists like it when I say that math is like programming...
LOL. Actually, I'm much more interested in seeing math and CS cross-pollinate.
For example, while mathematicians have had the idea of 'a theory' (like the theory of monoids, groups, etc) for a long time, CS really refined it to the notion of an 'interface'. Math textbooks are sloppy about sometimes writing to the interface and sometimes using the underlying implementation details (because there's no checker for that stuff). Having implementation details spilling over everywhere is annoying.
There's a huge wealth of stuff where, strictly speaking, mathematicians and/or logicians were there first, but then stopped pursuing the ideas -- which the computer scientists then gladly picked up.
My co-authors and I touched on bits of this in our Mathematical Intelligencer paper Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge (it's open access).
Patrick Nicodemus (Apr 08 2022 at 14:02):Mike Shulman said:
Or maybe HΩTT?
I think this should be the final version, in keeping with the tradition of being used to denote the end, "from alpha to omega" :)
Patrick Nicodemus (Apr 08 2022 at 14:03):Oh, John already made this joke. My apologies.
Mike Shulman (May 11 2022 at 04:17):The Grothendieck conference has posted the schedule of talks, but as far as I can see they haven't posted the abstracts (yet). So here's mine:
Title: Lifting Grothendieck universes to Grothendieck toposes
Abstract: A Grothendieck topos is a category that behaves much like the category of sets, and in particular interprets constructive type theory. A Grothendieck universe is a set of sets giving rise to a small category that behaves much like the large category of all sets. It is thus natural to ask, if Grothendieck universes exist in sets, do Grothendieck toposes also contain analogous "universes"? This was shown for presheaf toposes by Hofmann and Streicher in 1997, and for all Grothendieck toposes by Streicher in 2005. However, Streicher's sheaf universes lack a "realignment" property that is needed for some applications, including the interpretation of cumulative universes in type theory. We will use a form of Quillen's small object argument, plus descent, to construct universes satisfying realignment in all Grothendieck toposes. This is joint work with Gratzer and Sterling.
(The paper is Strict universes for Grothendieck topoi.)
Mike Shulman (Jan 04 2023 at 21:11):Last semester I was teaching calculus and also thinking about proof assistant implementations, and as often happens when I think about two unrelated things my mind finds a way to relate them. In this case, it occurred to me that one reason integration-by-substitution is difficult is that it involves mentally solving a higher-order unification problem that's outside the pattern fragment. Too bad saying it that way doesn't help my students... (-:
Jacques Carette (Jan 04 2023 at 21:57):Did you also notice that first-year "solve this integral" problems are syntactic/intensional while the correctness theorems are all extensional? Perhaps also noticed that the proofs that various techniques are correct are in proof assistants (like Isabelle and HOL Light), but all the algorithms are only implemented in Computer Algebra Systems? This isn't an accident.
I'd also love to see "higher order unification" appear in math papers, not just CS papers.
Mike Shulman (Jan 04 2023 at 22:36):The algorithms for finding derivatives and antiderivatives are intensional, in that they operate on syntactic representatives of functions rather than on extensional mathematical functions. Is that what you mean?
Jacques Carette (Jan 05 2023 at 00:16):Yes.
Mike Shulman (Mar 07 2023 at 18:05):I haven't posted much here recently, partly because I've been spending a lot of time mentoring rather than working on my personal projects. But I just posted a note about Semantics of multimodal adjoint type theory, which I'm excited about as a step towards the goal of a satisfactory general modal dependent type theory. It doesn't introduce much new at the syntactic level, just puts together a couple of general modal type theories already in the literature, but the point is that this theory actually has the general semantics we would expect in diagrams of categories, despite the fact that there appear to be "extra left adjoints" in the syntax.
Graham Manuell (Mar 10 2023 at 16:06):You mention that there isn't an explicit construction in the literature of the category obtained by freely adding adjoints to a 2-category. I don't know if it'll be exactly what you need, but Lurdes Sousa and I are currently working on a paper that does something very much like this. (It is the generalisation of this paper from the order-enriched setting.)
Mike Shulman (Mar 11 2023 at 03:29):@Graham Manuell That's definitely related, thanks! Based on the abstract of the paper you linked to, it looks like it's different from what I would want in three ways: (1) order-enrichment rather than Cat-enrichment, (2) the adjunction units are identities, and (3) the original 2-category is assumed to have a calculus of lax fractions. It sounds like you're currently working on generalizing away from (1). Are you keeping (2) and (3)?
Graham Manuell (Mar 11 2023 at 12:14):The main point of the paper is generalising (1), but we are also thinking about generalising (2). We are definitely keeping (3) though, so if that is too restrictive for your setting, our work will unfortunately be of limited use to you.
Mike Shulman (Mar 11 2023 at 16:24):Ok, thanks. I haven't actually thought about which of the 2-categories that tend to arise in modal type theories might have a calculus of lax fractions. But ideally I would definitely like to understand the general case without an assumption like that.
Mike Shulman (Mar 11 2023 at 16:33):I'm planning to have some students work on the problem this summer, though.
Nathanael Arkor (Mar 11 2023 at 17:48):Mike Shulman said:
I'm planning to have some students work on the problem this summer, though.
Just in case you haven't come across it, Freely adjoining monoidal duals might be a useful reference. I expect it would be simpler to generalise that construction from the setting of monoids categories (essentially by adding colours) than to generalise Adjoining adjoints from the setting of locally-discrete 2-categories.
Nathanael Arkor (Mar 11 2023 at 17:50):(Though now I recall we discussed this topic before.)
Mike Shulman (Mar 11 2023 at 19:44):Thanks for reminding me of that. It's not exactly what I would want, though: their presentation seems to be almost tautological, in that they take the objects to be essentially freely generated by those of and a dual of , and then the morphisms to be freely generated by those of and a unit and counit, and then quotient by the obvious relations. I was hoping for something more like the adjoining-adjoints construction where the 2-cell representatives have an explicit "fence" form, even if the equivalence relation is specified by generators.
Christian Williams (Mar 11 2023 at 19:56):fence form?
Mike Shulman (Mar 12 2023 at 16:01):That's what they call the 2-cells in "Adjoining adjoints".
Matteo Capucci (he/him) (Mar 12 2023 at 17:08):It probably comes from the orders called fences
Ralph Sarkis (Mar 12 2023 at 17:20):That 6th equivalent condition came out of nowhere :mind_blown:
Mike Shulman (Mar 12 2023 at 17:39):Hmm, I think it could have been independently invented just because the diagrams look like a fence.
Mike Shulman (Dec 05 2023 at 02:37):Most of my time recently has been taken up with teaching, mentoring, and working on joint projects. But soon that should be lightening up a bit, in particular now that my paper with @Astra Kolomatskaia is about done. So I hope that further updates on other projects should be forthcoming shortly.
To start with, I'm giving a talk at Chapman University on January 31 at a conference entitled Is Philosophy Useful for Science, and/or Vice Versa?. My plan is to tell the story of how my work on Higher Observational Type Theory was influenced by philosophical considerations, specifically my desire to convince philosophers that homotopy type theory can be just as "autonomous" a foundation of mathematics as set theory is.
Mike Shulman (Dec 05 2023 at 05:26):Looks like @Evan Patterson is also speaking at the conference.
Evan Patterson (Dec 05 2023 at 05:47):Yes, I am looking forward to it, and to your talk in particular!
Mike Shulman (Dec 05 2023 at 06:14):I'm also curious to hear what you'll be talking about!
Evan Patterson (Dec 05 2023 at 06:30):I'm going to talk about how work on theories and models in philosophy of science influenced my thinking about scientific modeling and, conversely, how I think ideas from category theory and categorical logic could be relevant to debates in that field.
Here's my abstract:
Beginning with the logical positivists, the philosophical project to make sense of scientific theories and models using mathematical logic is now about a hundred years old. Although the project has had notable successes in "rationally reconstructing" various theories and models, the use of formal logic by working scientists remains extremely limited today. This state of affairs seems to be due to the impracticality of formalizing typical science in standard logic and to the lack of obvious benefit that would ensue to scientists by doing so. In this talk, I will argue that there is a significant opportunity to encourage greater use of formal logic in science by adopting modern techniques from categorical logic, the approach to logic based on category theory. I will explain how specific features of categorical logic, such as the ability to assemble "domain-specific" logics, the algebraization of syntax, morphisms between theories, flexible notions of theory equivalence, and the functorial view of semantics, all help to overcome philosophical and practical obstacles to formalization in science and suggest ways to create new capabilities for scientists. Finally, I will briefly describe ongoing efforts to realize these ideas as software for scientific modeling. Throughout, I take the perspective that philosophy of science should not be merely descriptive of current or past scientific practice, but has an important prescriptive role to play in shaping scientific methodology in the long term.
Mike Shulman (Dec 05 2023 at 06:50):Nice! Nobody asked me for an abstract yet, so I haven't written one.
Mike Shulman (Dec 05 2023 at 06:50):I wonder whether any of the talks are going to answer "no" to the question in the title of the conference...
Evan Patterson (Dec 05 2023 at 06:51):Haha, that would be rather bold!
Evan Washington (Dec 05 2023 at 18:53):Evan Patterson said:
I'm going to talk about how work on theories and models in philosophy of science influenced my thinking about scientific modeling and, conversely, how I think ideas from category theory and categorical logic could be relevant to debates in that field.
Here's my abstract:
Beginning with the logical positivists, the philosophical project to make sense of scientific theories and models using mathematical logic is now about a hundred years old. Although the project has had notable successes in "rationally reconstructing" various theories and models, the use of formal logic by working scientists remains extremely limited today. This state of affairs seems to be due to the impracticality of formalizing typical science in standard logic and to the lack of obvious benefit that would ensue to scientists by doing so. In this talk, I will argue that there is a significant opportunity to encourage greater use of formal logic in science by adopting modern techniques from categorical logic, the approach to logic based on category theory. I will explain how specific features of categorical logic, such as the ability to assemble "domain-specific" logics, the algebraization of syntax, morphisms between theories, flexible notions of theory equivalence, and the functorial view of semantics, all help to overcome philosophical and practical obstacles to formalization in science and suggest ways to create new capabilities for scientists. Finally, I will briefly describe ongoing efforts to realize these ideas as software for scientific modeling. Throughout, I take the perspective that philosophy of science should not be merely descriptive of current or past scientific practice, but has an important prescriptive role to play in shaping scientific methodology in the long term.
This is really interesting! Would love to chat more about this some time, very much related to some issues I've spent some time thinking thinking about
Evan Patterson (Dec 05 2023 at 21:30):Definitely! In fact, you're at UC Berkeley, right? You should come visit and give a talk here at Topos. I'll follow up with you separately about that so as not to make too much noise in this thread.
David Michael Roberts (Dec 06 2023 at 05:44):I hope the videos are put on YouTube, like the Grothendieck conference that was held at Chapman.
John Baez (Dec 06 2023 at 11:49):I may have had to pressure the folks at Chapman a bit to record videos and put them online for the Grothendieck conference. So, I hope someone speaking at " Is Philosophy Useful for Science, and/or Vice Versa?" asks them to put videos online.
John Baez (Dec 06 2023 at 11:49):Not everyone automatically records conference talks. So if anyone is ever giving a talk, it's always useful to suggest doing it!
But since this is Mike Shulman's thread I'll suggest that he do it. :upside_down:
Mike Shulman (Dec 06 2023 at 17:38):Thanks for the suggestion! I'll bring it up.
Mike Shulman (Dec 07 2023 at 18:43):I'm told that the talks will be recorded and posted with the speakers' permission.
Mike Shulman (Feb 05 2024 at 22:35):I've posted the slides from my talk here. The conference was very thought-provoking!
David Michael Roberts (Feb 06 2024 at 00:51):Very nice, @Mike Shulman ! Looking forward to your comments in the talk recording and any resulting discussion.
Mike Shulman (Apr 24 2024 at 16:54):For a little under a year, I've been working on a prototype of a new proof assistant that will hopefully implement Higher Observational Type Theory. I recently made the repository public, so you can check it out at https://github.com/mikeshulman/narya. So far, it implements an internal parametricity theory that's intended to serve as a non-univalent substrate for defining HOTT later (hopefully not too much later!), but it can also be used directly right now for several versions of parametricity.
There aren't a lot of ergonomic features (e.g. no unification, implicit arguments, or interactivity), and it's technically inconsistent (e.g. type-in-type and no termination, positivity, or productivity checking) but it's fairly usable. The GitHub README describes the syntax and capabilities in a fair amount of detail, and last weekend I gave a talk at the "Running HoTT" conference sketching the normalization algorithm that it's based on.
David Corfield (Apr 25 2024 at 09:49):Interesting talk! Where you say on slide 38 that for every primitive type we need to stipulate identity types and reflexivity terms, what happens with a formation principle such as forming (higher) inductive types? Is there a way to give identity types and reflexivity terms here based on information of constructors?
Mike Shulman (Apr 25 2024 at 22:40):On slide 11 I said that what's actually implemented doesn't compute the identity types definitionally to something else, but rather says what kind of type they behave as, which is generally a type of the same class as the base type. In the case of an original inductive type, its identity type is an inductive family, indexed over two copies of the base inductive type, whose constructors are reflexivities of the constructors of the base type. So, for instance, is an indexed inductive family with constructors and .
Mike Shulman (Apr 25 2024 at 22:41):I haven't implemented higher inductive types yet, but I think they should behave similarly, except that the path-constructors of the base HIT also become point-constructors of its identity types. And then one needs to add fibrancy/transport, which I haven't quite worked out yet.