Category Theory
Zulip Server
Archive

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.

Stream: community: our work

Topic: Mike Shulman

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:

1. Finish The univalence principle with Benedikt Ahrens and Paige North, a much longer elaboration of A Higher Structure Identity Principle.

2. <redacted>

3. Revise and submit All (∞,1)-toposes have strict univalent universes for publication.

4. 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.

5. Expand my categorical logic notes into a textbook.

6. 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.

7. A couple of unfinished projects involving $\ast$-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:

5. 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.

1. Prepare a talk I'm giving next Wednesday at UNAM on "Double categories, multivariable mates, and Chu constructions".
2. <redacted>
3. Revise and submit "All (∞,1)-toposes have strict univalent universes" for publication.
4. 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.

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:

1. Give a talk today at the University of Wisconsin on "Avoiding large cardinals in category theory".
2. Prepare and give a talk next Wednesday at Harvard on "HOTT and the quest for extensionality".
3. Revise "Categories of Nets" for final LICS publication with John Baez, Fabrizio Genovese, and Jade Master.
4. Revise and submit other papers for publication

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 $\rm Set_*$ 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:

1. A pile of refereeing committments due this month and next.
2. Three papers that still need revising/(re)submitting -- I finally got the antithesis construction and symmetric-monoidal type theory papers revised, but it seems there's always more to do.
3. Come up with a title and abstract for a talk at a POMSIGMAA JMM special session. The session is called “Competing foundations for mathematics: how do we choose?”, and it looks like my role is the (homotopy) type theorist.
4. Writing my own proof assistant.
5. <still redacted>

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):

4. 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 associativity in 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:

1. Make it through our departmental hiring cycle.
2. <redacted>
3. Revise some papers.
4. Write my talk for the postponed now-virtual JMM session "Competing foundations for mathematics: how do we choose?" My talk is scheduled for April 6 and is contrarily titled "Complementary foundations for mathematics: when do we choose?" but that's about all I know about it so far.
5. Plan my 3 talks for the "HoTTEST Distinguished Lecture Series" on April 14, 21, and 28. For these I don't even have a title yet.

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 $\Omega$ 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 $C$ and a dual of $J$, and then the morphisms to be freely generated by those of $C$ 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, $\mathsf{Id}_{\mathbb{N}}$ is an indexed inductive family with constructors $\mathsf{refl}_0 : \mathsf{Id}_{\mathbb{N}}(0,0)$ and $\mathsf{refl}_{\mathsf{suc}} : (m\,n : \mathbb{N}) \to \mathsf{Id}_{\mathbb{N}}(m,n) \to \mathsf{Id}_{\mathbb{N}}(m+1,n+1)$.

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.

Mike Shulman (Sep 05 2024 at 00:36):

Today was the first day of class in the fall semester, which is the day every year when I'm reminded that I love teaching. The day before the first day of class, I'm always reluctant to get back in the classroom after summer break; but in the classroom on the first day I get re-energized by all the new faces ready to learn (and I haven't gotten beaten down by grading yet).

Mike Shulman (Sep 05 2024 at 01:09):

This semester I'm teaching a new class, a second semester of abstract algebra. Our first semester of abstract algebra introduces groups and rings, but I more or less get to invent this class. I'm planning to do some module theory with an eye towards homological algebra and applications to homology of cell complexes, and introduce some category theory along the way.

However, I don't intend it to be a category theory class as such, so I don't want to spend a long time getting comfortable with abstract categories with examples like posets, deloopings of groups, and so on. So I'm toying with the idea of not defining an abstract category at all, but instead giving a definition like this:

Definition: A concrete category consists of

1. A collection of objects, each of which is a set equipped with some extra structure (if we want to be extra-precise, we can say that each object is an ordered $n$-tuple for some $n\ge 1$ whose first component is a set). If $X$ is an object, we often write $X$ also for this set, called its "underlying" set.
2. For any two objects $X,Y$, a subset $\hom(X,Y) \subseteq Y^X$ of the set of functions from (the underlying set of) $X$ to (the underlying set of) $Y$, whose elements are called morphisms.
3. For each object $X$, the identity function on $X$ is a morphism from $X$ to itself.
4. For any two morphisms $f\in \hom(X,Y)$ and $g\in \hom(Y,Z)$, the composite $g\circ f$ lies in $\hom(X,Z)$.
5. "Amnesty" (optional): If $X_1$ and $X_2$ are two objects with the same underlying set $X$, and the identity function on $X$ lies in both $\hom(X_1,X_2)$ and $\hom(X_2,X_1)$, then $X_1=X_2$.

Of course, in some ways this is more complicated than the abstract definition of category (particularly if we include amnesty). But I'm thinking it might be easier to conceptualize as a direct abstraction of examples like groups, rings, vector spaces, and so on, by leaving out the extra hurdle of having to think of a "morphism" as an undefined abstract object rather than just as a "structure-preserving function", and getting properties like associativity for free from familiar composition of set-functions.

I don't think I've seen a direct definition of "concrete category" like this that doesn't go through the definition of an abstract category (except I have a vague memory of something like it somewhere in Bourbaki). Probably we all agree nowadays that in principle it's better to define abstract categories first and then concrete categories as abstract ones with a special kind of functor to Set, but I wonder whether anyone has considered the possible pedagogical value of starting with concrete ones only? Or can you think of reasons why it's a bad idea?

Kevin Carlson (Sep 05 2024 at 01:36):

I think this is a good idea. I haven't done this but I've taught group theory to high schoolers in an analogous way, starting with groups of symmetries of a fixed set, i.e. a group is a subset of the set of functions $X\to X$ for some set $X,$ containing the identity and closed under composition and inverses. It works great, and makes proving Cauchy's theorem later far more exciting.

Kevin Carlson (Sep 05 2024 at 01:38):

If you wanted to be really pre-modernist you could probably introduce the notion of universal property in terms of "$\mathrm{Hom}$" between two abelian groups/modules, and then perhaps notice that you can do that in terms of "$\mathrm{Fun}$" between two sets, and only then actually give the notion of concrete category.

Mike Shulman (Sep 05 2024 at 01:41):

You mean look at some examples of universal properties in particular categories before defining a concrete category?

Jorge Soto-Andrade (Sep 05 2024 at 02:15):

Mike shulman: I have done more or less this, a number of times myself, it
seems indeed to be a natural first step. We have even written some papers
in systemic biology which deal just with concrete categories...
A couple of caveats though:

• I usually quickly go into concrete path categories, which are very
  intuitive and sort of "the other side of the coin" at a basic level, in my
  view. You can work first with paths in graphs, to avoid getting bogged
  down in homotopy issues, like "thin homotopy" (this can afford a motivation
  for homotopy, though)

• universal properties first, is also a good idea, I find. I recall also
  that Bourbaki's viewpoint was to say what "functorial" is, without
  explicitly defining categories. Like the physicists who work with
  differentiable or analytic mappings without minding source and target too
  much.
  So a variant of your approach would be to give or to have the students
  work first with concrete examples of functors. This is also quite
  intuitive: you do not just transform the objects but also the structure
  preserving mappings between them.
  Good luck!

Chris Grossack (they/them) (Sep 05 2024 at 02:19):

I'll give a dissenting opinion, and say that I kind of don't see the point of this. Like, what does this buy you that you couldn't get by giving the usual definition of a category, only giving concrete algebraic examples, and making a passing remark that "not every category looks like this, but we won't encounter other kinds of category in this class"? You could say that "categories in which every object has an underlying set are called 'concrete', and in this class we'll only talk about concrete categories". Then students know there's a broader world, see the usual definition, and still don't have to grapple with categories as combinatorial/geometric/etc. objects

Chris Grossack (they/them) (Sep 05 2024 at 02:21):

I don't think the usual definition, followed by examples like the categories of groups, rings, vector spaces, and sets, is any more complicated at all than the pre-concretified definition. But maybe there's some other benefit you want to get by using this approach?

Mike Shulman (Sep 05 2024 at 02:26):

Kevin Carlson said:

I've taught group theory to high schoolers in an analogous way, starting with groups of symmetries of a fixed set, i.e. a group is a subset of the set of functions $X\to X$ for some set $X,$ containing the identity and closed under composition and inverses.

I have a vague memory of looking at a textbook that does this too, but I can't remember right now which it was.

Mike Shulman (Sep 05 2024 at 02:30):

Jorge Soto-Andrade said:

• I usually quickly go into concrete path categories, which are very
  intuitive and sort of "the other side of the coin" at a basic level, in my
  view.

What is a "concrete path category"? There doesn't seem to be a natural way to make a path category "concrete" in the usual sense. Do you mean defining path categories as special objects in their own right, alongside but not an example of "concrete categories"? That makes sense in a class that's intended as a category theory class, but I don't think I would want to digress in that direction in this class.

So a variant of your approach would be to give or to have the students
work first with concrete examples of functors.

Yes, that's a good idea too. I'm not sure whether I'd want to do that before defining concrete categories, but it does make sense as a way to lead into general functors.

Jorge Soto-Andrade (Sep 05 2024 at 02:34):

The Soviet encyclopedia of math (edited by Shafarevitch, Kostrikin,
Kirillov and the like) begins group theory with transformation groups...)
available at annas-archive ...

Jorge Soto-Andrade (Sep 05 2024 at 02:55):

MS: I said "concrete" path categories in the sense that paths in a graph
or in a topological space are quite concrete. I should have written
"concrete" with quotations mark, sorry. The point is exactly that
categories of paths do not look like concrete categories of structured
sets. I mean that you look at all paths in (directed) graph, say
(sequences of connected nodes) and realize that they compose in a natural
associative way and that you also have paths which never took off. Some
paths are invertible, all of them in non directed graph. To check that
the reverse path is the inverse you need some innocent homotopy (a "thin"
one, in fact)". In my view the students' categorical understanding would
remain a bit biased if they just played around with concrete (structured
set). categories. I am also fond of categories of diagrams like braids,
which are ultra "concrete". You can concretize them with geoboard and
colored woolen threads. E.g. you connect 3 pins with 3 pins (call them a,
b, c and a', b', c' ) with woollen threads. This is subtler than set
mappings, because when you physically connect a to b' , b to a' and c to
c', you have to *make up your mind: *how do you cross the threads, the
second over the first or the second below the first? This is an example
of inclusive materialism: how material objects shape your "abstract"
cognition... :blush:

Madeleine Birchfield (Sep 05 2024 at 03:22):

Mike Shulman said:

Definition: A concrete category consists of

1. A collection of objects, each of which is a set equipped with some extra structure (if we want to be extra-precise, we can say that each object is an ordered $n$-tuple for some $n\ge 1$ whose first component is a set). If $X$ is an object, we often write $X$ also for this set, called its "underlying" set.
2. For any two objects $X,Y$, a subset $\hom(X,Y) \subseteq Y^X$ of the set of functions from (the underlying set of) $X$ to (the underlying set of) $Y$, whose elements are called morphisms.
3. For each object $X$, the identity function on $X$ is a morphism from $X$ to itself.
4. For any two morphisms $f\in \hom(X,Y)$ and $g\in \hom(Y,Z)$, the composite $g\circ f$ lies in $\hom(X,Z)$.

Mike Shulman said:

Probably we all agree nowadays that in principle it's better to define abstract categories first and then concrete categories as abstract ones with a special kind of functor to Set, but I wonder whether anyone has considered the possible pedagogical value of starting with concrete ones only?

The component-wise definition of a concrete category can be directly defined after defining an abstract category, as an abstract category with additional structure, while the other definition of a concrete category first requires defining functors and $\mathrm{Set}$.

I personally don't have an opinion about defining concrete or abstract categories first, but unless functors are going to be used in this algebra class, I would rather not define functors at all (for a similar reason for your not wanting to define abstract categories) and simply define concrete categories component-wise.

Mike Shulman (Sep 05 2024 at 03:30):

Chris, thanks for the dissent! I tried to explain the benefit I was hoping for when I said:

leaving out the extra hurdle of having to think of a "morphism" as an undefined abstract object rather than just as a "structure-preserving function", and getting properties like associativity for free from familiar composition of set-functions.

But maybe it will help if I try to explain more about where I'm coming from. One of the things I've only gradually come to appreciate in my years of teaching is that I'm atypical, at least compared to my students, in terms of what's intuitive to me and how I like to think about things. I am reminded of John Baez's quip that category theorists dual to ordinary people, getting more confused when you surround an abstract concept with lots of distracting specifics. The flip side of that is that we category theorists can recognize that many ordinary people are dual to us, getting more confused the more abstract a definition is.

Last summer I had some undergraduate research students who started out by learning some category theory, and I found one of the hurdles for them to get over was the idea that a "morphism" can be anything at all. Of course this is an important hurdle to get over eventually, but I would rather not spend the time getting over it in this class if I don't have to, and all the categories I plan to use in this class are concrete.

Does that help explain the benefit I hope to get?

Mike Shulman (Sep 05 2024 at 03:32):

Madeleine Birchfield said:

unless functors are going to be used in this algebra class, I would rather not define functors at all

Functors are definitely going to appear in this class, like homology.

John Baez (Sep 05 2024 at 03:37):

Will you explicitly discuss any natural transformations? (I'm thinking of Mac Lane's story.)

David Egolf (Sep 05 2024 at 03:47):

I really enjoyed the "aha!" moment that came with realizing how we can view a group (such as the integers with addition) as a one object category. For that reason, when I try to explain what a category is to an interested friend, this is one of the first examples I give.

That being said, I do remember the process of reaching that "aha!" moment as being somewhat brain-bending. I suspect that if I were taking this class a few years ago, I would have found your proposed approach (via the definition of "concrete category") easier to understand, but also less exciting than working with the abstract definition of category.

Mike Shulman (Sep 05 2024 at 04:05):

John Baez said:

Will you explicitly discuss any natural transformations? (I'm thinking of Mac Lane's story.)

Perhaps the connecting morphism in the homology long exact sequence, or induced maps between homology with different coefficients.

Madeleine Birchfield (Sep 05 2024 at 04:26):

I suppose I took an odd route to category theory, compared to everybody else, and thus didn't have the brain-bending experiences that everybody else seemed to have.

For me, category theory began as a way to define set theory in the foundations of mathematics - the objects were sets, and the morphisms were functions, and different categories corresponded to weaker or stronger foundational set theories. These were abstract categories because there was no pre-existing notion of set to define concrete categories; I only had a sorted first-order logic with equality where one sort is for the objects/sets and the others are for the morphisms/functions.

Later I found out that there were also categories of other mathematical structures like the category of commutative rings and ring homomorphisms, with similar limits and colimits as the various foundational categories of sets I had been studying.

David Michael Roberts (Sep 05 2024 at 04:27):

Your point 1 feels like the Bourbaki notion of 'species of structure' - I guess this is made more complete by knowing that the projection map onto the set that's the first item in the list is the underlying set functor, and if you use this approach, that would be a good first functor to introduce I think.

David Michael Roberts (Sep 05 2024 at 04:29):

I think Bourbaki originally could most easily talk about groupoids of structured sets, but talking about general structure-preserving morphisms was, I think, not so easy.

Madeleine Birchfield (Sep 05 2024 at 04:29):

David Michael Roberts said:

Your point 1 feels like the Bourbaki notion of 'species of structure' - I guess this is made more complete by knowing that the projection map onto the set that's the first item in the list is the underlying set functor, and if you use this approach, that would be a good first functor to introduce I think.

The underlying set functor would also take morphisms to functions and so would also include parts of point 2.

David Michael Roberts (Sep 05 2024 at 04:33):

You have clunky statements in Bourbaki's set theory book about proving the theorem that a relation. i.e. a proposition on $X\times Y$, is a function from $X$ to $Y$ in the given theory for a given species of structure.

Mike Shulman (Sep 05 2024 at 05:23):

David Michael Roberts said:

I guess this is made more complete by knowing that the projection map onto the set that's the first item in the list is the underlying set functor, and if you use this approach, that would be a good first functor to introduce I think.

Yes, that's an important functor. I'm also planning to talk about free objects and their universal property relative to this functor, and then the free functor is natural to mention as well. And I might as well then give the definition of adjunctions in terms of universal arrows, though I don't expect I'll want to mention the homset-bijection or triangle-identity versions.

Mike Shulman (Sep 05 2024 at 05:26):

Another attraction of working with concrete categories is that certain other notions can be defined more simply by concretizing them. For example, say a pointed concrete category (or "concretely pointed category"?) is a concrete category such that all underlying sets are pointed, all morphisms are pointed functions, and the constant function at the basepoint is always a morphism. This feels like a natural definition looking at examples like groups, module, pointed sets, and nonunital rings, and I think it'd be easier for students to work with than the abstract definition saying that each homset has a "zero morphism".

Morgan Rogers (he/him) (Sep 05 2024 at 08:39):

Chris Grossack (they/them) said:

I'll give a dissenting opinion, and say that I kind of don't see the point of this. Like, what does this buy you that you couldn't get by giving the usual definition of a category, only giving concrete algebraic examples, and making a passing remark that "not every category looks like this, but we won't encounter other kinds of category in this class"? You could say that "categories in which every object has an underlying set are called 'concrete', and in this class we'll only talk about concrete categories". Then students know there's a broader world, see the usual definition, and still don't have to grapple with categories as combinatorial/geometric/etc. objects

I would like to second this; for the few that encounter categories later on, having to unlearn this specific understanding of what a category is will be much simpler if they know in advance that there is more to the story.
More importantly, a majority of students will look up some of the stuff you teach them at some point, and not knowing that there is a bigger story (or at least that the way you are presenting things is atypical) will make the way things are presented on the nLab or Wikipedia much more confusing.

Mike Shulman (Sep 05 2024 at 08:41):

Well, I would of course tell them that there is a bigger story.

Mike Shulman (Sep 05 2024 at 08:41):

But thanks for the negative feedback; I will think carefully about it.

Mike Shulman (Sep 05 2024 at 08:51):

Perhaps I misunderstood Chris's point? I took it as a criticism of the whole approach, but are you suggesting only that instead of starting with my direct definition of "concrete category" I start instead with

Definition: A category is (the usual thing).

Definition: A category is concrete if

1. Every object is a set together with some additional structure.
2. Each hom-set $\hom(X,Y)$ is a subset of $Y^X$.
3. Each identity morphism is the identity function.
4. Composition of morphisms is composition of functions.

and then proceed exactly as I was going to, discussing only concrete categories but having written down the general definition?

Josselin Poiret (Sep 05 2024 at 09:10):

Mike Shulman said:

I'm planning to do some module theory with an eye towards homological algebra and applications to homology of cell complexes

Hi Mike, tangentially to the discussion about concrete categories, I'm very interested in how you would motivate homological algebra from first principles: I remember that I ended up studying it because it seemed like an interesting topic (I knew it was a basic tool of the trade in algebraic geometry), but that's about it. The only free-standing narrative I could think of nowadays is as an abelian version of homotopy, however I'm still struggling to get that off the ground and be a useful way to think about most constructions and theorems. The Dold-Kan correspondance being quite involved doesn't help to go back and forth freely imo.

Do you have any insights?

David Michael Roberts (Sep 05 2024 at 11:20):

Personally, I think Mike's proposed definition, slightly baroque though it may seem to us, familiar with the normal definition of categories, would be a guard against the kind of conceptual confusion students get when they grapple with trying to forget that not all categories are concrete.

Mike's students, I assume, can appreciate the difference between abstract groups and concrete groups, and the passage from the above definition to the normal one seems like it would be eased by reference to the group case.

John Baez (Sep 05 2024 at 13:03):

Josselin Poiret said:

Hi Mike, tangentially to the discussion about concrete categories, I'm very interested in how you would motivate homological algebra from first principles: I remember that I ended up studying it because it seemed like an interesting topic (I knew it was a basic tool of the trade in algebraic geometry), but that's about it. The only free-standing narrative I could think of nowadays is as an abelian version of homotopy, however I'm still struggling to get that off the ground and be a useful way to think about most constructions and theorems.

This is an interesting question to me because I learned homology, cohomology and homological algebra as extremely practical but slightly mysterious tools before meeting deeper explanations along the lines of "chain complexes are secretly just simplicial abelian groups, which are especially nice Kan complexes", "Kan complexes are secretly just $\infty$-groupoids" and most especially "$\infty$-categories rule the world". In retrospect I think this was a fun way to learn things: it was like getting to know a house fairly well and then discovering it had a secret door leading to a much larger set of rooms, which explained the peculiar architecture of the part I'd seen.

In the first phase, I enjoyed how concepts from homology and cohomology are extremely visual when you're working with a chain complex coming from a topological space - you can see that a cycle is not a boundary if it encloses a hole in your space, etc., you can see why $H^1(\mathbb{RP^3}) \cong \mathbb{Z}/2$, etc., and you can use your visual reasoning to guess what to compute. I also enjoyed how people use homology and cohomology to crack lots of otherwise elusive problems like the Brouwer fixpoint theorem or the hairy ball theorem.

Since I'm a mathematical physicist, all this stuff seemed more than merely fun - it was downright practical! De Rham cohomology underlies electromagnetism in a wonderful way. Nonabelian gauge fields use even more algebraic topology. All the visual reasoning about topological spaces gets blended with physical reasoning about fields that live on these spaces. There are some very nice books explaining all this.

But many things remained rather unintuitive and mysterious, like resolutions, derived functors, etc. - I saw how they worked and what they did, but I didn't know what they meant. Some of this was just laziness on my part, since some of these things do have visual interpretations. But the $\infty$-categorical viewpoint was like a key to a secret door leading to deeper understanding.

Josselin Poiret (Sep 05 2024 at 13:16):

John Baez said:

This is an interesting question to me because I learned homology, cohomology and homological algebra as extremely practical but slightly mysterious tools before meeting deeper explanations along the lines of "chain complexes are secretly just simplicial abelian groups, which are especially nice Kan complexes", "Kan complexes are secretly just ∞-groupoids" and most especially "∞-categories rule the world". In retrospect I think this was a fun way to learn things: it was like getting to know a house fairly well and then discovering it had a secret door leading to a much larger set of rooms, which explained the peculiar architecture of the part I'd seen.
[...]
But many things remained rather unintuitive and mysterious, like resolutions, derived functors, etc. - I saw how they worked and what they did, but I didn't know what they meant. Some of this was just laziness on my part, since some of these things do have visual interpretations. But the ∞-categorical viewpoint was like a key to a secret door leading to deeper understanding.

I've gone through all of the above as well, although you're describing this better than I had! To keep up with the metaphor, I'm interested in 1) how to introduce the first house as something that is not just a tool but has an intrinsic, self-standing meaning and interest, 2) how to frame that first house as not just connected to a second similar but bigger house via some backdoor, but rather as an integral part of the second!

Maybe someone has a reference to a formal, systematic study of how all those homological tools translate under that correspondance, or something similar?

John Baez (Sep 05 2024 at 13:25):

I would love for there to exist a book on "homological algebra from an $\infty$-categorical point of view", but I haven't seen one, so I've been going here and there trying to learn what would be in that book. I have at times wanted to write a book on higher categories - but when I think about it, it grows too big in my mind and I realize writing it would stop me from thinking about new things.

Mike Shulman (Sep 05 2024 at 14:58):

I have no intention of trying to motivate homological algebra from what I would call "first principles". Instead I'm planning to motivate it with cellular homology, not in full topological generality (since topology is not a prerequisite) but using simple cut-and-paste diagrams for 2D surfaces and things like $H_1$ of the torus, Klein bottle, and projective plane. If enough of the students remember enough multivariable calculus, I might also try to bring in some baby De Rham cohomology, to make the point that there's more than one application.

Mike Shulman (Sep 05 2024 at 14:59):

In other words, get them started on the path John described traveling.

Madeleine Birchfield (Sep 05 2024 at 15:07):

Mike Shulman said:

Definition: A category is concrete if

1. Every object is a set together with some additional structure.

Is the additional structure necessary in this definition? The category of sets is concrete and more generally the category of $\kappa$-small sets for some cardinal $\kappa$ is concrete, but the sets do not come with any additional structure.

John Baez (Sep 05 2024 at 15:19):

Knowing Mike, he counts "no additional structure" as a degenerate example of "some additional structure".

Madeleine Birchfield (Sep 05 2024 at 15:25):

John Baez said:

Knowing Mike, he counts "no additional structure" as a degenerate example of "some additional structure".

In that case, "with some additional structure" is redundant in the definition, because every set comes with some additional structure.

John Baez (Sep 05 2024 at 15:27):

No, it's not redundant. "Set" means just "set". "Set with additional structure" means "object of a category equipped with a faithful functor to the category Set".

John Baez (Sep 05 2024 at 15:27):

The former is a special case of the latter.

John Baez (Sep 05 2024 at 15:29):

Of course Mike won't be in a position in his course to define "with additional structure" in the way I just did, when he's just introducing category theory. So the question is whether some intelligent student will ask exactly what that means (they should!) and what Mike will say then.

Madeleine Birchfield (Sep 05 2024 at 15:35):

John Baez said:

No, it's not redundant. "Set" means just "set". "Set with additional structure" means "object of a category equipped with a faithful functor to the category Set".

Then I take issue with the phrasing that "every object is a set" in the definition, since the objects are clearly not sets.

A concrete category $C$ should come with a collection $\mathrm{Ob}(C)$ whose elements are called "objects", and a family of sets $U(x)$ indexed by objects $x \in \mathrm{Ob}(C)$.

Kevin Carlson (Sep 05 2024 at 15:37):

Just reinforcing that in my experience there is indeed almost always a substantial mind-bending moment when students have to understand how exactly it can be that opposite categories, groups, etc can really be categories, to the point that I would avoid trying to teach the abstract definition to typical undergrads unless I was teaching a whole semester of category theory. By far the most common beginner question on category theory math stack exchange is something about “but how does a morphism in the opposite category act on elements of the domain?” Compared to that guaranteed struggle, I have trouble feeling very worried about Morgan’s concerns; students are unlikely to meet more category theory until graduate level courses, when we can assume they’re prepared to think hard, and at the undergrad level math Wikipedia and all the more so the nLab are very hard to use no matter what.

Madeleine Birchfield (Sep 05 2024 at 15:40):

Madeleine Birchfield said:

Then I take issue with the phrasing that "every object is a set" in the definition, since the objects are clearly not sets.

A concrete category $C$ should come with a collection $\mathrm{Ob}(C)$ whose elements are called "objects", and a family of sets $U(x)$ indexed by objects $x \in \mathrm{Ob}(C)$.

On second thought, this is just the Russell vs Tarski universe debate from type theory all over again, only in the context of concrete categories. Are the objects in concrete categories literal sets, or are they codes for sets? The functor definition of a concrete category implies that objects of concrete categories are codes for sets, a la Tarski, while Mike Shulman's definition of a concrete category says that the objects are sets, a la Russell.

John Baez (Sep 05 2024 at 16:05):

Madeleine Birchfield said:

John Baez said:

No, it's not redundant. "Set" means just "set". "Set with additional structure" means "object of a category equipped with a faithful functor to the category Set".

Then I take issue with the phrasing that "every object is a set" in the definition, since the objects are clearly not sets.

Let's just hope you don't take Mike's course. Given our faithful functor $F: \mathsf{C} \to \mathsf{Set}$, a 'set with extra structure' is a set $S$ together with an object $C \in \mathsf{C}$ with $F(C) = S$. $S$ is the set and $C$ is the extra structure.

Mike Shulman (Sep 05 2024 at 16:17):

Madeleine Birchfield said:

Then I take issue with the phrasing that "every object is a set" in the definition, since the objects are clearly not sets.

I didn't say "every object is a set". I said "every object is a set with additional structure". Of course, that should be parsed as "every object is a (set with additional structure)". And in my first post I already gave what my answer would be to John's intelligent student:

if we want to be extra-precise, we can say that each object is an ordered $n$-tuple for some $n\ge 1$ whose first component is a set.

The case $n=1$ is the case of "no additional structure".

John Baez (Sep 05 2024 at 16:19):

If the student asks if the second component can be another set, then you're stuffed. (Pun based on British slang.)

Madeleine Birchfield (Sep 05 2024 at 16:25):

I would personally prefer this definition of a concrete category:

Definition: A category is concrete if

1. For every object $x$ there is a set $U(x)$
2. There is an injection $i_{X, Y}$ from the hom-set $\hom(X,Y)$ to the function set $Y^X$.
3. The injection takes the identity morphism on an object $x$ to the identity function on its corresponding set $U(x)$: $i_{X, X}(1_X) = \mathrm{id}_{U(x)}$.
4. The injection preserves composition: given objects $X$, $Y$, and $X$, two morphisms $f:\hom(x, y)$ and $g:\hom(x, y)$, $i_{X, Z}(g \circ f) = i_{Y, Z}(g) \circ i_{X, Y}(f)$

since this is just a direct translation of the definition of a faithful functor, and sidesteps entirely the question of what a "set with additional structure" is. Then a set with additional structure is simply defined to be an object of the category as John Baez said.

Mike Shulman (Sep 05 2024 at 16:27):

From my perspective, that definition basically defeats the point, namely that by working only with concrete categories we can assume that the morphisms are certain functions -- as is always the case in naturally-arising concrete categories -- rather than merely being associated to some function.

Mike Shulman (Sep 05 2024 at 16:28):

If it makes you happier, you can think that what I'm really defining is a certain kind of [[displayed category]] over Set.

Madeleine Birchfield (Sep 05 2024 at 16:29):

Mike Shulman said:

From my perspective, that definition basically defeats the point, namely that by working only with concrete categories we can assume that the morphisms are certain functions -- as is always the case in naturally-arising concrete categories -- rather than merely being associated to some function.

Then my point I was making to John Baez is that your definition of a "set with additional structure" is different from John Baez's definition of a "set with additional structure" as "object of a category equipped with a faithful functor to the category Set":

John Baez said:

No, it's not redundant. "Set" means just "set". "Set with additional structure" means "object of a category equipped with a faithful functor to the category Set".

Mike Shulman (Sep 05 2024 at 16:30):

Yes, I agree, it is different.

Simon Burton (Sep 05 2024 at 17:14):

Mike, would you also describe concrete groups and/or concrete posets? seems like that could be fruitful.. and also might pave the way to understand the concrete/abstract divide later on...

Mike Shulman (Sep 05 2024 at 17:37):

No, because this isn't a category theory class. It's a second-semester abstract algebra class. The students are already familiar with abstract groups, including concrete groups (permutation groups), and I don't anticipate having any need to discuss posets.

Exequiel Rivas (Sep 06 2024 at 22:07):

There is a book by Adámek titled "Theory of Mathematical Structures", where Part I covers 'constructs' first, which I think are similar to the idea being discussed. Categories are introduced later in Part II of the book. I'm not certain if links to Google Books work across different regions, but here is a link to the page defining constructs.

Mike Shulman (Sep 07 2024 at 06:14):

Ah, nice, thanks!

David Michael Roberts (Sep 07 2024 at 10:32):

Screenshot_20240907_200104_Firefox.jpg

Fwiw here is a screenshot of the definition from a different instance of Google books to the link

Jorge Soto-Andrade (Sep 07 2024 at 14:42):

Obrigado! you can easily find Jiri Adámek books in annas-archive.org, btw.