Does types being terms imply your dependend theory is considered polymorphic?
-
30-10-2019 - |
Question
In the introduction of the book by B.Jacobs, "Categorical Logic and Type Theory" (it's online here), he classifies type systems into three general flavours: Simply typed ones, depended typed (term depended types) and polymorphic types (type depended types). He says also there are also mix types.
Now if you start out with a dependently types theory and introduce transitive universes, hence forcing types on the level of terms, are you automatically speaking of a polymorphic type system then?
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange