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.

## References

Last revised on November 27, 2022 at 23:19:58. See the history of this page for a list of all contributions to it.