Refactor properties of lifts of families out of 26-descent (#988)

The file consisted of two sections: proof that the pullback property of
pushouts implies the dependent pullback property of pushouts (with some
infrastructure for lifts of families of elements), and characterization
of families over pushouts via descent data for pushouts.

This PR refactors the first part into more appropriate locations
throughout the library.

src/foundation/commuting-squares-of-maps.lagda.md

@@ -590,7 +590,7 @@ newly created rectangles, or by first horizontally composing the squares, and
 then vertically composing the rectangles.
 
 The following lemma states that the big squares obtained by these two
-compositions are again homotopic. Diagramatically, we have
+compositions are again homotopic. Diagrammatically, we have
 
 ```text
  H | K   H | K

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

@@ -11,6 +11,7 @@ open import foundation-core.functoriality-dependent-pair-types public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.cones-over-cospans
+open import foundation.dependent-homotopies
 open import foundation.dependent-pair-types
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
@@ -38,6 +39,101 @@ open import foundation-core.truncation-levels
 
 ## Properties
 
+### The map `htpy-map-Σ` preserves homotopies
+
+Given a [homotopy](foundation.homotopies.md) `H : f ~ f'` and a family of
+[dependent homotopies](foundation.dependent-homotopies.md) `K a : g a ~ g' a`
+over `H`, expressed as
+[commuting triangles](foundation.commuting-triangles-of-maps.md)
+
+```text
+        g a
+   C a -----> D (f a)
+      \      /
+  g' a \    / tr D (H a)
+        V  V
+      D (f' a)         ,
+```
+
+we get a homotopy `htpy-map-Σ H K : map-Σ f g ~ map-Σ f' g'`.
+
+This assignment itself preserves homotopies: given `H` and `K` as above,
+`H' : f ~ f'` with `K' a : g a ~ g' a` over `H'`, we would like to express
+coherences between the pairs `H, H'` and `K, K'` which would ensure
+`htpy-map-Σ H K ~ htpy-map-Σ H' K'`. Because `H` and `H'` have the same type, we
+may require a homotopy `α : H ~ H'`, but `K` and `K'` are families of dependent
+homotopies over different homotopies, so their coherence is provided as a family
+of
+[commuting triangles of identifications](foundation.commuting-triangles-of-identifications.md)
+
+```text
+                      ap (λ p → tr D p (g a c)) (α a)
+  tr D (H a) (g a c) --------------------------------- tr D (H' a) (g a c)
+                     \                               /
+                        \                         /
+                           \                   /
+                      K a c   \             /   K' a c
+                                 \       /
+                                    \ /
+                                  g' a c        .
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4)
+  {f f' : A → B} {H H' : f ~ f'}
+  {g : (a : A) → C a → D (f a)}
+  {g' : (a : A) → C a → D (f' a)}
+  {K : (a : A) → dependent-homotopy (λ _ → D) (λ _ → H a) (g a) (g' a)}
+  {K' : (a : A) → dependent-homotopy (λ _ → D) (λ _ → H' a) (g a) (g' a)}
+  where
+
+  abstract
+    htpy-htpy-map-Σ :
+      (α : H ~ H') →
+      (β :
+        (a : A) (c : C a) →
+        K a c ＝ ap (λ p → tr D p (g a c)) (α a) ∙ K' a c) →
+      htpy-map-Σ D H g K ~ htpy-map-Σ D H' g K'
+    htpy-htpy-map-Σ α β (a , c) =
+      ap
+        ( eq-pair-Σ')
+        ( eq-pair-Σ
+          ( α a)
+          ( map-compute-dependent-identification-eq-value-function
+            ( λ p → tr D p (g a c))
+            ( λ _ → g' a c)
+            ( α a)
+            ( K a c)
+            ( K' a c)
+            ( inv
+              ( ( ap
+                  ( K a c ∙_)
+                  ( ap-const (g' a c) (α a))) ∙
+                ( right-unit) ∙
+                ( β a c)))))
+```
+
+As a corollary of the above statement, we can provide a condition which
+guarantees that `htpy-map-Σ` is homotopic to the trivial homotopy.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4)
+  {f : A → B} {H : f ~ f}
+  {g : (a : A) → C a → D (f a)}
+  {K : (a : A) → tr D (H a) ∘ g a ~ g a}
+  where
+
+  abstract
+    htpy-htpy-map-Σ-refl-htpy :
+      (α : H ~ refl-htpy) →
+      (β : (a : A) (c : C a) → K a c ＝ ap (λ p → tr D p (g a c)) (α a)) →
+      htpy-map-Σ D H g K ~ refl-htpy
+    htpy-htpy-map-Σ-refl-htpy α β =
+      htpy-htpy-map-Σ D α (λ a c → β a c ∙ inv right-unit)
+```
+
 ### The map on total spaces induced by a family of truncated maps is truncated
 
 ```agda

src/foundation/precomposition-type-families.lagda.md

@@ -7,9 +7,14 @@ module foundation.precomposition-type-families where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.homotopy-induction
+open import foundation.transport-along-homotopies
 open import foundation.universe-levels
 
 open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.whiskering-homotopies
 ```
 
 </details>
@@ -35,6 +40,50 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  precomp-family : (l : Level) → (B → UU l) → (A → UU l)
-  precomp-family l Q = Q ∘ f
+  precomp-family : {l : Level} → (B → UU l) → (A → UU l)
+  precomp-family Q = Q ∘ f
+```
+
+## Properties
+
+### Transport along homotopies in precomposed type families
+
+[Transporting](foundation.transport-along-homotopies.md) along a
+[homotopy](foundation.homotopies.md) `H : g ~ h` in the family `Q ∘ f` gives us
+a map of families of elements
+
+```text
+  ((a : A) → Q (f (g a))) → ((a : A) → Q (f (h a))) .
+```
+
+We show that this map is homotopic to transporting along
+`f ·l H : f ∘ g ~ f ∘ h` in the family `Q`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A → B) (Q : B → UU l3)
+  {X : UU l4} {g : X → A}
+  where
+
+  statement-tr-htpy-precomp-family :
+    {h : X → A} (H : g ~ h) → UU (l3 ⊔ l4)
+  statement-tr-htpy-precomp-family H =
+    tr-htpy (λ _ → precomp-family f Q) H ~ tr-htpy (λ _ → Q) (f ·l H)
+
+  abstract
+    tr-htpy-precomp-family :
+      {h : X → A} (H : g ~ h) →
+      statement-tr-htpy-precomp-family H
+    tr-htpy-precomp-family =
+      ind-htpy g
+        ( λ h → statement-tr-htpy-precomp-family)
+        ( refl-htpy)
+
+    compute-tr-htpy-precomp-family :
+      tr-htpy-precomp-family refl-htpy ＝
+      refl-htpy
+    compute-tr-htpy-precomp-family =
+      compute-ind-htpy g
+        ( λ h → statement-tr-htpy-precomp-family)
+        ( refl-htpy)
 ```

src/foundation/type-theoretic-principle-of-choice.lagda.md

@@ -37,6 +37,10 @@ In this file we record some further facts about the
 [structures](foundation.structure.md) introduced in
 [`foundation-core.type-theoretic-principle-of-choice`](foundation-core.type-theoretic-principle-of-choice.md).
 
+We relate precomposition of maps into a dependent pair type by a function with
+precomposition in dependent pair types of functions in the file
+[`orthogonal-factorization-systems.precomposition-lifts-families-of-elements`](orthogonal-factorization-systems.precomposition-lifts-families-of-elements.md).
+
 ## Lemma
 
 ### Characterizing the identity type of `universally-structured-Π`

src/foundation/whiskering-homotopies.lagda.md

@@ -115,7 +115,7 @@ may be whiskered by a homotopy `L` on the left or right, which results in a
 commuting square of homotopies with `L` appended or prepended to the two ways of
 going around the square.
 
-Diagramatically, we may turn the pasting diagram
+Diagrammatically, we may turn the pasting diagram
 
 ```text
         H

src/orthogonal-factorization-systems.lagda.md

@@ -46,6 +46,7 @@ open import orthogonal-factorization-systems.null-types public
 open import orthogonal-factorization-systems.open-modalities public
 open import orthogonal-factorization-systems.orthogonal-factorization-systems public
 open import orthogonal-factorization-systems.orthogonal-maps public
+open import orthogonal-factorization-systems.precomposition-lifts-families-of-elements public
 open import orthogonal-factorization-systems.pullback-hom public
 open import orthogonal-factorization-systems.raise-modalities public
 open import orthogonal-factorization-systems.reflective-modalities public

src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md

@@ -7,6 +7,15 @@ module orthogonal-factorization-systems.lifts-families-of-elements where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.precomposition-functions
+open import foundation.precomposition-type-families
+open import foundation.transport-along-homotopies
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
@@ -38,6 +47,42 @@ elements `a` is a family of elements
   (i : I) → B (a i).
 ```
 
+A family of elements equipped with a dependent lift is a
+{{#concept "dependent lifted family of elements"}}, and analogously a family of
+elements equipped with a lift is a {{#concept "lifted family of elements"}}.
+
+To see how these families relate to
+[lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md), consider the
+lifting diagram
+
+```text
+      Σ (x : A) (B x)
+            |
+            | pr1
+            |
+            v
+  I ------> A         .
+       a
+```
+
+Then a lift of the map `a` against `pr1` is a map `b : I → Σ A B`, such that the
+triangle commutes. Invoking the
+[type theoretic principle of choice](foundation.type-theoretic-principle-of-choice.md),
+we can show that this type is equivalent to the type of families of elements
+`(i : I) → B (a i)`:
+
+```text
+  Σ (b : I → Σ A B) ((i : I) → a i ＝ pr1 (b i))
+    ≃ (i : I) → Σ ((x , b) : Σ A B) (a i ＝ x)
+    ≃ (i : I) → Σ (x : A) (a i ＝ x × B x)
+    ≃ (i : I) → B (a i) .
+```
+
+The first equivalence is the principle of choice, the second is associativity of
+dependent pair types, and the third is the left unit law of dependent pair
+types, since `Σ (x : A) (a i ＝ x)` is
+[contractible](foundation.contractible-types.md).
+
 ## Definitions
 
 ### Dependent lifts of families of elements
@@ -63,6 +108,31 @@ module _
   lift-family-of-elements = dependent-lift-family-of-elements (λ _ → B) a
 ```
 
+### Dependent lifted families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} {I : UU l1} (A : I → UU l2) (B : (i : I) → A i → UU l3)
+  where
+
+  dependent-lifted-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
+  dependent-lifted-family-of-elements =
+    Σ ( (i : I) → A i)
+      ( dependent-lift-family-of-elements B)
+```
+
+### Lifted families of elements
+
+```agda
+module _
+  {l1 l2 l3 : Level} (I : UU l1) {A : UU l2} (B : A → UU l3)
+  where
+
+  lifted-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
+  lifted-family-of-elements =
+    dependent-lifted-family-of-elements (λ (_ : I) → A) (λ _ → B)
+```
+
 ### Dependent lifts of binary families of elements
 
 ```agda
@@ -89,6 +159,58 @@ module _
     dependent-lift-binary-family-of-elements (λ _ → C) a
 ```
 
+## Properties
+
+### Transport in lifts of families of elements along homotopies of precompositions
+
+Given a map `a : I → A`, and a homotopy `H : f ~ g`, where `f, g : J → I`, we
+know that there is an identification `a ∘ f ＝ a ∘ g`. Transporting along this
+identification in the type of lifts of families of elements into a type family
+`B : A → 𝓤`, we get a map
+
+```text
+  ((j : J) → B (a (f j))) → ((j : J) → B (a (g j))) .
+```
+
+We show that this map is homotopic to transporting along `H` in the type family
+`B ∘ a : I → 𝓤`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) (a : I → A)
+  {J : UU l4} {f : J → I}
+  where
+
+  statement-tr-lift-family-of-elements-precomp :
+    {g : J → I} (H : f ~ g) → UU (l3 ⊔ l4)
+  statement-tr-lift-family-of-elements-precomp H =
+    tr (lift-family-of-elements B) (htpy-precomp H A a) ~
+    tr-htpy (λ _ → precomp-family a B) H
+
+  tr-lift-family-of-elements-precomp-refl-htpy :
+    statement-tr-lift-family-of-elements-precomp refl-htpy
+  tr-lift-family-of-elements-precomp-refl-htpy b =
+    ap
+      ( λ p → tr (lift-family-of-elements B) p b)
+      ( compute-htpy-precomp-refl-htpy f A a)
+
+  abstract
+    tr-lift-family-of-elements-precomp :
+      {g : J → I} (H : f ~ g) → statement-tr-lift-family-of-elements-precomp H
+    tr-lift-family-of-elements-precomp =
+      ind-htpy f
+        ( λ g → statement-tr-lift-family-of-elements-precomp)
+        ( tr-lift-family-of-elements-precomp-refl-htpy)
+
+    compute-tr-lift-family-of-elements-precomp :
+      tr-lift-family-of-elements-precomp refl-htpy ＝
+      tr-lift-family-of-elements-precomp-refl-htpy
+    compute-tr-lift-family-of-elements-precomp =
+      compute-ind-htpy f
+        ( λ g → statement-tr-lift-family-of-elements-precomp)
+        ( tr-lift-family-of-elements-precomp-refl-htpy)
+```
+
 ## See also
 
 - [Double lifts of families of elements](orthogonal-factorization-systems.double-lifts-families-of-elements.md)