16
$\begingroup$

I have noticed a very common missuse of tags: the tag [homotopy-type-theory] is frequently used where the tag [homotopy-theory] should be used instead. Just in the last few questions, two questions (Projective plane as a subcomplex of a 2-dimensional CW complex homotopy equivalent to $S^2$ and Constructing a map between suspensions that induces isomorphism on homology groups) were given the tag [homotopy-type-theory]. Yet they are not questions specific to homotopy type theory, but are just about general homotopy theory.

This may be caused by the close resemblance between the appearances of the two tags, and a possible lack of understanding of what the homotopy-type-theory tag is for.

This causes a few problems. First, it polutes the [homotopy-type-theory] tag. When someone (such as myself) searches that tag, we are faced with a bunch questions unrelated to the subject. Second, including this tag may lead viewers to believe that the author of the question is looking for a solution to the problem in the language of homotopy type theory. This is often a reasonable confusion, given the tag, since most of the mis-tagged questions are about homotopy theory. Third, the questions mis-tagged with [homotopy-type-theory] often fail to have the [homotopy-theory] tag. This means the question may not be seen by viewers looking for [homotopy-theory] questions.

Is there anything that we can do to remedy this? Of course, we can edit each mis-tagged question on a case by case basis. But I think this may be a common occurance, at least relative to the number of actual [homotopy-type-theory] questions. Even if nothing can really be done, I thought it was worth bringing this problem to the attention of some mods, unless of course this is a well known problem.

$\endgroup$
8
  • 4
    $\begingroup$ Perhaps a tag warning could be added: Do we want tag warnings, and for which tags? (They can only be added by SE staff, so it would involve persuading some of the CMs. But the first step would be to suggest the wording.) And also one could create a comment template and at it to this list. $\endgroup$
    – Martin Sleziak
    Commented Oct 23, 2023 at 5:57
  • 7
    $\begingroup$ As @MartinSleziak suggests, a warning could be useful. If someone who is more qualified than I could write a warning and post it as an answer, I can mark this question as feature-request and status-review so that the community moderation team can, perhaps, implement a warning. $\endgroup$
    – Xander Henderson Mod
    Commented Oct 23, 2023 at 12:38
  • $\begingroup$ @XanderHenderson Is there anything else I should do for this question? $\endgroup$
    – IsAdisplayName
    Commented Oct 23, 2023 at 22:42
  • $\begingroup$ @IsAdisplayName Like I said, I am not qualified to write a tag warning. If someone can do that, and post it as an answer, I can kick things up to the level at which someone can implement it. $\endgroup$
    – Xander Henderson Mod
    Commented Oct 24, 2023 at 12:34
  • $\begingroup$ @XanderHenderson by qualified, do you mean having more experience with math.stackexchange, or more experience with the difference between the subjects of homotopy type theory and classical homotopy theory? If the latter, I may qualify. If the former, well, I'm certainly not more qualified than you. $\endgroup$
    – IsAdisplayName
    Commented Oct 24, 2023 at 20:25
  • $\begingroup$ @IsAdisplayName I'm not a regular here, but I'm pretty sure they just want someone who understands the difference between the two subjects and can explain it such that a relative novice has a fighting chance to figure out which tag(s) to put on their question. I believe the idea is to show the message right as/after they choose homotopy-type-theory but before they post their question/edit? If there's any tricky SE syntax involved, I assume the mods/CMs can sort that out. $\endgroup$
    – SamB
    Commented Oct 24, 2023 at 21:06
  • 2
    $\begingroup$ @IsAdisplayName I know that homotopy-type-theory is some category theory nonsense, and that homotopy-theory has something to do with loops. I'm analyst---all of this is well outside my area of expertise. Someone who knows the difference (probably someone who actually knows homotopy type theory) should write the warning (and post it as an answer). $\endgroup$
    – Xander Henderson Mod
    Commented Oct 24, 2023 at 22:41
  • $\begingroup$ Okay, I wrote a draft. Happy to make any suggested edits. $\endgroup$
    – IsAdisplayName
    Commented Oct 26, 2023 at 1:00

3 Answers 3

Reset to default
10
$\begingroup$

We could rename the tag to HoTT, which I think is widely recognized by homotopy type theorists. Of course, that's not very descriptive, but people who don't know what it means can always read the tag description. And I don't think that people will pick it by accident; there's an extra letter and weird case to distinguish it from hot (which is strange enough that I wouldn't expect people to pick by accident much either).

$\endgroup$
1
  • 2
    $\begingroup$ Thats a very nice solution! Anyone who is familiar enough with the subject to be asking a question should know the acronym HoTT. $\endgroup$
    – IsAdisplayName
    Commented Oct 28, 2023 at 3:52
6
$\begingroup$

There is also a somewhat simpler solution exemplified by the tag entry for [hyperbolic-geometry].

Generally speaking, when I see a post about hyperbolas qua [conic-sections] which is tagged as [hyperbolic-geometry], I will simply edit the tag myself. Sometimes I'll even do a search on [hyperbolic-geometry] to clean things up. It's not an everyday occurrence, and so it doesn't take much vigilance or effort.

$\endgroup$
5
$\begingroup$

It was suggested in the comments that a warning attached to the tag [homotopy-type-theory] could solve the problem. Below I will write a draft of the warning. Since I have not written one of these before, I am happy to take any feedback and implement it.

You have added the tag to your question. Do you mean ?

  • should be used for questions on the use of type theory as a language for synthetic homotopy theory. Thus, only use this tag for a homotopy theory question if you want an answer to your question in the language of homotopy type theory. If you have not heard of homotopy type theory before, you do not want this tag.
  • should be used for questions about the theory of a homotopy between functions, or the more abstract contemporary counterparts. This includes questions about homotopy groups, higher homotopy groups, homology and cohomology, and other constructions form algebraic topology.
$\endgroup$
4
  • 2
    $\begingroup$ Missing word: "However, if [you] do not want..." $\endgroup$
    – KReiser
    Commented Oct 26, 2023 at 1:05
  • 1
    $\begingroup$ I'll be honest: this would not help me to know if I was using the tag correctly or not. Is there any way that you can distinguish between "homotopy type theory" and "homotopy theory" without using the word "homotopy"? $\endgroup$
    – Xander Henderson Mod
    Commented Oct 26, 2023 at 23:19
  • 3
    $\begingroup$ I've edited your answer to provide something of a template, which should maybe give you an idea of what is expected. All I know of homotopy theory is what I learned out of Munkres and Hatcher (which is to say, very little), and I know almost nothing about type theory, let alone homotopy type theory. It would help me if you could help to elucidate the differences. $\endgroup$
    – Xander Henderson Mod
    Commented Oct 26, 2023 at 23:41
  • $\begingroup$ thanks @XanderHenderson! $\endgroup$
    – IsAdisplayName
    Commented Oct 27, 2023 at 0:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .