Maps in subuniverses

Content created by Fredrik Bakke.

Created on 2024-08-18.
Last modified on 2025-02-10.

module foundation.maps-in-subuniverses where
Imports 
open import foundation.homotopies
open import foundation.subuniverses
open import foundation.universe-levels

open import foundation-core.fibers-of-maps

Idea

Given a subuniverse 𝒫, a map f : A → B is said to be a map in 𝒫, or a 𝒫-map, if its fibers are in 𝒫.

Definitions

The predicate on maps of being in a subuniverse

is-in-subuniverse-map :
  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2} →
  (A → B) → UU (l2 ⊔ l3)
is-in-subuniverse-map P {A} {B} f = (b : B) → is-in-subuniverse P (fiber f b)

Properties

Subuniverses are closed under homotopies of maps

module _
  {l1 l2 l3 : Level} (P : subuniverse (l1 ⊔ l2) l3) {A : UU l1} {B : UU l2}
  {f g : A → B}
  where

  is-in-subuniverse-map-htpy :
    f ~ g → is-in-subuniverse-map P f → is-in-subuniverse-map P g
  is-in-subuniverse-map-htpy H F y =
    is-in-subuniverse-equiv' P (equiv-fiber-htpy H y) (F y)

See also

Recent changes