Weakly anodyne maps

Content created by Fredrik Bakke.

Created on 2025-07-15.
Last modified on 2025-07-15.

module orthogonal-factorization-systems.weakly-anodyne-maps where
Imports 
open import foundation.equivalences-arrows
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.retracts-of-maps
open import foundation.unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.anodyne-maps
open import orthogonal-factorization-systems.maps-local-at-maps
open import orthogonal-factorization-systems.orthogonal-maps
open import orthogonal-factorization-systems.types-local-at-maps

open import synthetic-homotopy-theory.cocartesian-morphisms-arrows

Idea

A map is said to be weakly anodyne with respect to a map , or weakly -anodyne, if every map that is local at is also local at .

Definitions

The predicate of being weakly anodyne with respect to a map

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) (j : C → D)
  where

  is-weakly-anodyne-map-Level :
    (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
  is-weakly-anodyne-map-Level l5 l6 =
    {X : UU l5} {Y : UU l6} (g : X → Y) → is-local-map f g → is-local-map j g

  is-weakly-anodyne-map : UUω
  is-weakly-anodyne-map = {l5 l6 : Level} → is-weakly-anodyne-map-Level l5 l6

Properties

Anodyne maps are weakly anodyne

module _
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  (f : A → B) {j : C → D}
  where

  is-weakly-anodyne-map-is-anodyne-map :
    is-anodyne-map f j → is-weakly-anodyne-map f j
  is-weakly-anodyne-map-is-anodyne-map J g G x =
    is-local-is-orthogonal-terminal-map j
      ( J ( terminal-map (fiber g x))
          ( is-orthogonal-terminal-map-is-local f (G x)))

Weakly anodyne maps are closed under retracts of maps

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6}
  (f : A → B) {j : C → D} {j' : C' → D'}
  where

  is-weakly-anodyne-map-retract-map :
    retract-map j j' → is-weakly-anodyne-map f j → is-weakly-anodyne-map f j'
  is-weakly-anodyne-map-retract-map α J g G x =
    is-local-retract-map-is-local j' j α (fiber g x) (J g G x)

Recent changes