diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md
index 23e82b5948..de15f1eb08 100644
--- a/src/foundation/equivalences-arrows.lagda.md
+++ b/src/foundation/equivalences-arrows.lagda.md
@@ -87,8 +87,7 @@ module _
     coherence-hom-arrow f g (map-equiv i) (map-equiv j)
 
   equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  equiv-arrow =
-    Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
+  equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
 
   module _
     (e : equiv-arrow)
@@ -100,6 +99,9 @@ module _
     map-domain-equiv-arrow : A → X
     map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow
 
+    map-inv-domain-equiv-arrow : X → A
+    map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow
+
     is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow
     is-equiv-map-domain-equiv-arrow =
       is-equiv-map-equiv equiv-domain-equiv-arrow
@@ -110,6 +112,9 @@ module _
     map-codomain-equiv-arrow : B → Y
     map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow
 
+    map-inv-codomain-equiv-arrow : Y → B
+    map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow
+
     is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow
     is-equiv-map-codomain-equiv-arrow =
       is-equiv-map-equiv equiv-codomain-equiv-arrow
diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md
index b80513a416..7abfa99887 100644
--- a/src/foundation/morphisms-arrows.lagda.md
+++ b/src/foundation/morphisms-arrows.lagda.md
@@ -10,6 +10,8 @@ module foundation.morphisms-arrows where
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
+open import foundation.postcomposition-functions
+open import foundation.precomposition-functions
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -19,8 +21,6 @@ open import foundation-core.functoriality-dependent-function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.postcomposition-functions
-open import foundation-core.precomposition-functions
 ```
 
 </details>
@@ -309,19 +309,25 @@ A morphism of arrows `α : f → g` gives a morphism of precomposition arrows
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level}
+  {l1 l2 l3 l4 l : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → B) (g : X → Y) (α : hom-arrow f g)
+  (S : UU l)
   where
 
-  precomp-hom-arrow :
-    {l : Level} (S : UU l) → hom-arrow (precomp g S) (precomp f S)
-  pr1 (precomp-hom-arrow S) =
-    precomp (map-codomain-hom-arrow f g α) S
-  pr1 (pr2 (precomp-hom-arrow S)) =
-    precomp (map-domain-hom-arrow f g α) S
-  pr2 (pr2 (precomp-hom-arrow S)) h =
-    inv (eq-htpy (h ·l coh-hom-arrow f g α))
+  transpose-precomp-hom-arrow :
+    hom-arrow
+      ( precomp (map-codomain-hom-arrow f g α) S)
+      ( precomp (map-domain-hom-arrow f g α) S)
+  transpose-precomp-hom-arrow =
+    ( precomp g S , precomp f S , htpy-precomp (coh-hom-arrow f g α) S)
+
+  precomp-hom-arrow : hom-arrow (precomp g S) (precomp f S)
+  precomp-hom-arrow =
+    transpose-hom-arrow
+      ( precomp (map-codomain-hom-arrow f g α) S)
+      ( precomp (map-domain-hom-arrow f g α) S)
+      ( transpose-precomp-hom-arrow)
 ```
 
 ### Morphisms of arrows give morphisms of postcomposition arrows
@@ -338,12 +344,10 @@ module _
 
   postcomp-hom-arrow :
     {l : Level} (S : UU l) → hom-arrow (postcomp S f) (postcomp S g)
-  pr1 (postcomp-hom-arrow S) =
-    postcomp S (map-domain-hom-arrow f g α)
-  pr1 (pr2 (postcomp-hom-arrow S)) =
-    postcomp S (map-codomain-hom-arrow f g α)
-  pr2 (pr2 (postcomp-hom-arrow S)) h =
-    eq-htpy (coh-hom-arrow f g α ·r h)
+  postcomp-hom-arrow S =
+    ( postcomp S (map-domain-hom-arrow f g α) ,
+      postcomp S (map-codomain-hom-arrow f g α) ,
+      htpy-postcomp S (coh-hom-arrow f g α))
 ```
 
 ## See also
diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md
index b24c28bb74..f2f61bf6b5 100644
--- a/src/foundation/postcomposition-pullbacks.lagda.md
+++ b/src/foundation/postcomposition-pullbacks.lagda.md
@@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.postcomposition-functions
 open import foundation.standard-pullbacks
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
@@ -21,7 +22,6 @@ open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
-open import foundation-core.postcomposition-functions
 open import foundation-core.pullbacks
 open import foundation-core.universal-property-pullbacks
 ```
@@ -68,9 +68,10 @@ postcomp-cone :
   {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5)
   (f : A → X) (g : B → X) (c : cone f g C) →
   cone (postcomp T f) (postcomp T g) (T → C)
-pr1 (postcomp-cone T f g c) h = vertical-map-cone f g c ∘ h
-pr1 (pr2 (postcomp-cone T f g c)) h = horizontal-map-cone f g c ∘ h
-pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h)
+postcomp-cone T f g c =
+  ( postcomp T (vertical-map-cone f g c) ,
+    postcomp T (horizontal-map-cone f g c) ,
+    htpy-postcomp T (coherence-square-cone f g c))
 ```
 
 ## Properties
@@ -121,38 +122,33 @@ triangle-map-standard-pullback-postcomp T f g c h =
 ### Pullbacks are closed under postcomposition exponentiation
 
 ```agda
-abstract
-  is-pullback-postcomp-is-pullback :
-    {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-    (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c →
-    (T : UU l5) →
-    is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
-  is-pullback-postcomp-is-pullback f g c is-pb-c T =
-    is-equiv-top-map-triangle
-      ( cone-map f g c)
-      ( map-standard-pullback-postcomp f g T)
-      ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-      ( triangle-map-standard-pullback-postcomp T f g c)
-      ( is-equiv-map-standard-pullback-postcomp f g T)
-      ( universal-property-pullback-is-pullback f g c is-pb-c T)
-
-abstract
-  is-pullback-is-pullback-postcomp :
-    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-    (f : A → X) (g : B → X) (c : cone f g C) →
-    ( {l5 : Level} (T : UU l5) →
-      is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) →
-    is-pullback f g c
-  is-pullback-is-pullback-postcomp f g c is-pb-postcomp =
-    is-pullback-universal-property-pullback f g c
-      ( λ T →
-        is-equiv-left-map-triangle
-          ( cone-map f g c)
-          ( map-standard-pullback-postcomp f g T)
-          ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-          ( triangle-map-standard-pullback-postcomp T f g c)
-          ( is-pb-postcomp T)
-          ( is-equiv-map-standard-pullback-postcomp f g T))
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  abstract
+    is-pullback-postcomp-is-pullback :
+      is-pullback f g c → {l5 : Level} (T : UU l5) →
+      is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
+    is-pullback-postcomp-is-pullback is-pb-c T =
+      is-equiv-top-map-triangle _ _ _
+        ( triangle-map-standard-pullback-postcomp T f g c)
+        ( is-equiv-map-standard-pullback-postcomp f g T)
+        ( universal-property-pullback-is-pullback f g c is-pb-c T)
+
+  abstract
+    is-pullback-is-pullback-postcomp :
+      ( {l5 : Level} (T : UU l5) →
+        is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) →
+      is-pullback f g c
+    is-pullback-is-pullback-postcomp is-pb-postcomp =
+      is-pullback-universal-property-pullback f g c
+        ( λ T →
+          is-equiv-left-map-triangle _ _ _
+            ( triangle-map-standard-pullback-postcomp T f g c)
+            ( is-pb-postcomp T)
+            ( is-equiv-map-standard-pullback-postcomp f g T))
 ```
 
 ### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation
diff --git a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
index 09335074fa..73a755edc1 100644
--- a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
+++ b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md
@@ -243,7 +243,9 @@ module _
 
 ### Unit laws for standard pullbacks
 
-Pulling back along the identity map
+Pulling back along the identity map is the identity operation.
+
+#### Left unit law for standard pullbacks
 
 ```agda
 module _
@@ -302,7 +304,7 @@ module _
 
 ### Unit laws for standard pullbacks
 
-Pulling back along the identity map is the identity operation.
+#### Right unit law for standard pullbacks
 
 ```agda
 module _
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
index a167d57d4a..e2a8bf7286 100644
--- a/src/orthogonal-factorization-systems.lagda.md
+++ b/src/orthogonal-factorization-systems.lagda.md
@@ -9,6 +9,7 @@
 ```agda
 module orthogonal-factorization-systems where
 
+open import orthogonal-factorization-systems.anodyne-maps public
 open import orthogonal-factorization-systems.cd-structures public
 open import orthogonal-factorization-systems.cellular-maps public
 open import orthogonal-factorization-systems.closed-modalities public
@@ -71,6 +72,7 @@ open import orthogonal-factorization-systems.types-local-at-maps public
 open import orthogonal-factorization-systems.types-separated-at-maps public
 open import orthogonal-factorization-systems.uniquely-eliminating-modalities public
 open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public
+open import orthogonal-factorization-systems.weakly-anodyne-maps public
 open import orthogonal-factorization-systems.wide-function-classes public
 open import orthogonal-factorization-systems.wide-global-function-classes public
 open import orthogonal-factorization-systems.zero-modality public
diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
new file mode 100644
index 0000000000..8f86a1c09d
--- /dev/null
+++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md
@@ -0,0 +1,179 @@
+# Anodyne maps
+
+```agda
+module orthogonal-factorization-systems.anodyne-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.equivalences-arrows
+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.universe-levels
+
+open import orthogonal-factorization-systems.orthogonal-maps
+
+open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
+```
+
+</details>
+
+## Idea
+
+A map $j : C → D$ is said to be
+{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne-map}} with
+respect to a map $f : A → B$, or **$f$-anodyne**, if every map that is
+[orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to $f$ is also
+orthogonal to $j$.
+
+## Definitions
+
+### The predicate of being anodyne with respect to a map
+
+```agda
+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-anodyne-map-Level :
+    (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  is-anodyne-map-Level l5 l6 =
+    {X : UU l5} {Y : UU l6} (g : X → Y) → is-orthogonal f g → is-orthogonal j g
+
+  is-anodyne-map : UUω
+  is-anodyne-map = {l5 l6 : Level} → is-anodyne-map-Level l5 l6
+```
+
+## Properties
+
+### Anodyne maps are closed under homotopies
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) {j i : C → D}
+  where
+
+  is-anodyne-map-htpy : j ~ i → is-anodyne-map f j → is-anodyne-map f i
+  is-anodyne-map-htpy K J g H = is-orthogonal-htpy-left j g K (J g H)
+```
+
+### Anodyne maps are closed under equivalences of maps
+
+```agda
+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-anodyne-map-equiv-arrow :
+    equiv-arrow j j' → is-anodyne-map f j → is-anodyne-map f j'
+  is-anodyne-map-equiv-arrow α J g H =
+    is-orthogonal-left-equiv-arrow α g (J g H)
+```
+
+### Anodyne maps are closed under retracts of maps
+
+> This remains to be formalized.
+
+### Anodyne maps compose
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5}
+  (f : A → B) (j : C → D) (i : D → E)
+  where
+
+  is-anodyne-map-comp :
+    is-anodyne-map f j → is-anodyne-map f i → is-anodyne-map f (i ∘ j)
+  is-anodyne-map-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H)
+```
+
+### Cancellation property for anodyne maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5}
+  (f : A → B) (j : C → D) (i : D → E)
+  where
+
+  is-anodyne-map-left-factor :
+    is-anodyne-map f j → is-anodyne-map f (i ∘ j) → is-anodyne-map f i
+  is-anodyne-map-left-factor J IJ g H =
+    is-orthogonal-left-left-factor j i g (J g H) (IJ g H)
+```
+
+### Anodyne maps are closed under dependent sums
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {I : UU l3} {C : I → UU l4} {D : I → UU l5}
+  (f : A → B) (j : (i : I) → C i → D i)
+  where
+
+  is-anodyne-map-tot :
+    ((i : I) → is-anodyne-map f (j i)) → is-anodyne-map f (tot j)
+  is-anodyne-map-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H)
+```
+
+### Anodyne maps are closed under products
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-map-map-product :
+    is-anodyne-map f j → is-anodyne-map f i → is-anodyne-map f (map-product j i)
+  is-anodyne-map-map-product J I g H =
+    is-orthogonal-left-product j i g (J g H) (I g H)
+```
+
+### Anodyne maps are closed under coproducts
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-map-map-coproduct :
+    is-anodyne-map f j →
+    is-anodyne-map f i →
+    is-anodyne-map f (map-coproduct j i)
+  is-anodyne-map-map-coproduct J I g H =
+    is-orthogonal-left-coproduct j i g (J g H) (I g H)
+```
+
+### Anodyne maps are closed under cobase change
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  (f : A → B) (j : C → D) (i : E → F)
+  where
+
+  is-anodyne-map-cobase-change :
+    cocartesian-hom-arrow j i → is-anodyne-map f j → is-anodyne-map f i
+  is-anodyne-map-cobase-change α J g H =
+    is-orthogonal-left-cobase-change j i g α (J g H)
+```
+
+### Anodyne maps are closed under pushout-products
+
+> This remains to be formalized.
diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
index ac69503101..921e0c45d7 100644
--- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md
@@ -147,6 +147,19 @@ module _
       ( G (map-codomain-inclusion-retract-map g' g R d))
 ```
 
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6}
+  {f : A → B} {g : C → D} {f' : E → F}
+  where
+
+  is-local-retract-map' :
+    is-local-map f g → f' retract-of-map f → is-local-map f' g
+  is-local-retract-map' F R d =
+    is-local-retract-map-is-local f' f R (fiber g d) (F d)
+```
+
 ## See also
 
 - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md)
diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
index a5b845c065..beee150e80 100644
--- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -29,6 +29,7 @@ open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies
+open import foundation.identity-types
 open import foundation.morphisms-arrows
 open import foundation.postcomposition-functions
 open import foundation.postcomposition-pullbacks
@@ -37,6 +38,7 @@ open import foundation.precomposition-functions
 open import foundation.products-pullbacks
 open import foundation.propositions
 open import foundation.pullbacks
+open import foundation.type-arithmetic-cartesian-product-types
 open import foundation.type-arithmetic-dependent-function-types
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
@@ -51,6 +53,10 @@ open import foundation.whiskering-homotopies-composition
 open import orthogonal-factorization-systems.lifting-structures-on-squares
 open import orthogonal-factorization-systems.pullback-hom
 open import orthogonal-factorization-systems.types-local-at-maps
+
+open import synthetic-homotopy-theory.cocartesian-morphisms-arrows
+open import synthetic-homotopy-theory.pullback-property-pushouts
+open import synthetic-homotopy-theory.pushouts
 ```
 
 </details>
@@ -426,19 +432,40 @@ module _
         ( ( commutative-htpy-postcomp-htpy-precomp F G) ∙h
           ( inv-htpy-right-unit-htpy)))
 
-  is-orthogonal-pullback-condition-htpy-left :
-    {f' : A → B} → f ~ f' →
-    is-orthogonal-pullback-condition f g →
-    is-orthogonal-pullback-condition f' g
-  is-orthogonal-pullback-condition-htpy-left F =
-    is-orthogonal-pullback-condition-htpy F refl-htpy
-
-  is-orthogonal-pullback-condition-htpy-right :
-    {g' : X → Y} → g ~ g' →
-    is-orthogonal-pullback-condition f g →
-    is-orthogonal-pullback-condition f g'
-  is-orthogonal-pullback-condition-htpy-right =
-    is-orthogonal-pullback-condition-htpy refl-htpy
+  abstract
+    is-orthogonal-pullback-condition-htpy-left :
+      {f' : A → B} → f ~ f' →
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f' g
+    is-orthogonal-pullback-condition-htpy-left F =
+      is-orthogonal-pullback-condition-htpy F refl-htpy
+
+  abstract
+    is-orthogonal-pullback-condition-htpy-right :
+      {g' : X → Y} → g ~ g' →
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f g'
+    is-orthogonal-pullback-condition-htpy-right =
+      is-orthogonal-pullback-condition-htpy refl-htpy
+
+  abstract
+    is-orthogonal-htpy :
+      {f' : A → B} {g' : X → Y} → f ~ f' → g ~ g' →
+      is-orthogonal f g → is-orthogonal f' g'
+    is-orthogonal-htpy {f'} {g'} F G H =
+      is-orthogonal-is-orthogonal-pullback-condition f' g'
+        ( is-orthogonal-pullback-condition-htpy F G
+          ( is-orthogonal-pullback-condition-is-orthogonal f g H))
+
+  abstract
+    is-orthogonal-htpy-left :
+      {f' : A → B} → f ~ f' → is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-htpy-left F = is-orthogonal-htpy F refl-htpy
+
+  abstract
+    is-orthogonal-htpy-right :
+      {g' : X → Y} → g ~ g' → is-orthogonal f g → is-orthogonal f g'
+    is-orthogonal-htpy-right = is-orthogonal-htpy refl-htpy
 ```
 
 ### Equivalences are orthogonal to every map
@@ -698,6 +725,70 @@ module _
         ( is-orthogonal-pullback-condition-is-orthogonal (h ∘ f) g HF))
 ```
 
+### Orthogonality is preserved by equivalences of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6}
+  {f : A → B} {f' : A' → B'}
+  where
+
+  abstract
+    is-orthogonal-left-equiv-arrow :
+      equiv-arrow f f' → (g : X → Y) → is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-left-equiv-arrow α g F =
+      is-orthogonal-htpy-left
+        ( map-codomain-equiv-arrow f f' α ∘
+          f ∘
+          map-inv-domain-equiv-arrow f f' α)
+        ( g)
+        ( ( coh-equiv-arrow f f' α ·r map-inv-domain-equiv-arrow f f' α) ∙h
+          ( f' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow f f' α)))
+        ( is-orthogonal-left-comp
+          ( f ∘ map-inv-domain-equiv-arrow f f' α)
+          ( map-codomain-equiv-arrow f f' α)
+          ( g)
+          ( is-orthogonal-left-comp
+            ( map-inv-domain-equiv-arrow f f' α)
+            ( f)
+            ( g)
+            ( is-orthogonal-equiv-left (equiv-domain-inv-equiv-arrow f f' α) g)
+            ( F))
+          ( is-orthogonal-equiv-left (equiv-codomain-equiv-arrow f f' α) g))
+
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6}
+  (f : A → B) {g : X → Y} {g' : X' → Y'}
+  where
+
+  abstract
+    is-orthogonal-right-equiv-arrow :
+      equiv-arrow g g' → is-orthogonal f g → is-orthogonal f g'
+    is-orthogonal-right-equiv-arrow α G =
+      is-orthogonal-htpy-right
+        ( f)
+        ( map-codomain-equiv-arrow g g' α ∘
+          g ∘
+          map-inv-domain-equiv-arrow g g' α)
+        ( ( coh-equiv-arrow g g' α ·r map-inv-domain-equiv-arrow g g' α) ∙h
+          ( g' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow g g' α)))
+        ( is-orthogonal-right-comp
+          ( f)
+          ( g ∘ map-inv-domain-equiv-arrow g g' α)
+          ( map-codomain-equiv-arrow g g' α)
+          ( is-orthogonal-equiv-right f (equiv-codomain-equiv-arrow g g' α))
+          ( is-orthogonal-right-comp
+            ( f)
+            ( map-inv-domain-equiv-arrow g g' α)
+            ( g)
+            ( G)
+            ( is-orthogonal-equiv-right
+              ( f)
+              ( equiv-domain-inv-equiv-arrow g g' α))))
+```
+
 ### Right orthogonality is preserved by dependent products
 
 If `f ⊥ gᵢ`, for each `i : I`, then `f ⊥ (map-Π g)`.
@@ -912,10 +1003,10 @@ module _
   (f : (i : I) → A i → B i) (g : X → Y)
   where
 
-  is-orthogonal-pullback-condition-left-Σ :
+  is-orthogonal-pullback-condition-left-tot :
     ((i : I) → is-orthogonal-pullback-condition (f i) g) →
     is-orthogonal-pullback-condition (tot f) g
-  is-orthogonal-pullback-condition-left-Σ F =
+  is-orthogonal-pullback-condition-left-tot F =
     is-pullback-top-is-pullback-bottom-cube-is-equiv
       ( map-Π (λ i → postcomp (B i) g))
       ( map-Π (λ i → precomp (f i) X))
@@ -951,14 +1042,56 @@ module _
         ( λ i → cone-pullback-hom (f i) g)
         ( F))
 
-  is-orthogonal-left-Σ :
+  is-orthogonal-left-tot :
     ((i : I) → is-orthogonal (f i) g) → is-orthogonal (tot f) g
-  is-orthogonal-left-Σ F =
+  is-orthogonal-left-tot F =
     is-orthogonal-is-orthogonal-pullback-condition (tot f) g
-      ( is-orthogonal-pullback-condition-left-Σ
+      ( is-orthogonal-pullback-condition-left-tot
         ( λ i → is-orthogonal-pullback-condition-is-orthogonal (f i) g (F i)))
 ```
 
+### Left orthogonality is preserved by products
+
+If `f ⊥ g` and `f' ⊥ g`, then `(f × f') ⊥ g`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
+  where
+
+  is-orthogonal-left-map-right-product :
+    {l5 : Level} (C : UU l5) →
+    is-orthogonal f g → is-orthogonal (map-product (id' C) f) g
+  is-orthogonal-left-map-right-product C F =
+    is-orthogonal-left-tot (λ _ → f) g (λ _ → F)
+
+  is-orthogonal-left-map-left-product :
+    {l5 : Level} (C : UU l5) →
+    is-orthogonal f g → is-orthogonal (map-product f (id' C)) g
+  is-orthogonal-left-map-left-product C F =
+    is-orthogonal-left-equiv-arrow
+      ( commutative-product , commutative-product , refl-htpy)
+      ( g)
+      ( is-orthogonal-left-map-right-product C F)
+
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6}
+  (f : A → B) (f' : A' → B') (g : X → Y)
+  where
+
+  is-orthogonal-left-product :
+    is-orthogonal f g → is-orthogonal f' g → is-orthogonal (map-product f f') g
+  is-orthogonal-left-product F F' =
+    is-orthogonal-left-comp
+      ( map-product f id)
+      ( map-product id f')
+      ( g)
+      ( is-orthogonal-left-map-left-product f g A' F)
+      ( is-orthogonal-left-map-right-product f' g B F')
+```
+
 ### Left orthogonality is preserved by coproducts
 
 If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`.
@@ -966,7 +1099,7 @@ If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`.
 **Proof:** We need to show that the square
 
 ```text
-                     - ∘ (f + f')
+                   - ∘ (f + f')
   ((B + B') → X) ---------------> ((A + A') → X)
         |                               |
         |                               |
@@ -1114,6 +1247,94 @@ module _
         ( is-orthogonal-pullback-condition-is-orthogonal f g G))
 ```
 
+### Left orthogonality is preserved under cobase change
+
+Given a pushout square
+
+```text
+    A ------> A'
+    |         |
+  f'|         | f'
+    ∨       ⌜ ∨
+    B ------> B',
+```
+
+if `f ⊥ g`, then `f' ⊥ g`.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {A' : UU l5} {B' : UU l6}
+  (f : A → B) (f' : A' → B') (g : X → Y) (α : cocartesian-hom-arrow f f')
+  where
+
+  abstract
+    is-orthogonal-pullback-condition-left-cobase-change :
+      is-orthogonal-pullback-condition f g →
+      is-orthogonal-pullback-condition f' g
+    is-orthogonal-pullback-condition-left-cobase-change F =
+      is-pullback-swap-cone
+        ( postcomp A' g)
+        ( precomp f' Y)
+        ( precomp f' X , postcomp B' g , refl-htpy)
+        ( is-pullback-back-left-is-pullback-back-right-cube
+          ( refl-htpy)
+          ( refl-htpy)
+          ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))
+          ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) Y))
+          ( refl-htpy)
+          ( refl-htpy)
+          ( right-unit-htpy ∙h
+            ( inv ·l
+              commutative-postcomp-htpy-precomp g
+                ( coh-cocartesian-hom-arrow f f' α)) ∙h
+            ( inv-htpy
+              ( left-whisker-inv-htpy
+                ( postcomp A g)
+                ( htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))) ∙h
+            ( inv-htpy-right-unit-htpy))
+          ( is-pullback-swap-cone
+            ( precomp f Y)
+            ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y)
+            ( cone-hom-arrow
+              ( precomp (map-codomain-cocartesian-hom-arrow f f' α) Y)
+              ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y)
+              ( transpose-precomp-hom-arrow f f'
+                ( hom-arrow-cocartesian-hom-arrow f f' α)
+                ( Y)))
+            ( pullback-property-pushout-is-pushout
+              ( f)
+              ( map-domain-cocartesian-hom-arrow f f' α)
+              ( cocone-cocartesian-hom-arrow f f' α)
+              ( is-cocartesian-cocartesian-hom-arrow f f' α)
+              ( Y)))
+          ( is-pullback-swap-cone
+            ( precomp f Y)
+            ( postcomp A g)
+            ( cone-pullback-hom f g)
+            ( F))
+          ( is-pullback-swap-cone
+            ( precomp f X)
+            ( precomp (map-domain-cocartesian-hom-arrow f f' α) X)
+            ( cone-hom-arrow
+              ( precomp (map-codomain-cocartesian-hom-arrow f f' α) X)
+              ( precomp (map-domain-cocartesian-hom-arrow f f' α) X)
+              ( transpose-precomp-hom-arrow f f'
+                ( hom-arrow-cocartesian-hom-arrow f f' α)
+                ( X)))
+            ( pullback-property-pushout-is-pushout f
+              ( map-domain-cocartesian-hom-arrow f f' α)
+              ( cocone-cocartesian-hom-arrow f f' α)
+              ( is-cocartesian-cocartesian-hom-arrow f f' α) X)))
+
+    is-orthogonal-left-cobase-change :
+      is-orthogonal f g → is-orthogonal f' g
+    is-orthogonal-left-cobase-change F =
+      is-orthogonal-is-orthogonal-pullback-condition f' g
+        ( is-orthogonal-pullback-condition-left-cobase-change
+          ( is-orthogonal-pullback-condition-is-orthogonal f g F))
+```
+
 ### A type is `f`-local if and only if its terminal map is `f`-orthogonal
 
 **Proof (forward direction):** If the terminal map is right orthogonal to `f`,
diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
new file mode 100644
index 0000000000..a2a1cdbe49
--- /dev/null
+++ b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md
@@ -0,0 +1,90 @@
+# Weakly anodyne maps
+
+```agda
+module orthogonal-factorization-systems.weakly-anodyne-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+A map $j : C → D$ is said to be
+{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne-map}}
+with respect to a map $f : A → B$, or **weakly $f$-anodyne**, if every map that
+is local at $f$ is also local at $j$.
+
+## Definitions
+
+### The predicate of being weakly anodyne with respect to a map
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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)
+```
diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
index 9e34713e9c..634145c719 100644
--- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
+++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md
@@ -7,13 +7,17 @@ module synthetic-homotopy-theory.cocartesian-morphisms-arrows where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.cartesian-morphisms-arrows
 open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
 open import foundation.morphisms-arrows
+open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.pullbacks
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.pullback-property-pushouts
 open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
@@ -121,6 +125,47 @@ module _
       ( is-cocartesian-cocartesian-hom-arrow)
 ```
 
+### The cartesian morphism on precomposition maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (α : cocartesian-hom-arrow f g) (S : UU l)
+  where
+
+  precomp-cocartesian-hom-arrow : hom-arrow (precomp g S) (precomp f S)
+  precomp-cocartesian-hom-arrow =
+    precomp-hom-arrow f g (hom-arrow-cocartesian-hom-arrow f g α) S
+
+  abstract
+    is-cartesian-precomp-cocartesian-hom-arrow :
+      is-cartesian-hom-arrow
+        ( precomp g S)
+        ( precomp f S)
+        ( precomp-cocartesian-hom-arrow)
+    is-cartesian-precomp-cocartesian-hom-arrow =
+      is-pullback-swap-cone
+        ( precomp f S)
+        ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
+        ( cone-hom-arrow
+          ( precomp (map-codomain-cocartesian-hom-arrow f g α) S)
+          ( precomp (map-domain-cocartesian-hom-arrow f g α) S)
+          ( transpose-precomp-hom-arrow f g
+            ( hom-arrow-cocartesian-hom-arrow f g α)
+            ( S)))
+        ( pullback-property-pushout-is-pushout
+          ( f)
+          ( map-domain-cocartesian-hom-arrow f g α)
+          ( cocone-cocartesian-hom-arrow f g α)
+          ( is-cocartesian-cocartesian-hom-arrow f g α) S)
+
+  precomp-cartesian-hom-arrow-cocartesian-hom-arrow :
+    cartesian-hom-arrow (precomp g S) (precomp f S)
+  precomp-cartesian-hom-arrow-cocartesian-hom-arrow =
+    ( precomp-cocartesian-hom-arrow ,
+      is-cartesian-precomp-cocartesian-hom-arrow)
+```
+
 ## See also
 
 - [Cartesian morphisms of arrows](foundation.cartesian-morphisms-arrows.md) for
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 8c280f7233..5242c08e65 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -33,6 +33,7 @@ open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.induction-principle-pushouts
+open import synthetic-homotopy-theory.pullback-property-pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -459,6 +460,29 @@ module _
       ( up-pushout f g)
 ```
 
+### Pushout cocones satisfy the pullback property of the pushout
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
+  where
+
+  abstract
+    pullback-property-pushout-is-pushout :
+      is-pushout f g c → pullback-property-pushout f g c
+    pullback-property-pushout-is-pushout po =
+      pullback-property-pushout-universal-property-pushout f g c
+        ( universal-property-pushout-is-pushout f g c po)
+
+  abstract
+    is-pushout-pullback-property-pushout :
+      pullback-property-pushout f g c → is-pushout f g c
+    is-pushout-pullback-property-pushout pb =
+      is-pushout-universal-property-pushout f g c
+        ( universal-property-pushout-pullback-property-pushout f g c pb)
+```
+
 ### Fibers of the cogap map
 
 We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map