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)

A type B is f-local if and only if the terminal projection B → unit is f-local

This remains to be formalized.

A map is f-local if and only if it is f-orthogonal

This remains to be formalized.

See also

Recent changes