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

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

Definition

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:ABf:A \to B, the propositional image im(f)\mathrm{im}(f) is essentially 𝒰\mathcal{U}-small.

See also

References

  • Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry book (2021)

Revision on June 16, 2022 at 13:14:45 by Anonymous?. See the history of this page for a list of all contributions to it.