Small maps
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-17.
Last modified on 2023-09-06.
module foundation.small-maps where
Imports
open import foundation.dependent-pair-types open import foundation.locally-small-types open import foundation.universe-levels open import foundation-core.fibers-of-maps open import foundation-core.propositions open import foundation-core.small-types
Idea
A map is said to be small if its fibers are small.
Definition
is-small-map : (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (lsuc l ⊔ l1 ⊔ l2) is-small-map l {B = B} f = (b : B) → is-small l (fiber f b)
Properties
Any map between small types is small
abstract is-small-fiber : (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-small l A → is-small l B → (b : B) → is-small l (fiber f b) is-small-fiber l f H K b = is-small-Σ H (λ a → is-locally-small-is-small K (f a) b)
Being a small map is a property
abstract is-prop-is-small-map : (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-prop (is-small-map l f) is-prop-is-small-map l f = is-prop-Π (λ x → is-prop-is-small l (fiber f x)) is-small-map-Prop : (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → Prop (lsuc l ⊔ l1 ⊔ l2) pr1 (is-small-map-Prop l f) = is-small-map l f pr2 (is-small-map-Prop l f) = is-prop-is-small-map l f
Recent changes
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).