The axiom of replacement states that for every essentially $\mathcal{U}$-small type AA, every locally $\mathcal{U}$-small type BB, and every function f:A→Bf:A \to B, the propositional image im(f)\mathrm{im}(f) is essentially 𝒰\mathcal{U}-small.
Revision on June 15, 2022 at 22:28:50 by Anonymous?. See the history of this page for a list of all contributions to it.