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