< [[nlab:type theoretic axiom of replacement]] ## Definition ## The __axiom of replacement__ states that for every [[essentially small type|essentially $\mathcal{U}$-small]] type $A$, every [[locally small type|locally $\mathcal{U}$-small]] type $B$, and every function $f:A \to B$, the [[propositional image]] $\mathrm{im}(f)$ is essentially $\mathcal{U}$-small. ## See also ## * [[universe]] ## References ## * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, [Symmetry book](https://unimath.github.io/SymmetryBook/book.pdf) (2021) category: not redirected to nlab yet