agda-unimath
agda-unimath copied to clipboard
UniMath
The module index generator doesn't support modules with unicode characters in their names
Detected in #1025 when I tried having files including the string large-wild-⟨0,1⟩-precategories.lagda.md in their name.
While it's a discussion point whether filenames should ever contain Unicode (I don't see why not) a larger issue is that the CI fails silently.
Why would these file names have unconventional angled brackets? Aren't round parentheses always used in the literature when we talk about (n,m)-categories?
One reason to not have unicode in file names is that terminals don't have agda-mode, so it isn't easy to type unicode characters. I feel like unicode characters in file names is a definite no-no for this reason.
we can't have standard parentheses in module names sadly. And thanks for finding a reason :)
I think I would even omit punctuation characters in file names. How about wild-0-1-categories.lagda.md and friends?
I do find the notation of ⟨0,1⟩ in Large-Wild-⟨0,1⟩-Precategory quite cute though, although it's a bit of a hassle to type out
It's also super-wordy and I would like to look for alternative names.
How about calling a large wild precategory for a ~Metagory~ Premetagory? :)
The name Large-Wild-⟨0,1⟩-Precategory is suboptimal for a few reasons. First, it is just the baseline, so every additional adjective will have to be prepended making it even longer. Moreover, the index ⟨0,1⟩ is likely to be confused with the standard indexing scheme for categories where the first index refers to the depth of the hierarchy of the morphisms, and the second index refers to at which depth and onwards the arrows are invertible. But, as far as I can tell, that is not what the indices are used for here. (can we even make an inductive definition of a wild (n,m)-precategory?)
I guess it could be acceptible.
I have resisted hard in this library agains using symbols in unconventional ways, when the conventional symbols are unavailable for some technical reason. So that would be my main issue with this notation too, because the angled brackets usually are a mathematical operator. Here they are not used as a mathematical operator, but they are used instead of parentheses because parentheses aren't allowed.
That said, it is quite clear what is meant and therefore I think it can pass.
I do get wary of the potential introduction of infix notation Large-Wild-⟨_,_⟩-Precategory. Then we will be in a situation where the presence or absence of spaces makes the difference between how syntax gets interpreted, which I think is not really reader friendly.
If we can write down an inductive definition, then I like Wild-Precategory 0 1 better
How about calling a large wild precategory for a ~
Metagory~Premetagory? :)
Our large categories are called metacategories in Categories for the Working Mathematician, so I don't think the name metacategory is available for this.
Then the terminology seems to line up nicely, no? It's a (0,1)-approximation of a metacategory
Ah, because we have already established that categories are set-level structures