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
scroll top