Identity systems of descent data for pushouts (#1150)

This PR replaces the (unfinished, non-dependent) universal property of
identity types of pushouts with the induction principle, expressed as
the property of being an identity system.

I show that the canonical descent data for identity types is an identity
system, and that identity systems are uniquely unique.

references.bib

@@ -263,6 +263,22 @@ @article{KECA17
   eprintclass = {cs}
 }
 
+@inproceedings{KvR19,
+  title       =  {{Path Spaces of Higher Inductive Types in Homotopy Type Theory}},
+  booktitle   =  {Proceedings of the 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
+  author      =  {Kraus, Nicolai and von Raumer, Jakob},
+  year        =  {2019},
+  publisher   =  {IEEE Press},
+  abstract    =  {The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.},
+  articleno   =  {7},
+  numpages    =  {13},
+  location    =  {Vancouver, Canada},
+  series      =  {LICS '19},
+  eprint      =  {1901.06022},
+  eprinttype  =  {arxiv},
+  eprintclass =  {cs, math},
+}
+
 @book{May12,
   title      = {More {{Concise Algebraic Topology}}: {{Localization}}, {{Completion}}, and {{Model Categories}}},
   shorttitle = {More {{Concise Algebraic Topology}}},

src/foundation/universal-property-identity-types.lagda.md

@@ -21,15 +21,17 @@ open import foundation.preunivalence
 open import foundation.univalence
 open import foundation.universe-levels
 
+open import foundation-core.contractible-maps
 open import foundation-core.contractible-types
+open import foundation-core.families-of-equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
 open import foundation-core.injective-maps
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.torsorial-type-families
-open import foundation-core.type-theoretic-principle-of-choice
 ```
 
 </details>
@@ -86,6 +88,29 @@ is-equiv-ev-refl' :
 is-equiv-ev-refl' a = is-equiv-map-equiv (equiv-ev-refl' a)
 ```
 
+### The type of fiberwise maps from `Id a` to a torsorial type family `B` is equivalent to the type of fiberwise equivalences
+
+Note that the type of fiberwise equivalences is a
+[subtype](foundation-core.subtypes.md) of the type of fiberwise maps. By the
+[fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md),
+it is a [full subtype](foundation.full-subtypes.md), hence it is equivalent to
+the whole type of fiberwise maps.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (a : A) {B : A → UU l2}
+  (is-torsorial-B : is-torsorial B)
+  where
+
+  equiv-fam-map-fam-equiv-is-torsorial :
+    ((x : A) → (a ＝ x) ≃ B x) ≃ ((x : A) → (a ＝ x) → B x)
+  equiv-fam-map-fam-equiv-is-torsorial =
+    ( equiv-inclusion-is-full-subtype
+      ( λ h → Π-Prop A (λ a → is-equiv-Prop (h a)))
+      ( fundamental-theorem-id is-torsorial-B)) ∘e
+    ( equiv-fiberwise-equiv-fam-equiv _ _)
+```
+
 ### `Id : A → (A → 𝒰)` is an embedding
 
 We first show that [the preunivalence axiom](foundation.preunivalence.md)
@@ -138,10 +163,7 @@ module _
           ( equiv-tot
             ( λ x →
               ( equiv-ev-refl x) ∘e
-              ( equiv-inclusion-is-full-subtype
-                ( Π-Prop A ∘ (is-equiv-Prop ∘_))
-                ( fundamental-theorem-id (is-torsorial-Id a))) ∘e
-              ( distributive-Π-Σ))))
+              ( equiv-fam-map-fam-equiv-is-torsorial x (is-torsorial-Id a)))))
         ( emb-tot
           ( λ x →
             comp-emb
@@ -211,6 +233,44 @@ module _
       ( is-proof-irrelevant-total-family-of-equivalences-Id)
 ```
 
+### The type of point-preserving fiberwise equivalences between `Id x` and a pointed torsorial type family is contractible
+
+**Proof:** Since `ev-refl` is an equivalence, it follows that its fibers are
+contractible. Explicitly, given a point `b : B a`, the type of maps
+`h : (x : A) → (a = x) → B x` such that `h a refl = b` is contractible. But the
+type of fiberwise maps is equivalent to the type of fiberwise equivalences.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {a : A} {B : A → UU l2} (b : B a)
+  (is-torsorial-B : is-torsorial B)
+  where
+
+  abstract
+    is-torsorial-pointed-fam-equiv-is-torsorial :
+      is-torsorial
+        ( λ (e : (x : A) → (a ＝ x) ≃ B x) →
+          map-equiv (e a) refl ＝ b)
+    is-torsorial-pointed-fam-equiv-is-torsorial =
+      is-contr-equiv'
+        ( fiber (ev-refl a {B = λ x _ → B x}) b)
+        ( equiv-Σ _
+          ( inv-equiv
+            ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B))
+          ( λ h →
+            equiv-inv-concat
+              ( inv
+                ( ap
+                  ( ev-refl a)
+                  ( is-section-map-inv-equiv
+                    ( equiv-fam-map-fam-equiv-is-torsorial a is-torsorial-B)
+                    ( h))))
+              ( b)))
+        ( is-contr-map-is-equiv
+          ( is-equiv-ev-refl a)
+          ( b))
+```
+
 ## See also
 
 - In

src/synthetic-homotopy-theory.lagda.md

@@ -12,7 +12,6 @@ module synthetic-homotopy-theory where
 open import synthetic-homotopy-theory.0-acyclic-maps public
 open import synthetic-homotopy-theory.0-acyclic-types public
 open import synthetic-homotopy-theory.1-acyclic-types public
-open import synthetic-homotopy-theory.26-id-pushout public
 open import synthetic-homotopy-theory.acyclic-maps public
 open import synthetic-homotopy-theory.acyclic-types public
 open import synthetic-homotopy-theory.category-of-connected-set-bundles-circle public
@@ -73,6 +72,7 @@ open import synthetic-homotopy-theory.functoriality-sequential-colimits 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
+open import synthetic-homotopy-theory.identity-systems-descent-data-pushouts public
 open import synthetic-homotopy-theory.induction-principle-pushouts public
 open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public