Contents

# Contents

## Definition

In homotopy type theory, given a type universe $\mathcal{U}$, a type $A$ is locally $\mathcal{U}$-small if for all terms $a:A$ and $b:A$, the identity type $a =_A b$ is essentially $\mathcal{U}$-small.