Contents

# Contents

## Definition

In homotopy type theory, the axiom of replacement states that given a type universe $\mathcal{U}$, for every essentially $\mathcal{U}$-small type $A$, every locally $\mathcal{U}$-small type $B$, and every function $f:A \to B$, the image $\mathrm{im}(f)$ is essentially $\mathcal{U}$-small.