Contents

Contents

Idea

In formal logic and specifically in type theory, a resizing rule is an introduction rule which allows, under suitable conditions, to find a type that is in some type universe $U_2$ also in a smaller type universe $U_1$.

References

Last revised on March 26, 2015 at 19:18:16. See the history of this page for a list of all contributions to it.