Refactor the descent property of pushouts (#1145)

The module `26-descent` is replaced with a collection of files written
in the "new" style, defining descent data, morphisms and equivalences,
and showing the descent property.

There is currently some duplication with the development in
`26-id-pushout`, where I tried to make the absolute minimum changes
required for it to typecheck, since I'll be replacing the entire file in
an upcoming PR.

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-descent 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
@@ -48,15 +47,19 @@ 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-pushouts public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
+open import synthetic-homotopy-theory.descent-property-pushouts public
 open import synthetic-homotopy-theory.descent-property-sequential-colimits public
 open import synthetic-homotopy-theory.double-loop-spaces public
 open import synthetic-homotopy-theory.eckmann-hilton-argument public
 open import synthetic-homotopy-theory.equifibered-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
+open import synthetic-homotopy-theory.equivalences-descent-data-pushouts public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
+open import synthetic-homotopy-theory.families-descent-data-pushouts public
 open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
@@ -83,6 +86,7 @@ open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequenti
 open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows public
 open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
+open import synthetic-homotopy-theory.morphisms-descent-data-pushouts public
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.null-cocones-under-pointed-span-diagrams public