Small types

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

Created on 2022-02-17.
Last modified on 2025-10-28.

module foundation.small-types where

open import foundation-core.small-types public

open import foundation.dependent-pair-types
open import foundation.images
open import foundation.locally-small-types
open import foundation.replacement
open import foundation.surjective-maps
open import foundation.uniqueness-image
open import foundation.universal-property-image
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.homotopies

Properties

If f is a surjective map from a small type into a locally small type, then replacement implies that the codomain is small

is-small-is-surjective :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
  is-surjective f → is-small l3 A → is-locally-small l3 B →
  is-small l3 B
is-small-is-surjective {f = f} H K L =
  is-small-equiv'
    ( im f)
    ( equiv-equiv-slice-uniqueness-im f id-emb
      ( f , refl-htpy)
      ( is-image-is-surjective f id-emb (f , refl-htpy) H))
    ( replacement f K L)

See also

• Small maps
• The is-essentially-in-subuniverse predicate in foundation.subuniverses

Recent changes

• 2025-10-28. Fredrik Bakke. Morphisms of polynomial endofunctors (#1512).
• 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).
• 2023-10-21. Fredrik Bakke. Preunivalence holds in univalent foundations (#874).
• 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
• 2023-06-07. Fredrik Bakke. Move public imports before “Imports” block (#642).