5 ms·
The bird's eye overview of the univalence axiom is as follows. In homotopy type theory, we have in addition to familiar types like the type of natural numbers
by IngoBlechschmid 9y ago
The bird's eye overview of the univalence axiom is as follows.
In homotopy type theory, we have in addition to familiar types like the type of natural numbers or the type of lists of strings the "universe type U". Its inhabitants are the types themselves.
Just as we write "5 : Int", we can also write "Int : U".
The univalence axiom specifies when two inhabitants of U should be deemed equal. The remaining axioms of type theory don't settle this question.
- lgas 9y agoCan 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.