The type theoretic replacement axiom

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

Created on 2022-03-02.
Last modified on 2023-12-10.

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

  • Egbert Rijke, Theorem 4.6 in The join construction, 2017 (arXiv:1701.07538)
  • Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Section 2.19 of Symmetry (newest version, GitHub)

Recent changes