Some results about path-cosplit maps

src/foundation-core/functoriality-dependent-function-types.lagda.md

@@ -22,6 +22,7 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
+open import foundation-core.retractions
 open import foundation-core.type-theoretic-principle-of-choice
 ```
 
@@ -34,7 +35,7 @@ open import foundation-core.type-theoretic-principle-of-choice
 ```agda
 htpy-map-Π :
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-  {f f' : (i : I) → A i → B i} (H : (i : I) → (f i) ~ (f' i)) →
+  {f f' : (i : I) → A i → B i} (H : (i : I) → f i ~ f' i) →
   map-Π f ~ map-Π f'
 htpy-map-Π H h = eq-htpy (λ i → H i (h i))
 
@@ -45,6 +46,32 @@ htpy-map-Π' :
 htpy-map-Π' α H = htpy-map-Π (H ∘ α)
 ```
 
+### The operation `map-Π` preserves composition
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {C : I → UU l4}
+  where
+
+  preserves-comp-map-Π :
+    (g : (i : I) → B i → C i)
+    (f : (i : I) → A i → B i) →
+    map-Π (λ i → g i ∘ f i) ~ map-Π g ∘ map-Π f
+  preserves-comp-map-Π g f = refl-htpy
+```
+
+### The operation `map-Π` preserves identity functions
+
+```agda
+module _
+  {l1 l2 : Level} {I : UU l1} {A : I → UU l2}
+  where
+
+  preserves-id-map-Π : map-Π (λ i → id {A = A i}) ~ id
+  preserves-id-map-Π = refl-htpy
+```
+
 ### The fibers of `map-Π`
 
 ```agda
@@ -65,48 +92,50 @@ compute-fiber-map-Π' α f = compute-fiber-map-Π (f ∘ α)
 ### Families of equivalences induce equivalences of dependent function types
 
 ```agda
-abstract
-  is-equiv-map-Π-is-fiberwise-equiv :
-    {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    {f : (i : I) → A i → B i} → is-fiberwise-equiv f →
-    is-equiv (map-Π f)
-  is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
-    is-equiv-is-contr-map
-      ( λ g →
-        is-contr-equiv' _
-          ( compute-fiber-map-Π _ g)
-          ( is-contr-Π (λ i → is-contr-map-is-equiv (is-equiv-f i) (g i))))
-
-equiv-Π-equiv-family :
+module _
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-  (e : (i : I) → A i ≃ B i) → ((i : I) → A i) ≃ ((i : I) → B i)
-pr1 (equiv-Π-equiv-family e) =
-  map-Π (λ i → map-equiv (e i))
-pr2 (equiv-Π-equiv-family e) =
-  is-equiv-map-Π-is-fiberwise-equiv (λ i → is-equiv-map-equiv (e i))
+  where
+
+  abstract
+    is-equiv-map-Π-is-fiberwise-equiv :
+      {f : (i : I) → A i → B i} → is-fiberwise-equiv f → is-equiv (map-Π f)
+    is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
+      is-equiv-is-contr-map
+        ( λ g →
+          is-contr-equiv' _
+            ( compute-fiber-map-Π _ g)
+            ( is-contr-Π (λ i → is-contr-map-is-equiv (is-equiv-f i) (g i))))
+
+  equiv-Π-equiv-family :
+    (e : (i : I) → A i ≃ B i) → ((i : I) → A i) ≃ ((i : I) → B i)
+  equiv-Π-equiv-family e =
+    ( map-Π (λ i → map-equiv (e i)) ,
+      is-equiv-map-Π-is-fiberwise-equiv (λ i → is-equiv-map-equiv (e i)))
 ```
 
 ### Families of equivalences induce equivalences of implicit dependent function types
 
 ```agda
-is-equiv-map-implicit-Π-is-fiberwise-equiv :
-    {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-    {f : (i : I) → A i → B i} → is-fiberwise-equiv f →
-    is-equiv (map-implicit-Π f)
-is-equiv-map-implicit-Π-is-fiberwise-equiv is-equiv-f =
-  is-equiv-comp _ _
-    ( is-equiv-explicit-implicit-Π)
-    ( is-equiv-comp _ _
-      ( is-equiv-map-Π-is-fiberwise-equiv is-equiv-f)
-      ( is-equiv-implicit-explicit-Π))
-
-equiv-implicit-Π-equiv-family :
+module _
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
-  (e : (i : I) → (A i) ≃ (B i)) → ({i : I} → A i) ≃ ({i : I} → B i)
-equiv-implicit-Π-equiv-family e =
-  ( equiv-implicit-explicit-Π) ∘e
-  ( equiv-Π-equiv-family e) ∘e
-  ( equiv-explicit-implicit-Π)
+  where
+
+  is-equiv-map-implicit-Π-is-fiberwise-equiv :
+      {f : (i : I) → A i → B i} → is-fiberwise-equiv f →
+      is-equiv (map-implicit-Π f)
+  is-equiv-map-implicit-Π-is-fiberwise-equiv is-equiv-f =
+    is-equiv-comp _ _
+      ( is-equiv-explicit-implicit-Π)
+      ( is-equiv-comp _ _
+        ( is-equiv-map-Π-is-fiberwise-equiv is-equiv-f)
+        ( is-equiv-implicit-explicit-Π))
+
+  equiv-implicit-Π-equiv-family :
+    (e : (i : I) → (A i) ≃ (B i)) → ({i : I} → A i) ≃ ({i : I} → B i)
+  equiv-implicit-Π-equiv-family e =
+    ( equiv-implicit-explicit-Π) ∘e
+    ( equiv-Π-equiv-family e) ∘e
+    ( equiv-explicit-implicit-Π)
 ```
 
 ##### Computing the inverse of `equiv-Π-equiv-family`
@@ -127,6 +156,22 @@ module _
         ( eq-htpy (λ x → inv (is-section-map-inv-equiv (e x) (f x)))))
 ```
 
+### Families of retracts induce retracts of dependent function types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
+  where
+
+  abstract
+    retraction-map-Π-fiberwise-retraction :
+      {f : (i : I) → A i → B i} →
+      ((i : I) → retraction (f i)) → retraction (map-Π f)
+    retraction-map-Π-fiberwise-retraction {f} r =
+      ( ( map-Π (λ i → map-retraction (f i) (r i))) ,
+        ( λ h → eq-htpy (λ i → is-retraction-map-retraction (f i) (r i) (h i))))
+```
+
 ## See also
 
 - Arithmetical laws involving dependent function types are recorded in

src/foundation-core/functoriality-dependent-pair-types.lagda.md

@@ -7,11 +7,13 @@ module foundation-core.functoriality-dependent-pair-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
+open import foundation-core.dependent-identifications
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
 open import foundation-core.families-of-equivalences
@@ -82,7 +84,7 @@ module _
 
   triangle-map-Σ :
     (f : A → B) (g : (x : A) → C x → D (f x)) →
-    (map-Σ f g) ~ (map-Σ-map-base f D ∘ tot g)
+    map-Σ f g ~ map-Σ-map-base f D ∘ tot g
   triangle-map-Σ f g t = refl
 ```
 
@@ -396,16 +398,16 @@ module _
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
-  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h))
+  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
   where
 
   fiber-triangle :
-    (x : X) → (fiber f x) → (fiber g x)
+    (x : X) → fiber f x → fiber g x
   pr1 (fiber-triangle .(f a) (pair a refl)) = h a
   pr2 (fiber-triangle .(f a) (pair a refl)) = inv (H a)
 
   square-tot-fiber-triangle :
-    ( h ∘ (map-equiv-total-fiber f)) ~
+    ( h ∘ map-equiv-total-fiber f) ~
     ( map-equiv-total-fiber g ∘ tot fiber-triangle)
   square-tot-fiber-triangle (pair .(f a) (pair a refl)) = refl
 ```
@@ -420,7 +422,7 @@ module _
 
   abstract
     is-fiberwise-equiv-is-equiv-triangle :
-      (E : is-equiv h) → is-fiberwise-equiv (fiber-triangle f g h H)
+      is-equiv h → is-fiberwise-equiv (fiber-triangle f g h H)
     is-fiberwise-equiv-is-equiv-triangle E =
       is-fiberwise-equiv-is-equiv-tot
         ( is-equiv-top-is-equiv-bottom-square
@@ -459,6 +461,38 @@ module _
   compute-map-Σ-id = refl-htpy
 ```
 
+### Computing the action on identifications of `tot`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {X : A → UU l2} {Y : A → UU l3}
+  (g : (a : A) → X a → Y a) {a a' : A} {x : X a} {x' : X a'}
+  where
+
+  compute-ap-tot :
+    pair-eq-Σ ∘ ap (tot g) {a , x} {a' , x'} ~
+    tot (λ p q → inv (preserves-tr g p x) ∙ ap (g a') q) ∘ pair-eq-Σ
+  compute-ap-tot refl = refl
+```
+
+### Computing the action on identifications of the functorial action of Σ
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : A → UU l3} (Y : B → UU l4)
+  (f : A → B) (g : (a : A) → X a → Y (f a)) {a a' : A} {x : X a} {x' : X a'}
+  where
+
+  compute-ap-map-Σ :
+    pair-eq-Σ ∘ ap (map-Σ Y f g) ~
+    map-Σ
+      ( λ p → dependent-identification Y p (g a x) (g a' x'))
+      ( ap f {a} {a'})
+      ( λ p q → tr-ap f g p x ∙ ap (g a') q) ∘
+    pair-eq-Σ
+  compute-ap-map-Σ refl = refl
+```
+
 ## See also
 
 - Arithmetical laws involving dependent pair types are recorded in

src/foundation-core/homotopies.lagda.md

@@ -309,6 +309,18 @@ inv-nat-htpy-id :
 inv-nat-htpy-id H p = inv (nat-htpy-id H p)
 ```
 
+### Conjugation by homotopies
+
+Given a homotopy `H : f ~ g` we obtain a natural map `f x ＝ f y → g x ＝ g y`
+given by conjugation by `H`.
+
+```agda
+conjugate-htpy :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B}
+  (H : f ~ g) {x y : A} → f x ＝ f y → g x ＝ g y
+conjugate-htpy H {x} {y} p = inv (H x) ∙ (p ∙ H y)
+```
+
 ### Homotopies preserve the laws of the action on identity types
 
 ```agda

src/foundation-core/retractions.lagda.md

@@ -110,6 +110,22 @@ module _
   pr2 retraction-ap = is-retraction-is-injective-retraction
 ```
 
+### Retractions of homotopic maps
+
+Given a homotopy `H : f ~ g`, then if `g` has a retraction so does `f`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  {f g : A → B}
+  where
+
+  retraction-htpy-map : f ~ g → retraction g → retraction f
+  retraction-htpy-map H G =
+    ( map-retraction g G ,
+      map-retraction g G ·l H ∙h is-retraction-map-retraction g G)
+```
+
 ### Composites of retractions are retractions
 
 ```agda
@@ -176,24 +192,33 @@ that would result in a cyclic module dependency.
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
-  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
+  (f : A → X) (g : B → X) (h : A → B) (H : g ∘ h ~ f)
   (r : retraction f)
   where
 
-  map-retraction-top-map-triangle : B → A
-  map-retraction-top-map-triangle = map-retraction f r ∘ g
+  map-retraction-top-map-triangle' : B → A
+  map-retraction-top-map-triangle' = map-retraction f r ∘ g
+
+  is-retraction-map-retraction-top-map-triangle' :
+    is-retraction h map-retraction-top-map-triangle'
+  is-retraction-map-retraction-top-map-triangle' =
+    (map-retraction f r ·l H) ∙h is-retraction-map-retraction f r
 
-  is-retraction-map-retraction-top-map-triangle :
-    is-retraction h map-retraction-top-map-triangle
-  is-retraction-map-retraction-top-map-triangle =
-    ( inv-htpy (map-retraction f r ·l H)) ∙h
-    ( is-retraction-map-retraction f r)
+  retraction-top-map-triangle' : retraction h
+  pr1 retraction-top-map-triangle' =
+    map-retraction-top-map-triangle'
+  pr2 retraction-top-map-triangle' =
+    is-retraction-map-retraction-top-map-triangle'
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
+  (r : retraction f)
+  where
 
   retraction-top-map-triangle : retraction h
-  pr1 retraction-top-map-triangle =
-    map-retraction-top-map-triangle
-  pr2 retraction-top-map-triangle =
-    is-retraction-map-retraction-top-map-triangle
+  retraction-top-map-triangle =
+    retraction-top-map-triangle' f g h (inv-htpy H) r
 ```
 
 ### In a commuting triangle `f ~ g ∘ h`, retractions of `g` and `h` compose to a retraction of `f`

src/foundation.lagda.md

@@ -190,6 +190,7 @@ open import foundation.full-subtypes public
 open import foundation.function-extensionality public
 open import foundation.function-types public
 open import foundation.functional-correspondences public
+open import foundation.functoriality-action-on-identifications-functions public
 open import foundation.functoriality-cartesian-product-types public
 open import foundation.functoriality-coproduct-types public
 open import foundation.functoriality-dependent-function-types public

src/foundation/equality-coproduct-types.lagda.md

@@ -236,7 +236,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (A : UU l1) (B : UU l2)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
   abstract
@@ -313,7 +313,7 @@ module _
       ( ap inl)
       ( ap-comp (rec-coproduct f g) inl)
       ( H a a')
-      ( is-emb-inl A B a a')
+      ( is-emb-inl a a')
   is-emb-coproduct H K L (inl a) (inr b') =
     is-equiv-is-empty (ap (rec-coproduct f g)) (L a b')
   is-emb-coproduct H K L (inr b) (inl a') =
@@ -325,7 +325,7 @@ module _
       ( ap inr)
       ( ap-comp (rec-coproduct f g) inr)
       ( K b b')
-      ( is-emb-inr A B b b')
+      ( is-emb-inr b b')
 ```
 
 ### Coproducts of `k+2`-truncated types are `k+2`-truncated