Showing changes from revision #1 to #2:
Added | Removed | Changed
The axiom of replacement states that for every essentially $\mathcal{U}$-small type , every locally $\mathcal{U}$-small type , and every function , the propositional image is essentially -small.