Zigzag construction of identity types of pushouts

Makefile

@@ -14,7 +14,9 @@ else
 	AGDA_MIN_HEAP ?= 4G
 endif
 
-AGDARTS := +RTS -H$(AGDA_MIN_HEAP) -M6G -RTS
+# Temporarily raise maximum heap size; should compile with the previous 6G
+# before merging
+AGDARTS := +RTS -H$(AGDA_MIN_HEAP) -M14G -RTS
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)
 CONTRIBUTORS_FILE := CONTRIBUTORS.toml
 

src/foundation-core/families-of-equivalences.lagda.md

@@ -84,6 +84,24 @@ module _
   is-equiv-map-fam-equiv x = is-equiv-map-equiv (e x)
 ```
 
+### Inverses of families of equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} {Q : A → UU l3}
+  (e : fam-equiv P Q)
+  where
+
+  inv-fam-equiv : fam-equiv Q P
+  inv-fam-equiv a = inv-equiv (e a)
+
+  map-inv-fam-equiv : (a : A) → Q a → P a
+  map-inv-fam-equiv = map-fam-equiv inv-fam-equiv
+
+  is-equiv-map-inv-fam-equiv : is-fiberwise-equiv map-inv-fam-equiv
+  is-equiv-map-inv-fam-equiv = is-equiv-map-fam-equiv inv-fam-equiv
+```
+
 ## Properties
 
 ### Families of equivalences are equivalent to fiberwise equivalences

src/foundation-core/transport-along-identifications.lagda.md

@@ -68,6 +68,15 @@ module _
     preserves-tr p x ＝
     inv (tr-ap id f p x) ∙ ap (λ q → tr B q (f i x)) (ap-id p)
   compute-preserves-tr refl x = refl
+
+module _
+  {l1 l2 : Level} {I : UU l1} {A : I → UU l2}
+  where
+
+  compute-preserves-tr-id :
+    {i j : I} (p : i ＝ j) (x : A i) →
+    preserves-tr (λ i → id {A = A i}) p x ＝ refl
+  compute-preserves-tr-id refl x = refl
 ```
 
 ### Substitution law for transport

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

@@ -13,7 +13,11 @@ open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-triangles-of-homotopies
 open import foundation.commuting-triangles-of-maps
+open import foundation.dependent-pair-types
+open import foundation.embeddings
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-function-types
+open import foundation.homotopies
 open import foundation.homotopy-algebra
 open import foundation.postcomposition-functions
 open import foundation.precomposition-functions
@@ -27,7 +31,6 @@ open import foundation-core.commuting-squares-of-homotopies
 open import foundation-core.commuting-squares-of-identifications
 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.whiskering-identifications-concatenation
 ```
@@ -597,6 +600,58 @@ module _
             ( sq-right-top ·r top-left))))
 ```
 
+### Vertical pasting of a square with the right leg an equivalence is an equivalence
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
+  (top : A → X) (top-left : A → B) (top-right : X → Y) (mid : B → Y)
+  (bottom-left : B → C) (bottom-right : Y → Z) (bottom : C → Z)
+  (K : coherence-square-maps mid bottom-left bottom-right bottom)
+  (is-emb-bottom-right : is-emb bottom-right)
+  where
+
+  is-equiv-pasting-vertical-coherence-square-maps :
+    is-equiv
+      ( λ H →
+        pasting-vertical-coherence-square-maps
+          ( top)
+          ( top-left)
+          ( top-right)
+          ( mid)
+          ( bottom-left)
+          ( bottom-right)
+          ( bottom)
+          ( H)
+          ( K))
+  is-equiv-pasting-vertical-coherence-square-maps =
+    is-equiv-comp _ _
+      ( is-equiv-map-Π-is-fiberwise-equiv (λ _ → is-emb-bottom-right _ _))
+      ( is-equiv-concat-htpy (K ·r top-left) _)
+
+  equiv-pasting-vertical-coherence-square-maps :
+    coherence-square-maps top top-left top-right mid ≃
+    coherence-square-maps
+      ( top)
+      ( bottom-left ∘ top-left)
+      ( bottom-right ∘ top-right)
+      ( bottom)
+  pr1 equiv-pasting-vertical-coherence-square-maps H =
+    pasting-vertical-coherence-square-maps
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( mid)
+      ( bottom-left)
+      ( bottom-right)
+      ( bottom)
+      ( H)
+      ( K)
+  pr2 equiv-pasting-vertical-coherence-square-maps =
+    is-equiv-pasting-vertical-coherence-square-maps
+```
+
 ### Distributivity of pasting squares and transposing by precomposition
 
 Given two commuting squares which can be composed horizontally (vertically), we

src/foundation/dependent-identifications.lagda.md

@@ -116,14 +116,22 @@ module _
     dependent-identification B p x' y' →
     dependent-identification B q y' z' →
     dependent-identification B (p ∙ q) x' z'
-  concat-dependent-identification refl q refl q' = q'
+  concat-dependent-identification refl q p' q' = ap (tr B q) p' ∙ q'
 
   compute-concat-dependent-identification-left-base-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-left-base-refl q refl q' = refl
+  compute-concat-dependent-identification-left-base-refl q p' q' = refl
+
+  compute-concat-dependent-identification :
+    {x y z : A} (p : x ＝ y) (q : y ＝ z) →
+    {x' : B x} {y' : B y} {z' : B z} →
+    (p' : dependent-identification B p x' y') →
+    (q' : dependent-identification B q y' z') →
+    concat-dependent-identification p q p' q' ＝ tr-concat p q x' ∙ ap (tr B q) p' ∙ q'
+  compute-concat-dependent-identification refl q p' q' = refl
 ```
 
 #### Strictly right unital concatenation of dependent identifications

src/foundation/families-of-equivalences.lagda.md

@@ -9,10 +9,13 @@ open import foundation-core.families-of-equivalences public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.equality-dependent-function-types
 open import foundation.equivalences
+open import foundation.univalence
 open import foundation.universe-levels
 
 open import foundation-core.propositions
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
@@ -28,6 +31,19 @@ A **family of equivalences** is a family
 of [equivalences](foundation-core.equivalences.md). Families of equivalences are
 also called **fiberwise equivalences**.
 
+## Definitions
+
+### The family of identity equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  id-fam-equiv : fam-equiv B B
+  id-fam-equiv a = id-equiv
+```
+
 ## Properties
 
 ### Being a fiberwise equivalence is a proposition
@@ -43,6 +59,22 @@ module _
     is-prop-Π (λ a → is-property-is-equiv (f a))
 ```
 
+### TODO
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  is-torsorial-fam-equiv : is-torsorial (fam-equiv B)
+  is-torsorial-fam-equiv =
+    is-torsorial-Eq-Π (λ a → is-torsorial-equiv (B a))
+
+  is-torsorial-fam-equiv' : is-torsorial (λ C → fam-equiv C B)
+  is-torsorial-fam-equiv' =
+    is-torsorial-Eq-Π (λ a → is-torsorial-equiv' (B a))
+```
+
 ## See also
 
 - In

src/foundation/fiberwise-equivalence-induction.lagda.md

@@ -0,0 +1,119 @@
+# Fiberwise equivalence induction
+
+```agda
+module foundation.fiberwise-equivalence-induction where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.families-of-equivalences
+open import foundation.identity-systems
+open import foundation.identity-types
+-- open import foundation.subuniverses
+-- open import foundation.univalence
+-- open import foundation.universal-property-identity-systems
+open import foundation.universe-levels
+
+-- open import foundation-core.commuting-triangles-of-maps
+-- open import foundation-core.contractible-maps
+-- open import foundation-core.function-types
+-- open import foundation-core.postcomposition-functions
+-- open import foundation-core.sections
+-- open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+## Definitions
+
+### Evaluation at the family of identity equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2}
+  (R : (Q : A → UU l2) → fam-equiv P Q → UU l3)
+  where
+
+  ev-id-fam-equiv :
+    ((Q : A → UU l2) → (e : fam-equiv P Q) → R Q e) →
+    R P id-fam-equiv
+  ev-id-fam-equiv r = r P id-fam-equiv
+```
+
+### The induction principle of families of equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : A → UU l2)
+  where
+
+  induction-principle-fam-equiv : UUω
+  induction-principle-fam-equiv =
+    is-identity-system (λ (Q : A → UU l2) → fam-equiv P Q) P id-fam-equiv
+
+  induction-principle-fam-equiv' : UUω
+  induction-principle-fam-equiv' =
+    is-identity-system (λ (Q : A → UU l2) → fam-equiv Q P) P id-fam-equiv
+```
+
+## Theorems
+
+### Induction on families of equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {P : A → UU l2}
+  where
+
+  abstract
+    is-identity-system-fam-equiv : induction-principle-fam-equiv P
+    is-identity-system-fam-equiv =
+      is-identity-system-is-torsorial P
+        ( id-fam-equiv)
+        ( is-torsorial-fam-equiv)
+
+    is-identity-system-fam-equiv' : induction-principle-fam-equiv' P
+    is-identity-system-fam-equiv' =
+      is-identity-system-is-torsorial P
+        ( id-fam-equiv)
+        ( is-torsorial-fam-equiv')
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2}
+  (R : (Q : A → UU l2) → fam-equiv P Q → UU l3)
+  (r : R P id-fam-equiv)
+  where
+
+  abstract
+    ind-fam-equiv :
+      {Q : A → UU l2} (e : fam-equiv P Q) → R Q e
+    ind-fam-equiv {Q = Q} e =
+      pr1 (is-identity-system-fam-equiv R) r Q e
+
+    compute-ind-fam-equiv :
+      ind-fam-equiv id-fam-equiv ＝ r
+    compute-ind-fam-equiv =
+      pr2 (is-identity-system-fam-equiv R) r
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2}
+  (R : (Q : A → UU l2) → fam-equiv Q P → UU l3)
+  (r : R P id-fam-equiv)
+  where
+
+  abstract
+    ind-fam-equiv' :
+      {Q : A → UU l2} (e : fam-equiv Q P) → R Q e
+    ind-fam-equiv' {Q = Q} e =
+      pr1 (is-identity-system-fam-equiv' R) r Q e
+
+    compute-ind-fam-equiv' :
+      ind-fam-equiv' id-fam-equiv ＝ r
+    compute-ind-fam-equiv' =
+      pr2 (is-identity-system-fam-equiv' R) r
+```

src/foundation/transposition-identifications-along-equivalences.lagda.md

@@ -127,6 +127,11 @@ module _
     {a : A} {b : B} → map-inv-equiv e b ＝ a → b ＝ map-equiv e a
   map-inv-eq-transpose-equiv-inv {a} {b} =
     map-inv-equiv (eq-transpose-equiv-inv a b)
+
+  map-eq-transpose-equiv-inv' :
+    {a : A} {b : B} → b ＝ map-equiv e a → map-inv-equiv e b ＝ a
+  map-eq-transpose-equiv-inv' {a} {b} p =
+    ap (map-inv-equiv e) p ∙ is-retraction-map-inv-equiv e a
 ```
 
 ## Properties
@@ -155,6 +160,12 @@ module _
       ( equiv-ap e _ _)
       ( ( right-unit) ∙
         ( coherence-map-inv-equiv e _))
+
+  compute-refl-eq-transpose-equiv-inv' :
+    {x : A} →
+    map-eq-transpose-equiv-inv' e refl ＝ is-retraction-map-inv-equiv e x
+  compute-refl-eq-transpose-equiv-inv' =
+    refl
 ```
 
 ### The two definitions of transposing identifications along equivalences are homotopic

src/synthetic-homotopy-theory.lagda.md

@@ -51,6 +51,7 @@ 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-function-types-over-sequential-colimits 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
@@ -72,6 +73,7 @@ open import synthetic-homotopy-theory.flattening-lemma-sequential-colimits publi
 open import synthetic-homotopy-theory.free-loops public
 open import synthetic-homotopy-theory.functoriality-loop-spaces public
 open import synthetic-homotopy-theory.functoriality-sequential-colimits public
+open import synthetic-homotopy-theory.functoriality-stuff public
 open import synthetic-homotopy-theory.functoriality-suspensions public
 open import synthetic-homotopy-theory.groups-of-loops-in-1-types public
 open import synthetic-homotopy-theory.hatchers-acyclic-type public
@@ -120,6 +122,7 @@ open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
 open import synthetic-homotopy-theory.sphere-prespectrum public
 open import synthetic-homotopy-theory.spheres public
+open import synthetic-homotopy-theory.stuff-over public
 open import synthetic-homotopy-theory.suspension-prespectra public
 open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
@@ -139,5 +142,6 @@ open import synthetic-homotopy-theory.universal-property-sequential-colimits pub
 open import synthetic-homotopy-theory.universal-property-suspensions public
 open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.wedges-of-pointed-types public
+open import synthetic-homotopy-theory.zigzag-construction-identity-type-pushouts public
 open import synthetic-homotopy-theory.zigzags-sequential-diagrams public
 ```