Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I've felt for a while that what we call "double categories" might better be called "double 2-categories," since they are a lot more like "enhanced" 2-categories than they are like 1-categories. If we called them that, then "double bicategory" for Verity's notion would make perfect sense. Unfortunately "double category" is too entrenched to be changed by now.
But can we call them ‘double 2-categories’ in addition to their more prosaic and more common name? Or is that already established for internal 2-categories in some category of 2-categories?
I've never seen it used that way, but I think given the prevalence of "double category" for its current meaning, saying "double 2-category" for the same thing would just create additional confusion, and probably make some people think of internal 2-categories in 2cat whether or not it's been used that way before.
1 to 6 of 6