3 ms·
Calling those “types of types” is highly misleading. The term “type of types” has a very precise technical meaning: https://ncatlab.org/nlab/show/type+of+types
by catnaroek 11y ago
Calling those “types of types” is highly misleading. The term “type of types” has a very precise technical meaning: https://ncatlab.org/nlab/show/type+of+types https://ncatlab.org/nlab/show/type+of+types
- andrewprock 11y agoI guess there are different types of "types of types". :/
- gclaramunt 11y agoAlso, kinds can be viewed as the "types" of types, right?
- catnaroek 11y agoSure. If your hierarchy (values, types, etc.) stops at kinds, I'd rather call them kinds, but even TAPL informally explains kinds as “the types of types” (p. 441, quotation marks in the original).