Small types
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-17.
Last modified on 2024-04-17.
module foundation.small-types where open import foundation-core.small-types public
Imports
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
Recent changes
- 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).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).