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

Recent changes