# The type theoretic replacement axiom

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-03-02.

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

instance-replacement :
(l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) →
UU (lsuc l ⊔ l1 ⊔ l2)
instance-replacement l {A = A} {B} f =
is-small l A → is-locally-small l B → is-small l (im f)

replacement-axiom-Level : (l l1 l2 : Level) → UU (lsuc l ⊔ lsuc l1 ⊔ lsuc l2)
replacement-axiom-Level l l1 l2 =
{A : UU l1} {B : UU l2} (f : A → B) → instance-replacement l f

replacement-axiom : UUω
replacement-axiom = {l l1 l2 : Level} → replacement-axiom-Level l l1 l2


## Postulate

postulate
replacement : replacement-axiom

replacement' :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
is-locally-small l1 B → is-small l1 (im f)
replacement' f = replacement f is-small'


## References

[BBC+23]
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R Grayson. Symmetry. 06 2023. URL: https://unimath.github.io/SymmetryBook/book.pdf.
[Rij17]
Egbert Rijke. The join construction. 01 2017. arXiv:1701.07538.