Maps in global subuniverses

Content created by Fredrik Bakke.

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

module foundation.maps-in-global-subuniverses where
Imports 
open import foundation.cartesian-morphisms-arrows
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.functoriality-fibers-of-maps
open import foundation.global-subuniverses
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.propositions

Idea

Given a global 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 global subuniverse

module _
  {α : Level → Level} (𝒫 : global-subuniverse α)
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  is-in-global-subuniverse-map : UU (α (l1 ⊔ l2) ⊔ l2)
  is-in-global-subuniverse-map =
    (b : B) → is-in-global-subuniverse 𝒫 (fiber f b)

  is-prop-is-in-global-subuniverse-map : is-prop is-in-global-subuniverse-map
  is-prop-is-in-global-subuniverse-map =
    is-prop-Π (λ b → is-prop-is-in-global-subuniverse 𝒫 (fiber f b))

  is-in-global-subuniverse-map-Prop : Prop (α (l1 ⊔ l2) ⊔ l2)
  is-in-global-subuniverse-map-Prop =
    ( is-in-global-subuniverse-map , is-prop-is-in-global-subuniverse-map)

Properties

A type is in 𝒫 if and only if its terminal projection is in 𝒫

module _
  {α : Level → Level} (𝒫 : global-subuniverse α)
  {l1 : Level} {A : UU l1}
  where

  is-in-global-subuniverse-is-in-global-subuniverse-terminal-map :
    is-in-global-subuniverse-map 𝒫 (terminal-map A) →
    is-in-global-subuniverse 𝒫 A
  is-in-global-subuniverse-is-in-global-subuniverse-terminal-map H =
    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
      ( fiber (terminal-map A) star)
      ( A)
      ( equiv-fiber-terminal-map star)
      ( H star)

  is-in-global-subuniverse-terminal-map-is-in-global-subuniverse :
    is-in-global-subuniverse 𝒫 A →
    is-in-global-subuniverse-map 𝒫 (terminal-map A)
  is-in-global-subuniverse-terminal-map-is-in-global-subuniverse H u =
    is-closed-under-equiv-global-subuniverse 𝒫 l1 l1
      ( A)
      ( fiber (terminal-map A) u)
      ( inv-equiv-fiber-terminal-map u)
      ( H)

Closure under base change

Maps in 𝒫 are closed under base change.

module _
  {α : Level → Level} (𝒫 : global-subuniverse α)
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (g : C → D)
  where

  is-in-global-subuniverse-map-base-change :
    is-in-global-subuniverse-map 𝒫 f →
    cartesian-hom-arrow g f →
    is-in-global-subuniverse-map 𝒫 g
  is-in-global-subuniverse-map-base-change F α d =
    is-closed-under-equiv-global-subuniverse 𝒫 (l1 ⊔ l2) (l3 ⊔ l4)
      ( fiber f (map-codomain-cartesian-hom-arrow g f α d))
      ( fiber g d)
      ( inv-equiv (equiv-fibers-cartesian-hom-arrow g f α d))
      ( F (map-codomain-cartesian-hom-arrow g f α d))

Recent changes