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 May 1, 2022 at 22:55:59 by Anonymous?. See the history of this page for a list of all contributions to it.