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.
Watching @David Jaz Myers's latest DOTS lecture and looking into the background reading, amazingly to me, systems theory seem to be pointing us towards 2-topos theory:
Since we may well need a logic to specify systems characteristics, this got me wondering how we might consider today @Mike Shulman's 2-categorical logic (aka 'The internal logic of a 2-topos').
From my memory of these things, Mike was working in this area in the years up to around 2010, after which HoTT appeared sweeping all before it.
At that point, the definition of a 2-topos was contested, a situation which persists today it seems:
The reason why we focus on 2- classifiers is that the rest of the definition of elementary 2-topos proposed by Weber is yet to be ascertained. We hope that this paper will contribute to reach a universally accepted notion of elementary 2-topos. (Mesiti, p. 1)
I see Matteo and David (Prop. 2.29) have profited from Mike's old note on classifying discrete opfibrations, but what of the logical insights from back then?
About the logic, Mike wrote at the time:
My current opinion is that there already exists a “logic which treats sets as truth values,” without the need for any categorification, namely type theory (more precisely, dependent type theory).
Since the 2011 shift was from 2-toposes to -toposes, might one save time by jumping straight to -toposes and their internal logic as some kind of [[directed homotopy type theory]]? Is it likely that anything useful to say about 2-categorified logic will emerge here?
The idea that the whole topic of 2-categorical logic should be somehow referred to Shulman, who has no publication nor preprint on the topic, is incredibly strange (and simply unfair) to me.
The note on "classifying discrete opfibration" is only a report (and a very light elaboration) on the work of Weber and is admittedly not due to Shulman.
It is also simply not true that people are not working on 2-categorified logic (even in the narrow sense presented in this post). In the last years (after 2018) (at least) the following people have contributed (in different capacities and different flavours) to the topic: Arkor, McDermot, Descotte, Szyld, Dubuc, Osmond, Miranda, Hughes, Mesiti, Caviglia, Nasu, Walker, Myers, Lambert, Bourke, Ko, Mimram, Capucci, Koudenburg, Hoshino, (Osser, Jelinek), (Abellán, Martini)). All these people have actual publications (often 50+ pages long), master or PhD theses on the topic.
To provide a little more context for part of Ivan's comment: just as 1-topos theory provides a synthetic treatment of set theory (= 0-category theory), 2-topos theory might be expected to provide a synthetic treatment of category theory, which is essentially the subject of [[formal category theory]]. I think many people would argue that the appropriate structure for such a synthetic treatment is double categorical in nature, not 2-categorical. In this light, all of the recent work on formal category theory in (augmented) (virtual) double categories can be seen as part of this programme.
Nathanael Arkor said:
To provide a little more context for part of Ivan's comment: just as 1-topos theory provides a synthetic treatment of set theory (= 0-category theory), 2-topos theory might be expected to provide a synthetic treatment of category theory, which is essentially the subject of [[formal category theory]]. I think many people would argue that the appropriate structure for such a synthetic treatment is double categorical in nature, not 2-categorical. In this light, all of the recent work on formal category theory in (augmented) (virtual) double categories can be seen as part of this programme.
A programme that does not belong to anyone.
Oh dear, I've blundered in here with clumsy phrasing. I should have characterised things in terms of my own limited state of knowledge, and asked people to fill in the gaps of my ignorance.
Apologies for the upset caused, and thanks for the answers.
I was about to say, at last CT I saw a talk mentioning '2-topoi' just about every session. Now whether this counts as doing '2-logic', I don't know. I certainly would love a more cohesive exposition than what's around.
As David observed, Mike's nLab notes are readily accessible and hence why we cited them (specifically, a theorem about the equivalence of classifiying via commas rather than via pullbacks).
David Corfield said:
Watching @David Jaz Myers's latest DOTS lecture and looking into the background reading, amazingly to me, systems theory seem to be pointing us towards 2-topos theory
I'm glad you like this! :D
Viewed from my own limited trajectory, it's very surprising. In 2006, I went into the -Category Cafe venture (with John and Urs) with simplistic ideas on categorifying parts of mathematics. Categorified geometry was foremost for me, reaching (as far as I know) the development outlined at [[higher Cartan geometry]]. But we also spoke about categorifying logic. I remember John telling me some such ideas in Minneapolis in 2004.
Then Mike joined the nCafe, and the last I heard of an explicitly categorified logic was his Stack semantics. It seemed to fit with the Baez and Dolan sense of categorification:
Intriguing then to be steered back into this world and the chance to catch up on all the ideas devised since, and the many I'm sure I didn't know from earlier.
A good starting point to enter the modern development of the topic is the PhD thesis of Luca Mesiti Aspects of 2-dimensional Elementary Topos Theory (240+ pages). The thesis recaps on the relevant literature and makes a quite fair representation of the real contributions of past authors to the sedimentation of these notions. Quite correctly, the thesis makes no reference to anything by Shulman, as no contribution was ever provided to this topic by him. What Shulman did was a popularization of a programme that -- if by anyone -- had been envisaged by the Australian school and more precisely by Street (for the Grothendieck part) and Weber (for the elementary part).
It's worth clarifying in the context of my earlier comment that "2-dimensional" in the title of the thesis really means "2-categorical"; you won't find the literature relevant to formal category theory referenced in the thesis.
It's so great how the Internet preserves everyone's youthful indiscretions for all time and uses them to provide fuel for the flame wars that keep it running.
There was a time when I was young and naive and thought it was a great idea to do mathematics in public view, so that anyone can read it, see what's going on before it gets published, and even contribute as it's developing. Sometimes this works, when it actually leads to something publishable. But when it doesn't get that far, then we're stuck with half-finished notes that are already public, so that some people may have read them and cited them and thus we don't want to just disappear them, but also they haven't been published or peer-reviewed and so they shouldn't "lay claim" to a subject or dissuade other people from working on it and getting the deserved credit for making things work.
If anyone has a suggestion for what better thing I could do with those lab pages, short of going back in time and crushing the soul of youthful-me by telling him not to create them in the first place, I'd be happy to hear it.
maybe add a big disclaimer at the top with the current date and the context you just provided? like a new 'foreward' for an old book?
TBH most people who make such notes won't have any such problem, because nobody will notice them in the first place until (and unless) something is actually published.
@Ivan Di Liberti I would consider popularisation of a subject (cf the work of John Baez spreading massive awareness of CT) as a contribution to the subject, even if no novel theorems appeared in a published article, or even a preprint. (not to say John has no contributions, but there are certainly matters he wrote about but published little-to-nothing on)
And note that the nLab is a weird beast, a mix of research notes from reading the literature, reformulations of existing material, novel results or perspectives, and then actual new theorems; private 'webs' (as Mike's space with the 2-categorical logic is) are then even more unregulated, and as Mike said, doing mathematics in public can be messy and incomplete and sometimes abandoned (and certainly rigorous citation practices in one's personal notebook might just be not universally practiced...)
I still think the young and naive approach of doing mathematics in public view is great. I suspect that on average having half-finished notes lying around in public view is a stimulus to work - people see them, are inspired or dissatisfied, and try to go further.
If you want, @Mike Shulman, you could just stick something on top of your old tentative notes saying they're old tentative notes and you encourage people to work on this stuff. (And if you know further work on this stuff, you could list some of it, so it's very clear your old tentative notes aren't the last word.)
As a meta-comment, though Ivan's posts made no explicit accusation, from the negative tone they come across to me as having been intended to imply that Mike/David are culpably assigning Mike credit he is not due. It seems pretty clear that Mike just posted some thoughts 15 years ago that for contingent reasons happen to be both the top Google result for "2-topos" and the last thing David heard about the topic, while everyone involved is happy to take reasonable measures to be sure credit ends up where it's due; even if this were less clear, I think one should be more generous in considering what would really be rather serious misconduct as an explanation for this kind of situation and, if such misconduct really does seem to have occurred, more direct in making the accusation.
FWIW, I didn't interpret Ivan's comments as suggesting intentional misappropriation of credit. I assumed he was just frustrated because this case seems to fit into a common pattern where a well-known name gets credit for conjecturing or popularizing something at the expense of the less-established people who actually do the work of proving it.
Yeah, that's hopefully right; I continue to think it's a good idea in this situation to be clear whether one is expressing general frustration at structural issues or accusing particular individuals of doing something wrong.
I think that's true in all situations. But to be fair, there are also degrees of "doing something wrong". At one end of the spectrum is active dishonesty, and on the other side are angels. Somewhere in the middle is "failing to take action that you could have taken to mitigate a structural issue". But we should let Ivan speak for himself. (-:
Kevin Carlson said:
It seems pretty clear that Mike just posted some thoughts 15 years ago that for contingent reasons happen to be both the top Google result for "2-topos" and the last thing David heard about the topic
Thanks, Kevin. To clarify, I did know of recent work going on regarding 2-toposes. What I was asking about was how to think of "2-logic". Back in the day (2008), I would pose hopeless naive questions to my learned friends:
Just as @John Baez was categorifying parts of the mathematical world and mathematical physics, the vague question was what a categorified logic looked like. It was never terribly clear what precisely was to count as success here.
Here I was largely asking (clumsily), with the advantage of many years, how would one answer the younger me. Maybe the question is too vague, but if it isn't (and Ivan gave me a list of people he considered to be working on 2-categorified logic), how would one characterize it today?
Is anyone explicitly couching what they're doing in terms of categorification, not just of 1-toposes to 2-toposes, but of logic itself?
But then perhaps that term has moved on since we used to talk about such things: What is categorification?
I would recommend @Hayato Nasu's An Internal Logic of Virtual Double Categories, which gives a two-dimensional type theory for formal category theory, which can be seen as a form of categorification of logic for "formal set theory".
Thinking back to the atmosphere in which I was posing these questions, I was constantly up against philosophers who claimed to be open to learning of category theory's philosophical significance, but were yet to be convinced. Here's an example from 2007. As I say in response, it was unclear to me what would count as success in view of what had already been achieved, but I could see that if category theory could aid some breakthrough in philosophical logic that might be convincing to more people.
When @John Baez had suggested to me in 2004 that 2-logic was a kind of modal logic my eyes lit up. Modal logic is beloved by analytic philosophers as the key to the metaphysical treatment of necessity and possibility. But this idea never came to fruition and later my attention was drawn away to modal HoTT. Hence the book, and attempts to relate it to topics in, say, philosophy of language.
Now for the past year, I've been propelled into the world of applied category theory where double categories reign. I had a brief exchange with Hayato about his thesis (Nathanael's suggestion) in a thread on Peirce and logic. The ideal thing for me would be have a piece of recognisable good reasoning (outside of pure mathematics) that is shown to be well-represented by a categorified logic.
So then this week seeing systems theory reaching for 2-toposes gave me a tiny glimpse of an opportunity. Perhaps the specification language for systems behaviour could be derived from a corresponding (categorified) logic.
As someone working on a higher-logical type theory of my own, albeit in the early stages, my perspective is that while it may at times include tools from conventional logic like modalities, higher logic embodies a different kind of reasoning than conventional logic.
Conventional logic is about what statements you can prove with arguments. Higher logic encompasses this as a special case, but it's really about what specifications you can satisfy with constructions and (the higher part), how you can relate these different constructions. You already see the beginnings of this, including its inherent favoring of constructive logic, in Martin-Loef Type Theory, which is why it was able to become the basis for Homotopy Type Theory and its offshoots.
With conventional logic you manipulate constructions with "tongs", proving the existence of specified objects in your semantic universe, but the actual objects are never directly manipulated by the logic. It has the same technical expressive power, but higher logic can capture reasoning involving constructions of objects and their covariance in much more natural and fluent ways.
While this is more your domain, I feel that the philosophical impacts of the existence of higher logics include that covariance and simulation can reasonably be taken as fundamental to aspects of ontology like object identity and of epistemology like the meaning of knowledge.
Interesting! If you have anything in this area to share, I'd love to see it.
In the realm of physics, it's possible to give a HoTT rendition of general covariance. In my book I was suggesting some much simpler form of this in the context of identification under symmetry (via dependent pair and dependent function in the context of a (delooped) group (following on from this blog post). Might this come close to what you mean by covariance and object identity?
This indeed seems related! There's also obvious applications to things like the meaning of knowing things about the morning star and the evening star if you're not aware they're both the same thing. But higher logics also give you the chance to conceive of things that are only "kind of like" object identity, like being related by a noninvertible function, or being "approximately the same" or being "indiscernible" in the logic sense, as having potential metaphysical significance.
Mike Shulman said:
If anyone has a suggestion for what better thing I could do with those lab pages, short of going back in time and crushing the soul of youthful-me by telling him not to create them in the first place, I'd be happy to hear it.
I guess the current plan is to keep meeting every year or so in some online forum to have this conversation again and again, while the passive income coming from those pages -- platforming 24/7 -- remains untouched. Sounds fun.
After writing this comment I was privately encouraged to make a constructive criticism concerning how to solve the issue. My recommendation is to take down the pages. I don't think they are doing any good to anyone besides Mike himself at this point. As I have argued other times, I think (a) they are actually being detrimental to the development of the field, and (b) they are vastly misleading towards a fair attribution of people's efforts.
Something I'd like to see is a current resource indicating the latest thinking on the subject. An nLab page would be one option.
David Corfield said:
Something I'd like to see is a current resource indicating the latest thinking on the subject. An nLab page would be one option.
One reason for which this page does not exist is precisely the existence of Mike's pages.
Another one is the fact that the programme has many souls that is not easy at all to coordinate, and probably should really not go under one only label.
In the latter sense, several pages already exist and they correctly list a lot of the literature I suggested above.
One reason for which this page does not exist is precisely the existence of Mike's pages.
I don't this is an assertion one can make without strong evidence, no matter how amenable one is to the idea that Mike's personal notes on the topic should be updated to refer to prior (or subsequent) art.
The most active contributor to the nLab is interested in topic disjoint from these notes, and in any case literally anyone is free to start a serious page with citations on the nLab proper. Like, right now.
Did you, Ivan, personally feel you couldn't start such an nLab page before now due to the presence of these notes, despite knowing other references? I agree it might be intimidating. But the nForum is there to discuss suggested pages if one is unsure how to start.
I see we have a meagre and very old page [[2-logic]]. I don't see why this page couldn't act as an anchor to refer to the other pages you mention. I also don't see why there couldn't be some kind of overview provided. Coordination can be a good thing if handled sensitively.
David Michael Roberts said:
I agree it might be intimidating.
The fact that you agree with this proves my point, together with a minimal knowledge of topological dynamics, conservation of energy, and understanding of how incentives work for individuals in a society.
David Corfield said:
I see we have a meagre and very old page [[2-logic]]. I don't see why this page couldn't act as an anchor to refer to the other pages you mention. I also don't see why there couldn't be some kind of overview provided. Coordination can be a good thing if handled sensitively.
I would claim that If one reads this page in its current form it becomes harder and harder to disagree with me.
?? It was just a stub Urs created 14 years ago, ready for people to make something of it.
There's also [[2-type theory]].
If there's something that connects the contributions you mention, it must surely be possible to say something about what this is.
Ivan Di Liberti said:
David Michael Roberts said:
I agree it might be intimidating.
The fact that you agree with this proves my point, together with a minimal knowledge of topological dynamics, conservation of energy, and understanding of how incentives work for individuals in a society.
The primary source of intimidation, normally, is making your first nLab page at all, not the prior existence of some notes on someone's personal sub-lab. Somebody named "nw" already added some published references to [[2-logic]] (and, I notice, removed the crosslink to Shulman's notes) so clearly this wasn't too intimidating for somebody to do. (Maybe it was even you--this is somebody without any prior edits so it's hard to say who it was.)
It wasn't me.
Ivan Di Liberti said:
It wasn't me. (Your theory is genuinely funny, I am doing all of this under everyone's eye and I am telling very directly to Mike my opinion, why should I suddenly start doing it under cover?)
Doing something with a username I don't recognize is not the same as doing it "under cover". For all I know it could have been a username you use elsewhere. I just didn't know if it was you or not because I'm not that familiar with your online presence apart from here.
Ivan, I really don't think it's appropriate for Mike to delete something that people have been citing intermittently for 15 years, a point which he already made earlier. Indeed the existence of those citations means that the credit you claim he's getting incorrectly assigned is already in, so to speak, the permanent record; if he would delete them, you'd just have a conversation in two years where somebody asks whether anybody has a copy of Mike's old notes on classifying discrete opfibrations that Matteo and David cited (well, in this case it would just be on the Wayback Machine.) So I don't see how that's an actionable suggestion.
Several people have supported the idea of adding a disclaimer to those articles that have never led to a publication, and I agree this would be a good idea. But it would be an awful lot stronger if the disclaimer could include a link to an nLab page that's actually a better place to start. It would be a clear improvement if you would simply chuck the 20 papers you knew off the top of your head would be appropriate to mention in an article on 2-logic into the article on 2-logic which you mysteriously seem to claim you don't even think should exist. Even if it's just a list of links to other topics fleshing out various things people didn't realize were what they really wanted, such a list would self-evidently be helpful: the only reason this conversation is possible is because people keep searching for topics that have no more accessible answer online than Mike's notes. Your flurry of citations proves you are one of a small handful of people best qualified to do this writing; if you care about fixing this problem as well as about airing your grievances, you should really do it.
@Mike Shulman Did you have a response to Ryan's and John's idea of adding a disclaimer that these articles were based on preliminary notes that didn't lead to publication?
That's a good suggestion. I've added such a disclaimer to the front page of the notes:
Important Note: This is a collection of preliminary personal notes from approximately 2009-2012. None of them has been published or peer-reviewed, and in the years since they were written, a number of other authors have pushed the theory forward in published papers. I am keeping these notes available for reference, since they have already been cited by others. However, I recommend that when published references exist, they should be cited in preference to these notes.
As with pages on the main nLab, these notes are publicly editable. In particular, I encourage readers to add citations to published references on individual topic pages, for the convenience of later readers. (I simply do not have the time or knowledge to do that myself.)
I'm open to suggestions for improving the wording. Ideally there would be such a note on every sub-page as well, but I don't have the time to add such things by hand.
If someone makes a list of current references, I can add a link to that list from the disclaimer.
As Kevin said, it's not practical to simply remove the pages, because they've been cited and people will want to read them. I also can't agree with your claim, Ivan, that these notes don't contribute anything to the subject. Some of them simply exposit and systematize existing definitions, but others of them introduce new definitions and prove new results.
I'm sorry that I haven't done anything to address the problem before now, but I feel like there's a limited amount I can do about it. I feel like the problem would be much the same if I had published these notes in a journal, in which case there would certainly be nothing to be done about it. I can't help it if people see me having worked in some area and feel intimidated out of working on it themselves. The main difference I see between the wiki notes and a published paper is that the wiki notes look at first glance as though I'm still working in the area, unless you notice that they were last edited 15 years ago. Hopefully the new disclaimer will help mitigate that.
I just created a very drafty bibliography that I am trying to dump on the nlab. It's only a starting point though, and it will need some (a lot of) additional curation.
The tentative bibliography does not include some stuff on which I would ask @Nathanael Arkor to chime in. I am tired. Love you, Nath.
Great. And please, someone, a couple of paragraphs on what the topic is about.
Ideally someone with a grasp of the literature and strong ideas about the topic ^_^
I'd really not play the role of the go-between, but the recent additions to the nLab page have prompted Urs to write on the nForum:
I suggest that anyone who cares that the public gets the impression that people besides Mike have seriously thought about 2-categorical logic should revise at least the random-looking list of references in the entry here, adding commentary to clarify where in the articles listed what kind of 2-categorical logic is actually considered, if any.
I agree.
I do not think there is any chance I can participate to this conversation without being banned from the forum. Goodbye.
Portions I what I wrote on the nlab are being taken down as we speak. Lol. That’s quite ironic @Mike Shulman, isn’t it? :face_vomiting:
If you wish the material to be kept on the nLab, it needs to be contextualised as to why it should be on the page. A laundry list of references that is not clear about the relevance on any page, by any person, would be tidied up. This is not about you, or this page, or Mike's notes. Also, since anyone can edit the nLab, your contributions will inevitably be edited at some point. If you believe in this so strongly, put in the effort to make the page clear why all those references are about (2-)logic, and not merely citations by someone writing about (2-)logic.
Please take this advice as an honest attempt at helping your knowledge be preserved. If it isn't clear why you have cited x or y paper, and you mean to come back to expand, add an "under construction" notice, or note in your change message for the nLab/nForum that edits to add context are forthcoming. This is editing etiquette.
Constructive criticism of draft work in academia is not usually intended as admonishment or to be discouraging; on the contrary, it shows that someone thinks enough of the work to warrant deep thought and engagement with it aimed at improvement. Peer review is tough, but as they say, it takes a tough chef to make a tender chicken.
In case anyone was wondering, the page https://ncatlab.org/nlab/show/2-categorical+logic is definitely coming along. References to Ivan's work now outnumber Mike's 4:1. And there are dozens of interesting references grouped thematically with a description on why each is relevant to the page.
I agree, the list looks great, and so on point! Whomever put it together must be a true expert in the field, someone whose opinion seems worth listening to! Possibly this person may be in the position of evaluating contributions to the field more accurately than others! It would sound obscurantist if a collection of people collectively and repeatedly made fun of them. Eppur si muove.
I also see that you are very keen on Mike's representation in the list, you could convince him to write some papers on the topic! I personally would love to read them. You know, unfortunately that's the only way to make it in the list among us scientists.
Learning to conform to the stylistic and organizational quirks of a wiki well enough for major edits to last is always a painful process, even for subject matter experts. And it seems especially unfair when you're filling in a stub, because the bigger the page gets the higher the standards get, and you don't have examples of style locally so you have to scrub around in the edit views of other pages to find what you need even for basic styling.
The nLab is far more forgiving than Wikipedia, mainly because it's much smaller. You can just dump stuff in, in any format, and if the material itself is mathematically good someone will fix the formatting.
Indeed it's not clear to me, Ivan, whether anything was deleted from the list or just rearranged or formatted?
After some initial resistance, the list currently the one I uploaded.
@Ivan Di Liberti I was being genuine, and wanting to let people here know the good progress who might not be checking the nLab edits
John Baez said:
You can just dump stuff in, in any format, and if the material itself is mathematically good someone will fix the formatting.
Within reason, and with gracious requests for help on the nForum. It's hardly fair to expect people to clean up after
“
arXiv: https:// [arxiv.org/](http://arxiv.org/) abs/ 2401.16900"
Once upon a time, I left this Zulip because I felt that certain viewpoints being expressed in here might bring disrepute to category theorists, and I had reached the end of my own ability to engage constructively on the topic (in fact, I should have left before I reached that point). I still feel this way, but after reading this thread, I felt strongly that I needed to step in with one remark.
The (both veiled and unveiled) hostility to @Mike Shulman in this thread is really uncalled for. I know Mike doesn't need me to defend him. There are so many snide remarks being made in here, and I don't think it will be constructive or helpful for me to refute all of them individually. And it's worth saying that it is fine to criticise people. But what I am seeing here is vendetta of the most inappropriate and disreputable kind.
I will say for the record that (1) I have never ever seen Mike Shulman claim to be the driving force behind 2-dimensional logic, (2) it is not the case that having public learning-notes on the topic constitutes an implicit claim of priority, (3) it is not the case that notes need to be carefully referenced, (4) several people in this thread, including Ivan, have done excellent published work in 2-dimensional logic and it does not appear that they have been thwarted in doing so by Mike's (non-)priority on the topic, and (5) there is no such thing as "passive income" coming from wiki pages, and (6) if you are worried about what is on the nLab, please keep in mind that literally nobody who matters is looking at the nLab and that it really is a nothing more than a lab notebook from the 2010s filled with creative speculation from a small community of people who intended no harm.
I encourage people to take a deep breath, and consider whether it is healthy to invest so much energy into a vendetta against someone who in this case has done, so far as I can tell, no harm at all. I will say for my own part, I'm happy Mike's notes exist, and I'm also happy that all the publications by other authors mentioned in this thread exist. When I do work that involves 2-dimensional logic, I cite the latter because publications are the thing you cite. But I'm also happy to acknowledge my gratitude to Mike for all the effort he has taken to digest and explain the ideas that so many people have worked on, and provide accessible introductions to areas of research that can be difficult to get a handle on.
I suggest to the moderators that this thread might best be locked. Nobody should have to endure the kind of outrageous accusation of harm that are being allowed to pass here, and perhaps everyone would do well to have a break.
P.S. I will not be replying further, as my intention is not to spark a debate.
Jon Sterling said:
please keep in mind that literally nobody who matters is looking at the nLab
Now I’ll keep wondering who the people in category theory who really matter are. :sweat_smile:
(sorry, I just wanted to add a pinch of humor)
I suspect it was meant bean counters at universities or funders, the ones that to some extent have a heavy finger on the scales of academic careers.
The discussion was about other researchers, though, not universities/funding bodies, and it is certainly true that other researchers are making use of the nLab.
Discussion of that nLab page [[2-categorical logic]] is ongoing at the nForum here. Respectful contributions are of course welcome.