Local maps

Content created by Egbert Rijke and Fredrik Bakke

Created on 2023-09-11.
Last modified on 2023-09-12.

module orthogonal-factorization-systems.local-maps where

Imports

open import foundation.fibers-of-maps
open import foundation.propositions
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-families

Idea

A map g : A → B is said to be local at f : Y → X, or f-local, if all its fibers are. Likewise, a family B : A → UU l is local at f if each B x is.

Definition

module _
  where

  is-local-map :
    {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
    {A : UU l3} {B : UU l4} → (A → B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-local-map f g = is-local-family f (fiber g)

Properties

Being local is a property

module _
  {l1 l2 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
  where

  is-property-is-local-map :
    {l3 l4 : Level} {A : UU l3} {B : UU l4}
    (g : A → B) → is-prop (is-local-map f g)
  is-property-is-local-map g = is-property-is-local-family f (fiber g)

  is-local-map-Prop :
    {l3 l4 : Level} {A : UU l3} {B : UU l4}
    (g : A → B) → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-local-map-Prop g = is-local-family-Prop f (fiber g)