Maps in subuniverses

Content created by Fredrik Bakke.

Created on 2024-08-18.
Last modified on 2024-08-18.

module foundation.maps-in-subuniverses where
Imports 
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)

See also

Recent changes