Showing changes from revision #2 to #3:
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.