3 ms·
Can you write "U : _"? If so, what fills in the blank? It seems to parallel "Value :: Type", "Type :: Kind", and "Kind :: Sort" from FP.
by lgas 9y ago
Can you write "U : _"? If so, what fills in the blank? It seems to parallel "Value :: Type", "Type :: Kind", and "Kind :: Sort" from FP.
- IngoBlechschmid 9y agoIndeed, homotopy type theory employs a stratified approach to this question. That is, what I've written "U" would more formally be written "U_0". We then have U_0 : U_1, U_1 : U_2, and so on. All the base types are inhabitans of U_0, that is we have Int : U_0, String : U_0, and so on. In functional programming parlance, we'd have U_0 = Type, U_1 = Kind, U_2 = Sort. There's a thing called "typical ambiguity" which allows us to drop the index in most cases (and let it be automatically inferred).
- lgas 9y agoThanks. HTT sounds interesting. I'll have to investigate further.