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: theory: category theory

Topic: doctrines


view this post on Zulip Morgan Rogers (he/him) (Apr 28 2021 at 16:49):

At present I'm thinking about categories with pullbacks, and pullback-preserving functors between these. I want to construct pushouts of these things. However I realised today that I don't want to be working with 1-pushouts: I want pseudo-pushouts. That is, the universal completion of a span of such categories to a square commuting up to specified natural isomorphism.

Mildly inconveniently, I want this to be the pseudo-pushout in the (2-/bi-)category I get by including all natural transformations between these functors as 2-morphisms, not just cartesian ones; the latter are in some ways more natural, but that is up for discussion.

When I was (mistakenly) trying to use 1-pushouts, I was able to prove that they exist abstractly using some classical 1-categorical results about categories of algebras, thanks to Paré's result that one can construct free pullback-completions of categories, so that the underlying 1-category is monadic over the 1-category of categories.

It seems to me that I want to instead consider the "doctrine of pullbacks" (or indeed, of connected simply connected limits) and its associated 2-monad on the category of categories. Since the liftings of 1-categorical results in this context are sparsely reported, please can someone advise me on:

  1. whether I should be looking at a strict 2-monad or a weaker version, and similarly whether I should be looking at strict or pseudo algebras for this; I expect that whatever the right choice is, it will give me all natural transformations out at the end, but if this is not so or determined by these choices, I would like to understand how;
  2. any references containing useful abstract results about 2-monads generally, especially as regards to properties of the relevant categories of algebras.

view this post on Zulip Morgan Rogers (he/him) (Apr 28 2021 at 16:51):

Alternatively, anything about the equivalent situation for categories with finite limits might help, since that's like to be a more well-document case.

view this post on Zulip Nathanael Arkor (Apr 28 2021 at 16:53):

There is a strict 2-monad on Cat whose algebras and pseudomorphisms are pullback-complete categories and pullback-preserving functors (in the usual sense), which I imagine is what you're after. See Kelly–Lack's paper On the monadicity of categories with chosen colimits, for instance.

view this post on Zulip Morgan Rogers (he/him) (Apr 28 2021 at 16:54):

Will check that out and report back, thanks!

view this post on Zulip Nathanael Arkor (Apr 28 2021 at 16:55):

I don't think they discuss limits/colimits in the categories of algebras here, but this can be deduced from the fact the 2-monad is finitary, Cat is LFP, and so the 2-category of algebras will be too.

view this post on Zulip Mike Shulman (Apr 28 2021 at 19:25):

But if you want (bi)colimits in the 2-category of algebras and pseudo morphisms, you need to do some more work, such as in Blackwell-Kelly-Power "Two-dimensional monad theory".

view this post on Zulip Morgan Rogers (he/him) (Apr 28 2021 at 19:28):

Since I don't know in advance which one I want, I'll need to check both :wink:

view this post on Zulip Morgan Rogers (he/him) (Apr 29 2021 at 10:15):

Mike Shulman said:

But if you want (bi)colimits in the 2-category of algebras and pseudo morphisms, you need to do some more work, such as in Blackwell-Kelly-Power "Two-dimensional monad theory".

This looks like exactly what I needed, thanks! One of their main examples is the 2-category of lex categories with all natural transformations, and they at least cover pseudo-limits; there should be enough detail in there for me to work out how results about pseudo-colimits can be reconstructed :tada:

view this post on Zulip Mike Shulman (Apr 29 2021 at 13:38):

You're welcome. They do also construct bicolimits (not pseudo-colimits), I think it's via a biadjoint lifting.

view this post on Zulip Morgan Rogers (he/him) (Apr 29 2021 at 13:46):

Having read this and three related papers today, I'm seeing that bicolimits are what I wanted all along (and become a lot more comfortable with the meanings of bi-, pseudo-, ... in various contexts!)
The good news is that, as you've said, this paper demonstrates that they exist in the context I care about :tada:

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 09:17):

While the above has addressed my own query, by supplementing it with Paré's paper on simply connected limits, there is an abstract step which I haven't been able to find in digging through this material so far. In Kelly and Lack's On Property-Like Structures it is claimed that 'The prime examples of structures given by lax-idempotent 2-monads are categories with colimits of some class'; while it's clear that everything they say is true as soon as we can identify the category of categories with colimits in a class C as algebras for some 2-monad, how do we know that we can construct a free category with colimits in C?
Referring to On the monadicity of categories with chosen colimits, the general construction of these (when the category is small, at least) is to close the category of representable presheaves under the desired colimits in the category of presheaves. This sounds neat, but... how does one do it? We need a choice of colimit for each diagram indexed by a category in C, and closing once doesn't seem like it will do the trick, unless we first extend C to its saturation (in the sense of a maximal class of colimits admitted by any category with colimits in C); indeed, as soon as we have to do this in more than one step, the existence of a choice for the colimits is no longer evident.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 09:22):

So the proof of the existence of the adjoint becomes a matter of finding the saturation of a given class of colimits. I could convince myself that this always exists, but there's bound to be some size restrictions on the classes C. Kelly and Lack's claim that the free cocompletion of a small category under a small class of colimits seems credible, but again is far from obvious. Am I missing something, or is their argument simply non-constructive in nature?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 10:36):

Morgan Rogers (he/him) said:

Kelly and Lack's claim that the free cocompletion of a small category under a small class of colimits seems credible

I take this back; Paré's construction of the free pullback-completion of a category involves dualizing and constructing the colimits via presheaves in a similar way (after having identified the saturation of the class of pullbacks), and it's pretty clear that the result is only essentially small, contrary to what Kelly and Lack are claiming, just by virtue of not having a categorical way to distinguish isomorphic objects in the presheaf topos.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 10:39):

On the other hand, the pointwise nature of pullbacks in the presheaf topos means that there is a canonical choice of pullbacks in the resulting essentially small category, so is this the genuine free pullback-completion? Or is it only the right thing up to equivalence?

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 10:41):

Or is it only the right thing up to equivalence?

This doesn't sound like a very categorical question :sweat_smile:

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 10:48):

Kelly and Lack's claim that the free cocompletion of a small category under a small class of colimits seems credible

Is the statement you're taking objection to Theorem 2.3 of Kelly–Lack's paper?

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 10:49):

If Φ\Phi is a small class of weights, then ΦC\Phi C is small if CC is so.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 10:49):

It's what happens when you try to work in a 2-category of categories... :rolling_on_the_floor_laughing:

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 10:50):

If Φ\Phi is a small class of weights, then ΦC\Phi C is small if CC is so.

That's the one, indeed

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 10:54):

Did you take a look at Section 5.7 of Basic Concepts of Enriched Category Theory? It goes into some detail about size issues.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:22):

Where? All I can see is the same claim that the result is small without justification :speechless:

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:26):

For example, they say in the very next section that the idempotent completion of a category CC consists of all retract of representables in PSh(C)\mathrm{PSh}(C) and that this is "clearly small if CC is", but again the axiom of replacement makes that false. Is it just that Kelly has a very loose meaning of "small"?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:29):

In section 3.5 he even takes the closure of a full subcategory under colimits to be replete, so it seems like there must be some other subtlety I'm missing

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 11:38):

Morgan Rogers (he/him) said:

Where? All I can see is the same claim that the result is small without justification :speechless:

Oh, actually 3.5 is where he talks about it in more detail, but I didn't look too closely at it. I agree it doesn't address your concern…

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 11:41):

image.png

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:49):

Thanks for finding the relevant passage!!

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 11:50):

I shall eagerly await your upcoming paper, Constructive colimit completions.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:52):

So I just need to work in essentially small categories and try not to worry about their extent... It's an emotional blow, but I'll survive

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 11:58):

I'll bet this breaks all of the results about existence of pseudo-limits and bicolimits in this category too :face_palm:

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 11:58):

Are you working internally? Is that why you're more careful about these concerns?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 12:03):

No, it's not of critical importance, I just didn't expect to have to go beyond the 2-category of small categories with pullbacks in order to construct these colimits. I basically wanted to examine (the dual of) Beck-Chevalley conditions, and so needed some pushout squares to hand.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 12:06):

If you're happy to use AC, can't you take the essentially small category exhibiting the completion, and then take a small category to which it's equivalent? Then you can continue to work in that 2-category.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 12:09):

I may be mixing up dimensions here, but I think that still reduces the 2-adjunction to merely being a biadjunction.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 12:10):

And if so it seems likely I will need different references in order to deduce the (co)completeness properties...

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 12:11):

Morgan Rogers (he/him) said:

I may be mixing up dimensions here, but I think that still reduces the 2-adjunction to merely being a biadjunction.

Oh, that's probably right…

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 12:13):

I expect the results I need will still hold, it's just a non-trivial amount of work to dig them up. I prefer to accept essential smallness and then sweep the size issues under the rug once I've justified the results I need.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 12:14):

I expect the results I need will still hold, it's just a non-trivial amount of work to dig them up.

Considering this is supposed to be the main result of Kelly–Lack, I imagine there is a resolution; maybe it'd be worth asking Steve Lack directly.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 12:19):

Will do; I'll report back later.

view this post on Zulip Mike Shulman (Apr 30 2021 at 13:20):

Constructing a free cocompletion as a closure in the presheaf category will generally only give you a pseudomonad rather than a 2-monad; this isn't really related to the fact that you have to construct the closure carefully to get a small category rather than an essentially small one. The way to get a 2-monad is to consider colimits as an algebraic structure, such as in 5.6 of Lack's A 2-categories companion.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 13:31):

Once again, that seems to be what I was looking for, at least in the form of an example. Do you know of a more systematic treatment, @Mike Shulman?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 13:32):

(I'll scan through the 2-categories companion in case it's actually in there already)

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 13:41):

The way to get a 2-monad is to consider colimits as an algebraic structure, such as in 5.6 of Lack's A 2-categories companion.

But this is exactly the motivation behind the Kelly–Lack paper, so the construction there ought to work.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 13:42):

They're not using closure of representables in their proofs, but they are citing Kelly for some standard results about cocompletions which do use closure of representables.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 13:43):

And the question is then whether this actually causes problems or not.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 13:59):

Morgan Rogers (he/him) said:

(I'll scan through the 2-categories companion in case it's actually in there already)

It's not, and at least one of the references to Kelly at the end of the section uses the same small = essentially small convention... Hmmm

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:19):

Nathanael Arkor said:

And the question is then whether this actually causes problems or not.

It's certainly causing me a headache. I guess I'm a 1-person after all and hadn't realised it...

view this post on Zulip Mike Shulman (Apr 30 2021 at 14:24):

Can you point exactly to where in Kelly-Lack you're worried about?

view this post on Zulip Mike Shulman (Apr 30 2021 at 14:26):

Note that in the introduction they mention that Kelly-Cruerer "On the monadicity over graphs of categories with limits" proves the case of ordinary (co)limits. I don't think I've read that paper, but you could have a look at it too.

view this post on Zulip Mike Shulman (Apr 30 2021 at 14:29):

In general, it looks like Kelly-Lack use the closure-of-representables definition, suitably modified to be small, to obtain a left biadjoint to some functor, and then operate on this further to produce a strict left 2-adjoint to the desired functor. So there shouldn't be any problem.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:35):

So, on the third page of the Kelly-Creurer paper, they observe that one can present the theory of limits in a class MM in terms of operations of arities up to M×3M \times \mathbf{3}, which they spell out, and then conclude the monadicity outright without mention of any specific result, although there are a bunch of references crammed into the preceding paragraph.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:48):

The main reference for monadicity there seems to be this Kelly & Power paper which again sneaks in the essential smallness, in Section 5!

view this post on Zulip Mike Shulman (Apr 30 2021 at 14:51):

What exactly are you worried about? Are you trying to avoid using the axiom of choice to replace an essentially small category by a small one?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:54):

I'm not worried, exactly, it just makes me uncomfortable that I should have to appeal to choice to verify monadicity of even finitary completions of small categories.

view this post on Zulip Mike Shulman (Apr 30 2021 at 14:55):

I'm pretty sure that Lack's construction doesn't depend on any of this, as it doesn't make any reference to the construction via closure.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:56):

That's what I think too! In the finitary case at the very least, this theory should be doable constructively. But there's no explicit version of this in the literature that doesn't go through Kelly at some point or other, is there?

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 14:59):

Ultimately it doesn't matter for my application, because I can just take the 2-category of essentially small categories with pullbacks, but I wish there was a neater account of all this that I could refer to.

view this post on Zulip Mike Shulman (Apr 30 2021 at 15:01):

You mean, you want someone to have written out explicitly a presentation of a monad for more general limits or colimits in the style of Lack 5.6?

view this post on Zulip Mike Shulman (Apr 30 2021 at 15:04):

There's a sketch of the construction for pullbacks in section 3 of Kelly-Dubuc A presentation of topoi as algebraic relative to categories or graphs.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 15:17):

Mike Shulman said:

I'm pretty sure that Lack's construction doesn't depend on any of this, as it doesn't make any reference to the construction via closure.

Doesn't it use the construction via closure (by reference to Kelly) to prove the existence of a left biadjoint, which is valid only because one can use choice to cut an essentially small category down to a small category?

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 15:17):

(I may very well be completely misinterpreting the proof!)

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 15:19):

Strictly speaking, shouldn't it follow that it is the 2-category of essentially small categories with Φ\Phi-colimits that is pseudomonadic over the 2-category of small categories?

view this post on Zulip Mike Shulman (Apr 30 2021 at 15:43):

I'm not talking about the Kelly-Lack paper. I'm talking about the explicit construction of a 2-monad whose algebras are categories with a chosen terminal object in section 5.6 of Lack's "2-categories companion". There is no reference to biadjoints or closures there.

view this post on Zulip Mike Shulman (Apr 30 2021 at 15:51):

However, in generality these results do depend on choice in a different way, namely in the existence of free monads and colimits of monads. In general, these facts require transfinite constructions, which -- again, in general -- depend on choice. Indeed, it's known (at least assuming the consistency of some large cardinal axioms) that there are infinitary algebraic theories that cannot be proven to have free algebras (and hence not monadic) in ZF. (This is in Blass's paper "Words, coequalizers, and free algebras".)

view this post on Zulip Mike Shulman (Apr 30 2021 at 15:52):

Problems like this don't come up for finitary theories, at least on Set, so I would expect that the cases of categories with finite limits or colimits can be constructed more explicitly without any choice. But I don't know if anyone has done it.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 15:53):

Mike Shulman said:

I'm not talking about the Kelly-Lack paper. I'm talking about the explicit construction of a 2-monad whose algebras are categories with a chosen terminal object in section 5.6 of Lack's "2-categories companion". There is no reference to biadjoints or closures there.

Oh, I see, yes.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 16:04):

Mike Shulman said:

There's a sketch of the construction for pullbacks in section 3 of Kelly-Dubuc A presentation of topoi as algebraic relative to categories or graphs.

Yet another helpful reference, I am very grateful. In the final section they point to paper of Kelly (which doesn't seem to exist?) for showing that an equational presentation of a class of categories is actually monadic; I suspect that Kelly would have resorted to the same appeal to closure in presheaves there.
But the equational presentation in Section 3 doesn't obviously rely on it, so as you say it should be provably monadic by more elementary means. This is like a 2-categorical lifting of sketches (the paper of Burroni that they reference even more so), which is pleasant.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 16:05):

I would have thought the approach by Lack would fit into the "Lawvere 2-theories" framework of Lack–Power. Unfortunately, there are only slides so far.

view this post on Zulip Joe Moeller (Apr 30 2021 at 16:11):

I haven't been following this discussion closely, but I was thinking about Lawvere 2-theories a while ago, and these are the two papers I have in my notes for it:

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 16:12):

I just came across this one too
http://www.tac.mta.ca/tac/volumes/6/n7/n7.pdf

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 16:14):

Enriched algebraic theories aren't sufficient, because you want to consider pseudomorphisms.

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 16:14):

If I remember correctly, Yanofsky only considers strict morphisms too?

view this post on Zulip Nathanael Arkor (Apr 30 2021 at 16:14):

Nathanael Arkor said:

Enriched algebraic theories aren't sufficient, because you want to consider pseudomorphisms.

(Though maybe these approaches would be a good starting point.)

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 16:15):

No no, as long as I have monadicity for the strict things, I can use Blackwell-Kelly-Power to deduce the results I want for the categories with ordinary morphisms!

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 16:55):

I think all of the pieces are here, even if they aren't explicitly put together by anyone. This isn't so surprising given that there's a lengthy set-up any time someone writes a new paper on 2-category theory; in order to sustain any momentum at all, one must have to lean fairly heavily on existing literature.
Ultimately, I think there is a lot buried in this abstract treatment. Take Lack's example of the theory of categories with a terminal object, for example: the data required to specify the 2-theory is significantly more voluminous than one might expect, and yet in practice the free terminal-object completion of a category is extremely simple to describe. While I intend to weave a path through the literature in order to extract the general existence results for my case of interest, I intend to get my hands dirty to provide an explicit construction of the free pullback-completion.

view this post on Zulip Mike Shulman (Apr 30 2021 at 18:04):

Morgan Rogers (he/him) said:

No no, as long as I have monadicity for the strict things, I can use Blackwell-Kelly-Power to deduce the results I want for the categories with ordinary morphisms!

At least as long as you have enriched monadicity, i.e. 2-monadicity.

view this post on Zulip Morgan Rogers (he/him) (Apr 30 2021 at 19:57):

Nathanael Arkor said:

I shall eagerly await your upcoming paper, Constructive colimit completions.

I know this was originally a tongue-in-cheek comment, but would either of you (@Mike Shulman, @Nathanael Arkor) be interested in collaborating in a short paper to this effect in the near future, depending on what Steve Lack's response is? Since I'm going to be doing it anyway and the two of you seem better-versed in the relevant issues and literature, I figure I might as well ask.

view this post on Zulip Spencer Breiner (Apr 30 2021 at 20:35):

Relevant
image.png

view this post on Zulip Nathanael Arkor (May 01 2021 at 01:31):

@Morgan Rogers (he/him): now that you've pointed it out, it's definitely an issue I'd like to see resolved. I'd be interested in discussing the neatest way to approach this.

view this post on Zulip Nathanael Arkor (May 01 2021 at 01:32):

I'd also be very interested to know why this theorem holds conceptually: what properties do you need in an arbitrary 2-category K (with enough structure to talk about weighted colimits, e.g. a proarrow equipment, or a KZ doctrine) for objects admitting a class of weighted colimits to be 2-monadic? Is it enough for K to be locally presentable, for instance?

view this post on Zulip Nathanael Arkor (May 01 2021 at 01:33):

But this is straying quite far from the concrete applications you have in mind :)

view this post on Zulip Morgan Rogers (he/him) (May 01 2021 at 10:50):

Morgan Rogers (he/him) said:

Nathanael Arkor said:

I shall eagerly await your upcoming paper, Constructive colimit completions.

I know this was originally a tongue-in-cheek comment, but would either of you (Mike Shulman, Nathanael Arkor) be interested in collaborating in a short paper to this effect in the near future, depending on what Steve Lack's response is? Since I'm going to be doing it anyway and the two of you seem better-versed in the relevant issues and literature, I figure I might as well ask.

Anyone else reading this who wants to be involved is equally welcome; message me directly if you prefer :grinning_face_with_smiling_eyes:

view this post on Zulip Tim Campion (May 01 2021 at 13:18):

Nathanael Arkor said:

I'd also be very interested to know why this theorem holds conceptually: what properties do you need in an arbitrary 2-category K (with enough structure to talk about weighted colimits, e.g. a proarrow equipment, or a KZ doctrine) for objects admitting a class of weighted colimits to be 2-monadic? Is it enough for K to be locally presentable, for instance?

I have not followed this whole conversation, but you might be interested in Power-Cattani-Winskel's "Representation result for free cocompletions" https://doi.org/10.1016/S0022-4049(99)00063-8 which shows that under some additional hypotheses, every KZ doctrine is a free cocompletion.

view this post on Zulip Tim Campion (May 01 2021 at 13:19):

Sort of the opposite direction from what you're asking, I suppose.

view this post on Zulip Nathanael Arkor (May 01 2021 at 13:47):

Tim Campion said:

Nathanael Arkor said:

I'd also be very interested to know why this theorem holds conceptually: what properties do you need in an arbitrary 2-category K (with enough structure to talk about weighted colimits, e.g. a proarrow equipment, or a KZ doctrine) for objects admitting a class of weighted colimits to be 2-monadic? Is it enough for K to be locally presentable, for instance?

I have not followed this whole conversation, but you might be interested in Power-Cattani-Winskel's "Representation result for free cocompletions" https://doi.org/10.1016/S0022-4049(99)00063-8 which shows that under some additional hypotheses, every KZ doctrine is a free cocompletion.

Yes, this is just as interesting. It would be good to be able to have an exact correspondence between cocompletions and nice KZ doctrines on a nice 2-category.

view this post on Zulip Mike Shulman (May 02 2021 at 00:21):

I'm happy to continue chatting about it, whatever is helpful. I doubt I'll have the time to invest in being a coauthor, but once it's finished you can ask again if you think I contributed a lot. (-:

view this post on Zulip Morgan Rogers (he/him) (May 03 2021 at 14:41):

Nathanael and I have taken it to private messages, but we might report back sooner or later :-)

view this post on Zulip Morgan Rogers (he/him) (May 05 2021 at 07:14):

I got a reply from Steve Lack; I'm awaiting his permission to share it here :smile: