New answers tagged type-theory
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
