# 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$.