Anodyne maps

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

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

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

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 _

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