Homotopy Type Theory axiom of replacement > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

The axiom of replacement states that for every essentially $\mathcal{U}$-small type $A$, every 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 (2021)