New answers tagged

0

There is a proof by using parametricity/logical relations framework or free theorems as mentioned in Zhao et al.[1] For instance, we can conclude that there is no closed inhabitant of type ∀α.α in a pure setting. If there were such a term, it must yield a value of any type at which it is instantiated, but there is no uniform algorithm to compute a ...


6

Without cummulative universes, if you have $A : \mathsf{Type}_3$ then you do not have $A : \mathsf{Type}_7$. Instead, we also have to introduce lifting functions $\iota_{i,j} : \mathsf{Type}_i \to \mathsf{Type}_j$ for all $i \leq j$ and write $\iota_{3,7}(A)$ to port $A$ from the third universe to the seventh one. But this is not all, we also want to know ...


3

Suppose you have X : Type0. What universe can X -> Type0 go in? It can't go in Type0, because Type0 : Type0 doesn't hold. Universes are presumably closed under function types, so we'd hope it can go in Type1 because Type0 : Type1. But without the subtyping rule, we don't know that X : Type1, we only know that it is in Type0. Now, you could instead say ...


Top 50 recent answers are included