Different readers will have different questions in mind. A reader who already has a permanent position will not be asking your question. A reader who is interested in a permanent position below the R1 level, where prestige of the journals you publish in matters less, may also not be asking your question. And in any case, I think that in general, the total number of papers published in a given field is an even worse proxy for name recognition or impact factor than it is for the likelihood of a new article being accepted, even if it happens at the moment that some of the same journals appear high or low on both rankings.
]]>Hmm, okay, if that’s what you want. I guess I feel like the total number of articles published in a particular area may not be all that useful as a proxy for what is likely to usually be the real question a reader has in mind, namely “what are the chances of my article in this area being accepted here?”. I don’t know for sure, but I suspect that the main reason Compositionality and Higher Structures don’t publish a lot of papers is that they’re fairly new and people don’t submit a lot of papers to them, and my instinct is that a pure category theory paper (for instance) is more likely to get a sympathetic reception there than at a journal like TAMS even if the total number of papers published by TAMS is greater.
Also, how many of those TAMS papers are actually in category theory? Even if homotopy theorists face the same kind of journal challenge as category theorists, is their problem really always solved by the same journals? If we do want to also track journals publishing homotopy theory, maybe the list should be separated into two.
]]>I think the supposed ordering of this list is way off in many other places. E.g. I don’t think TAMS or Documenta Mathematica publishes more homotopy theory and category theory than Compositionality or Higher Structures.
Personally, I think this supposed ordering is too difficult to maintain. My inclination would be to order the journals alphabetically and just add a “comments” field indicating what we think about how many articles it publishes. Or we could separate them into groups by specialty such as categories, homotopy theory, logic, algebra, and generalist, which would probably be about as useful as the ordering.
]]>Added a section on examples.
]]>For instance, couldn’t you have a “logic” for skew-monoidal categories?
]]>I don’t think associativity of tensor is necessarily required in order to call something a “logic”.
]]>I mean, can you point to a specific reference that says that? Maybe sometimes people say “isomorphic types are equal” in informal surveys, but the HoTT Book for instance uses “equivalence” for sameness of types and reserves “isomorphism” for equivalences between 0-types, and in my experience this is the most common terminology.
]]>Isn’t this discussed on the page, in the section “from ternary frames to quantales”?
]]>Added some description of proof assistants and libraries.
]]>Thanks. FWIW I think a page like this serves a different purpose than an !include
file, even apart from the specificity to libraries and to HoTT-related ones: an include-file is mainly a contents list of links, whereas this page can include brief descriptions of the libraries and comparisons between them.
I also think that “equifibred” meaning pullback squares is significantly more common than “equifibration” meaning equivalence-lifting. So although it’s not exactly a “clash” per se, it’s potentially confusing. I could live with “weak 2-isofibration” although I would prefer “equiv-fibration”.
Who are these type theorists who have discarded “equivalence”?
]]>Added some more details about Lack’s model structure.
]]>I don’t like “equifibration” – it sounds to me like something related to an equifibered natural transformation. I suggest we go back to “equiv-fibration”.
]]>Fix definition of semi-strict equivalence
]]>The list of code repositories on https://www.homotopytypetheory.org is very out of date, so in an attempt to crowdsource creating a replacement and keeping it up to date, I’m making a wiki page instead.
]]>It looks like Remark 2.2 is also false unless this axiom is added, since a normed group includes the axiom .
I wonder if Berkovich just made a typo?
]]>To be consistent with the other cases, I think so, yes. Although of course every groupoid is isomorphic to its opposite.
]]>Stub
]]>Ah, there’s also a unit condition that was omitted. I added it, and also uniformized the notation.
]]>Perhaps not. Maybe I misunderstood the comments in the Fröhlich-Moser paper about their approach being different.
]]>Replace HTS by 2LTT, which is the modern version.
]]>Yes, I think that’s right. But I thought the two definitions of non-discrete double fibration were not equivalent?
]]>I reworded that a bit, is this okay?
]]>It seems that the definition of semi-strict equivalence on this page can’t be right. Shouldn’t they be the ordinary sort of “homotopy equivalences” defined using the semi-strict interval ?
]]>