The replacement axiom for type theory
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-03-02.
Last modified on 2023-06-08.
module foundation.replacement where
Imports
open import foundation.images open import foundation.locally-small-types open import foundation.universe-levels open import foundation-core.small-types
Idea
The type theoretic replacement axiom asserts that the image of a map
f : A → B
from a small type A
into a locally small type B
is small.
Statement
Replacement : (l : Level) → UUω Replacement l = {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-small l A → is-locally-small l B → is-small l (im f)
Postulate
postulate replacement : {l : Level} → Replacement l
replacement-UU : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-locally-small l1 B → is-small l1 (im f) replacement-UU f = replacement f is-small'
References
- Egbert Rijke, Theorem 4.6 in The join construction, 2017 (arXiv:1701.07538, DOI:10.48550)
- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Section 2.19 of Symmetry (newest version, GitHub)
Recent changes
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).