Flattening lemma for pushouts (UniMath#764)

src/foundation/dependent-identifications.lagda.md

@@ -9,6 +9,7 @@ open import foundation-core.dependent-identifications public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
@@ -117,6 +118,13 @@ module _
     dependent-identification B q y' z' →
     dependent-identification B (p ∙ q) x' z'
   concat-dependent-identification refl q refl q' = q'
+
+  compute-concat-dependent-identification-refl :
+    { y z : A} (q : y ＝ z) →
+    { x' y' : B y} {z' : B z} (p' : x' ＝ y') →
+    ( q' : dependent-identification B q y' z') →
+    ( concat-dependent-identification refl q p' q') ＝ ap (tr B q) p' ∙ q'
+  compute-concat-dependent-identification-refl refl refl q' = refl
 ```
 
 #### Inverses of dependent identifications

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

@@ -109,6 +109,20 @@ module _
   pr1-pair-eq-Σ-ap refl = refl
 ```
 
+### Computing action of functions on identifications of the form `eq-pair-Σ p q`
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y)
+  where
+
+  ap-eq-pair-Σ :
+    { x y : A} (p : x ＝ y) {b : B x} {b' : B y} →
+    ( q : dependent-identification B p b b') →
+    ap f (eq-pair-Σ p q) ＝ (ap f (eq-pair-Σ p refl) ∙ ap (ev-pair f y) q)
+  ap-eq-pair-Σ refl refl = refl
+```
+
 ## See also
 
 - Equality proofs in cartesian product types are characterized in

src/foundation/equivalences.lagda.md

@@ -262,6 +262,24 @@ module _
     equiv-is-equiv-right-factor-htpy e (f ∘ map-equiv e) refl-htpy
 ```
 
+### Being an equivalence is closed under homotopies
+
+```agda
+module _
+  { l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  equiv-is-equiv-htpy :
+    { f g : A → B} → (f ~ g) →
+    is-equiv f ≃ is-equiv g
+  equiv-is-equiv-htpy {f} {g} H =
+    equiv-prop
+      ( is-property-is-equiv f)
+      ( is-property-is-equiv g)
+      ( is-equiv-htpy f (inv-htpy H))
+      ( is-equiv-htpy g H)
+```
+
 ### The groupoid laws for equivalences
 
 #### Composition of equivalences is associative

src/foundation/function-types.lagda.md

@@ -10,11 +10,16 @@ open import foundation-core.function-types public
 
 ```agda
 open import foundation.action-on-identifications-dependent-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.function-extensionality
+open import foundation.homotopies
+open import foundation.homotopy-induction
 open import foundation.universe-levels
 
+open import foundation-core.dependent-identifications
+open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
-open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.transport-along-identifications
 ```
@@ -50,8 +55,7 @@ module _
     map-equiv (compute-dependent-identification-function-type p f g)
 ```
 
-Relation between`compute-dependent-identification-function-type` and
-`preserves-tr`
+### Relation between `compute-dependent-identification-function-type` and `preserves-tr`
 
 ```agda
 module _
@@ -67,3 +71,79 @@ module _
     inv-htpy (preserves-tr f p) a
   preserves-tr-apd-function refl = refl-htpy
 ```
+
+### Computation of dependent identifications of functions over homotopies
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level}
+  { S : UU l1} {X : UU l2} {P : X → UU l3} (Y : UU l4)
+  { i : S → X}
+  where
+
+  equiv-htpy-dependent-fuction-dependent-identification-function-type :
+    { j : S → X} (H : i ~ j) →
+    ( k : (s : S) → P (i s) → Y)
+    ( l : (s : S) → P (j s) → Y) →
+    ( s : S) →
+    ( k s ~ (l s ∘ tr P (H s))) ≃
+    ( dependent-identification
+      ( λ x → P x → Y)
+      ( H s)
+      ( k s)
+      ( l s))
+  equiv-htpy-dependent-fuction-dependent-identification-function-type =
+    ind-htpy i
+      ( λ j H →
+        ( k : (s : S) → P (i s) → Y) →
+        ( l : (s : S) → P (j s) → Y) →
+        ( s : S) →
+        ( k s ~ (l s ∘ tr P (H s))) ≃
+        ( dependent-identification
+          ( λ x → P x → Y)
+          ( H s)
+          ( k s)
+          ( l s)))
+      ( λ k l s → inv-equiv (equiv-funext))
+
+  compute-equiv-htpy-dependent-fuction-dependent-identification-function-type :
+    { j : S → X} (H : i ~ j) →
+    ( h : (x : X) → P x → Y) →
+    ( s : S) →
+    ( map-equiv
+      ( equiv-htpy-dependent-fuction-dependent-identification-function-type H
+        ( h ∘ i)
+        ( h ∘ j)
+        ( s))
+      ( λ t → ap (ind-Σ h) (eq-pair-Σ (H s) refl))) ＝
+    ( apd h (H s))
+  compute-equiv-htpy-dependent-fuction-dependent-identification-function-type =
+    ind-htpy i
+      ( λ j H →
+        ( h : (x : X) → P x → Y) →
+        ( s : S) →
+        ( map-equiv
+          ( equiv-htpy-dependent-fuction-dependent-identification-function-type
+            ( H)
+            ( h ∘ i)
+            ( h ∘ j)
+            ( s))
+          ( λ t → ap (ind-Σ h) (eq-pair-Σ (H s) refl))) ＝
+        ( apd h (H s)))
+      ( λ h s →
+        ( ap
+          ( λ f → map-equiv (f (h ∘ i) (h ∘ i) s) refl-htpy)
+          ( compute-ind-htpy i
+            ( λ j H →
+              ( k : (s : S) → P (i s) → Y) →
+              ( l : (s : S) → P (j s) → Y) →
+              ( s : S) →
+              ( k s ~ (l s ∘ tr P (H s))) ≃
+              ( dependent-identification
+                ( λ x → P x → Y)
+                ( H s)
+                ( k s)
+                ( l s)))
+            ( λ k l s → inv-equiv (equiv-funext)))) ∙
+        ( eq-htpy-refl-htpy (h (i s))))
+```

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

@@ -127,6 +127,34 @@ id-map-equiv-Π :
 id-map-equiv-Π B h = eq-htpy (compute-map-equiv-Π B id-equiv (λ _ → id-equiv) h)
 ```
 
+### Two maps being homotopic is equivalent to them being homotopic after pre- or postcomposition by an equivalence
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  equiv-htpy-Π-precomp-htpy :
+    { B : UU l2} {C : B → UU l3} →
+    ( f g : (b : B) → C b) (e : A ≃ B) →
+    ( (f ∘ map-equiv e) ~ (g ∘ map-equiv e)) ≃
+    ( f ~ g)
+  equiv-htpy-Π-precomp-htpy f g e =
+    equiv-Π
+      ( eq-value f g)
+      ( e)
+      ( λ a → id-equiv)
+
+  equiv-htpy-Π-postcomp-htpy :
+    { B : A → UU l2} { C : UU l3} →
+    ( e : (a : A) → B a ≃ C) (f g : (a : A) → B a) →
+    ( f ~ g) ≃
+    ( (a : A) → ( map-equiv (e a) (f a) ＝ map-equiv (e a) (g a)))
+  equiv-htpy-Π-postcomp-htpy e f g =
+    equiv-Π-equiv-family
+      ( λ a → equiv-ap (e a) (f a) (g a))
+```
+
 ### Truncated families of maps induce truncated maps on dependent function types
 
 ```agda

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

@@ -19,6 +19,7 @@ open import foundation-core.constant-maps
 open import foundation-core.embeddings
 open import foundation-core.equivalences
 open import foundation-core.function-types
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositional-maps
 open import foundation-core.truncated-maps
@@ -60,6 +61,32 @@ module _
   pr2 equiv-function-type = is-equiv-map-equiv-function-type
 ```
 
+### Two maps being homotopic is equivalent to them being homotopic after pre- or postcomposition by an equivalence
+
+```agda
+module _
+  { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  where
+
+  equiv-htpy-precomp-htpy :
+    ( f g : B → C) (e : A ≃ B) →
+    ( (f ∘ map-equiv e) ~ (g ∘ map-equiv e)) ≃
+    ( f ~ g)
+  equiv-htpy-precomp-htpy f g e =
+    equiv-Π
+      ( eq-value f g)
+      ( e)
+      ( λ a → id-equiv)
+
+  equiv-htpy-postcomp-htpy :
+    ( e : B ≃ C) (f g : A → B) →
+    ( f ~ g) ≃
+    ( (map-equiv e ∘ f) ~ (map-equiv e ∘ g))
+  equiv-htpy-postcomp-htpy e f g =
+    equiv-Π-equiv-family
+      ( λ a → equiv-ap e (f a) (g a))
+```
+
 ### A map is truncated iff postcomposition by it is truncated
 
 ```agda

src/foundation/univalence.lagda.md

@@ -165,6 +165,11 @@ compute-eq-equiv-comp-equiv A B C f g =
             ( λ e → map-equiv e (g ∘e f))
             ( inv (right-inverse-law-equiv equiv-univalence))))))
 
+compute-equiv-eq-ap-inv :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A} (p : x ＝ y) →
+  map-equiv (equiv-eq (ap B (inv p)) ∘e (equiv-eq (ap B p))) ~ id
+compute-equiv-eq-ap-inv refl = refl-htpy
+
 commutativity-inv-equiv-eq :
   {l : Level} (A B : UU l) (p : A ＝ B) →
   inv-equiv (equiv-eq p) ＝ equiv-eq (inv p)

src/foundation/universal-property-dependent-pair-types.lagda.md

@@ -12,6 +12,7 @@ open import foundation.function-extensionality
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 ```
@@ -26,18 +27,64 @@ maps out of a dependent pair types.
 ## Theorem
 
 ```agda
-abstract
-  is-equiv-ev-pair :
-    {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} →
-    is-equiv (ev-pair {C = C})
-  pr1 (pr1 is-equiv-ev-pair) = ind-Σ
-  pr2 (pr1 is-equiv-ev-pair) = refl-htpy
-  pr1 (pr2 is-equiv-ev-pair) = ind-Σ
-  pr2 (pr2 is-equiv-ev-pair) f = eq-htpy (ind-Σ (λ x y → refl))
-
-equiv-ev-pair :
-  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} →
-  ((x : Σ A B) → C x) ≃ ((a : A) (b : B a) → C (pair a b))
-pr1 equiv-ev-pair = ev-pair
-pr2 equiv-ev-pair = is-equiv-ev-pair
+module _
+  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3}
+  where
+
+  abstract
+    is-equiv-ev-pair : is-equiv (ev-pair {C = C})
+    pr1 (pr1 is-equiv-ev-pair) = ind-Σ
+    pr2 (pr1 is-equiv-ev-pair) = refl-htpy
+    pr1 (pr2 is-equiv-ev-pair) = ind-Σ
+    pr2 (pr2 is-equiv-ev-pair) f = eq-htpy (ind-Σ (λ x y → refl))
+
+    is-equiv-ind-Σ : is-equiv (ind-Σ {C = C})
+    is-equiv-ind-Σ = is-equiv-is-section is-equiv-ev-pair refl-htpy
+
+  equiv-ev-pair : ((x : Σ A B) → C x) ≃ ((a : A) (b : B a) → C (pair a b))
+  pr1 equiv-ev-pair = ev-pair
+  pr2 equiv-ev-pair = is-equiv-ev-pair
+```
+
+## Properties
+
+### Iterated currying
+
+```agda
+equiv-ev-pair² :
+  { l1 l2 l3 l4 l5 l6 : Level}
+  { A : UU l1} {B : A → UU l2} {C : UU l3}
+  { X : UU l4} {Y : X → UU l5}
+  { Z : ( Σ A B → C) → Σ X Y → UU l6} →
+  Σ ( Σ A B → C)
+    ( λ k → ( xy : Σ X Y) → Z k xy) ≃
+  Σ ( (a : A) → B a → C)
+    ( λ k → (x : X) → (y : Y x) → Z (ind-Σ k) (x , y))
+equiv-ev-pair² {X = X} {Y = Y} {Z = Z} =
+  equiv-Σ
+    ( λ k → (x : X) (y : Y x) → Z (ind-Σ k) (x , y))
+    ( equiv-ev-pair)
+    ( λ k → equiv-ev-pair)
+
+equiv-ev-pair³ :
+  { l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} →
+  { A : UU l1} {B : A → UU l2} {C : UU l3}
+  { X : UU l4} {Y : X → UU l5} {Z : UU l6}
+  { U : UU l7} {V : U → UU l8}
+  { W : ((Σ A B) → C) → ((Σ X Y) → Z) → (Σ U V) → UU l9} →
+  Σ ( (Σ A B) → C)
+    ( λ k →
+      Σ ( (Σ X Y) → Z)
+        ( λ l → ( uv : Σ U V) → W k l uv)) ≃
+  Σ ( (a : A) → B a → C)
+    ( λ k →
+      Σ ( (x : X) → Y x → Z)
+        ( λ l → (u : U) → (v : V u) → W (ind-Σ k) (ind-Σ l) (u , v)))
+equiv-ev-pair³ {X = X} {Y = Y} {Z = Z} {U = U} {V = V} {W = W} =
+  equiv-Σ
+    ( λ k →
+      Σ ( (x : X) → Y x → Z)
+        ( λ l → (u : U) → (v : V u) → W (ind-Σ k) (ind-Σ l) (u , v)))
+    ( equiv-ev-pair)
+    ( λ k → equiv-ev-pair²)
 ```