Characterization of various families over pushouts (#1148)

This PR characterizes (as in "provides the expected descent data and
shows equivalence") the following type families over pushouts:
- families of function types, `x ↦ P x → Q x`
- families of equivalence types, `x ↦ P x ≃ Q x`
- families of based identity types at `x₀ : X`, `x ↦ x₀ = x`

It also introduces sections of descent data, which correspond to
sections of the associated type family

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

@@ -56,20 +56,26 @@ module _
   (left : A → X) (right : B → X) (e : A ≃ B)
   where
 
+  equiv-coherence-triangle-maps-inv-top' :
+    coherence-triangle-maps left right (map-equiv e) ≃
+    coherence-triangle-maps' right left (map-inv-equiv e)
+  equiv-coherence-triangle-maps-inv-top' =
+    equiv-Π
+      ( λ b → left (map-inv-equiv e b) ＝ right b)
+      ( e)
+      ( λ a →
+        equiv-concat
+          ( ap left (is-retraction-map-inv-equiv e a))
+          ( right (map-equiv e a)))
+
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
     coherence-triangle-maps right left (map-inv-equiv e)
   equiv-coherence-triangle-maps-inv-top =
     ( equiv-inv-htpy
       ( left ∘ (map-inv-equiv e))
       ( right)) ∘e
-    ( equiv-Π
-      ( λ b → left (map-inv-equiv e b) ＝ right b)
-      ( e)
-      ( λ a →
-        equiv-concat
-          ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a))))
+    ( equiv-coherence-triangle-maps-inv-top')
 
   coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) →

src/foundation/equivalences.lagda.md

@@ -16,6 +16,7 @@ open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
 open import foundation.transposition-identifications-along-equivalences
 open import foundation.truncated-maps
 open import foundation.universal-property-equivalences
@@ -572,6 +573,19 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
 pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
 ```
 
+### Computing transport in the type of equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  tr-equiv-type :
+    {x y : A} (p : x ＝ y) (e : B x ≃ C x) →
+    tr (λ x → B x ≃ C x) p e ＝ equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
+  tr-equiv-type refl e = eq-htpy-equiv refl-htpy
+```
+
 ### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence
 
 ```agda

src/synthetic-homotopy-theory.lagda.md

@@ -47,6 +47,9 @@ open import synthetic-homotopy-theory.descent-circle-dependent-pair-types public
 open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 open import synthetic-homotopy-theory.descent-circle-function-types public
 open import synthetic-homotopy-theory.descent-circle-subtypes public
+open import synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts public
+open import synthetic-homotopy-theory.descent-data-function-types-over-pushouts public
+open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts public
 open import synthetic-homotopy-theory.descent-data-pushouts public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.descent-property-pushouts public
@@ -103,6 +106,7 @@ open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
+open import synthetic-homotopy-theory.sections-descent-data-pushouts public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
 open import synthetic-homotopy-theory.sequentially-compact-types public

src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md

@@ -27,6 +27,7 @@ open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.retractions
 open import foundation.sections
+open import foundation.span-diagrams
 open import foundation.structure-identity-principle
 open import foundation.torsorial-type-families
 open import foundation.transport-along-higher-identifications
@@ -104,6 +105,13 @@ module _
         ( horizontal-map-dependent-cocone (f s))
         ( vertical-map-dependent-cocone (g s))
     coherence-square-dependent-cocone = pr2 (pr2 d)
+
+dependent-cocone-span-diagram :
+  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
+  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
+  UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
+dependent-cocone-span-diagram {𝒮 = 𝒮} =
+  dependent-cocone (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮)
 ```
 
 ### Cocones equipped with dependent cocones
@@ -188,6 +196,13 @@ pr1 (pr2 (dependent-cocone-map f g c P h)) b =
   h (vertical-map-cocone f g c b)
 pr2 (pr2 (dependent-cocone-map f g c P h)) s =
   apd h (coherence-square-cocone f g c s)
+
+dependent-cocone-map-span-diagram :
+  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
+  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
+  ( (x : X) → P x) → dependent-cocone-span-diagram c P
+dependent-cocone-map-span-diagram {𝒮 = 𝒮} c =
+  dependent-cocone-map (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) c
 ```
 
 ## Properties