Cleanup style and prose for SDR20 formalization

src/papers/SDR20.lagda.md

@@ -1,200 +1,303 @@
 # Sequential Colimits in Homotopy Type Theory
 
-{{#cite SDR20}}
+This file collects references to formalization of constructions and theorems
+from {{#cite SDR20}}.
 
 ```agda
 module papers.SDR20 where
 ```
 
-## 3. Sequences and Sequential Colimits
+## 2 Homotopy Type Theory
 
-Definition 3.1: Sequences. We call sequences _sequential diagrams_.
+The second section introduces basic notions from homotopy type theory, which we
+import below for completeness.
 
 ```agda
-import synthetic-homotopy-theory.sequential-diagrams using
-  ( sequential-diagram)
+open import foundation.universe-levels using
+  ( UU
+  )
+open import foundation.identity-types using
+  ( Id -- "path"
+  ; refl -- "constant path"
+  ; inv -- "inverse path"
+  ; concat -- "concatenation of paths"
+  ; assoc -- "associativity of concatenation"
+  )
+open import foundation.action-on-identifications-functions using
+  ( ap -- "functions respect paths"
+  )
+open import foundation.homotopies using
+  ( _~_ -- "homotopy"
+  )
+open import foundation.equivalences using
+  ( equiv -- "equivalence"
+  )
+open import foundation.univalence using
+  ( univalence -- "the univalence axiom"
+  ; map-eq -- "function p̅ associated to a path"
+  )
+open import foundation.function-extensionality using
+  ( funext -- "the function extensionality axiom"
+  )
+open import foundation.fibers-of-maps using
+  ( fiber -- "the homotopy fiber of a function"
+  )
+open import foundation.transport-along-identifications using
+  ( tr -- "transport"
+  )
+open import foundation.action-on-identifications-dependent-functions using
+  ( apd -- "dependent functions respect paths"
+  )
+open import foundation.truncated-types using
+  ( is-trunc -- "`n`-truncated types"
+  )
+open import foundation.truncations using
+  ( trunc -- "the `n`-truncation of a type"
+  ; unit-trunc -- "the unit map into a type's `n`-truncation"
+  ; is-truncation-trunc -- "precomposing by the unit is an equivalence"
+  )
+open import foundation.connected-types using
+  ( is-connected -- "`n`-connected types"
+  )
+open import foundation.truncated-maps using
+  ( is-trunc-map -- "`n`-truncated functions"
+  )
+open import foundation.connected-maps using
+  ( is-connected-map -- "`n`-connected functions"
+  )
 ```
 
-Definition 3.2: Sequential colimits and their induction and recursion
-principles, given by the dependent and non-dependent universal properties,
-respectively. Our homotopies in the definitions of cocones go from left to
-right, instead of right to left.
+## 3 Sequences and Sequential Colimits
+
+The third section defines what one might call the (wild) category of sequences
+(which are called _sequential diagrams_ in agda-unimath) and the colimiting
+functor. It concludes by defining shifts of sequences, showing that they induce
+equivalences on sequential colimits, and defines lifts of elements in a
+sequential diagram.
+
+**Definition 3.1**: Sequences.
 
 ```agda
-import synthetic-homotopy-theory.sequential-colimits using
-  ( standard-sequential-colimit ;
-    map-cocone-standard-sequential-colimit ;
-    coherence-cocone-standard-sequential-colimit ;
-    dup-standard-sequential-colimit ;
-    up-standard-sequential-colimit)
+open import synthetic-homotopy-theory.sequential-diagrams using
+  ( sequential-diagram
+  )
 ```
 
-Lemma 3.3: Uniqueness property of the sequential colimit.
+**Definition 3.2**: Sequential colimits and their induction and recursion
+principles.
+
+Induction and recursion are given by the dependent and non-dependent universal
+properties, respectively. Since we work in a setting without computational
+higher inductive types, the maps induced by induction and recursion only compute
+up to a path, even on points. Our homotopies in the definitions of cocones go
+from left to right (i.e. `iₙ ~ iₙ₊₁ ∘ aₙ`), instead of right to left.
+
+Our formalization works with sequential colimits specified by a cocone with a
+universal property, and results about the standard construction of colimits are
+obtained by specialization to the canonical cocone.
 
 ```agda
-import synthetic-homotopy-theory.sequential-colimits using
-  ( equiv-htpy-htpy-out-of-standard-sequential-colimit ;
-    htpy-htpy-out-of-standard-sequential-colimit)
+open import synthetic-homotopy-theory.sequential-colimits using
+  ( standard-sequential-colimit -- the canonical colimit type
+  ; map-cocone-standard-sequential-colimit -- "the canonical injection"
+  ; coherence-cocone-standard-sequential-colimit -- "the glue"
+  ; dup-standard-sequential-colimit -- "the induction principle"
+  ; up-standard-sequential-colimit -- "the recursion principle"
+  )
 ```
 
-Definition 3.4: Natural transformations and natural equivalences between
-sequential diagrams. We call natural transformations _morphisms of sequential
-diagrams_.
+**Lemma 3.3**: Uniqueness property of the sequential colimit.
+
+The data of a homotopy between two functions out of the standard sequential
+colimit is specified by the type `htpy-out-of-standard-sequential-colimit`,
+which we can then turn into a proper homotopy.
 
 ```agda
-import synthetic-homotopy-theory.morphisms-sequential-diagrams using
-  ( hom-sequential-diagram ;
-    id-hom-sequential-diagram ;
-    comp-hom-sequential-diagram)
-import synthetic-homotopy-theory.equivalences-sequential-diagrams using
-  ( equiv-sequential-diagram)
+open import synthetic-homotopy-theory.sequential-colimits using
+  ( htpy-out-of-standard-sequential-colimit -- data of a homotopy
+  ; htpy-htpy-out-of-standard-sequential-colimit -- "data of a homotopy induces a homotopy"
+  )
 ```
 
-Lemma 3.5: Functoriality of the Sequential Colimit.
+**Definition 3.4**: Natural transformations and natural equivalences between
+sequential diagrams.
+
+We call natural transformations _morphisms of sequential diagrams_, and natural
+equivalences _equivalences of sequential diagrams_.
 
 ```agda
-import synthetic-homotopy-theory.functoriality-sequential-colimits using
-  ( map-hom-standard-sequential-colimit ; -- 1)
-    preserves-id-map-hom-standard-sequential-colimit ; -- 2
-    preserves-comp-map-hom-standard-sequential-colimit ; -- 3
-    htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram ; -- 4
-    equiv-equiv-standard-sequential-colimit) -- 5
+open import synthetic-homotopy-theory.morphisms-sequential-diagrams using
+  ( hom-sequential-diagram -- "natural transformation"
+  ; id-hom-sequential-diagram -- "identity natural transformation"
+  ; comp-hom-sequential-diagram -- "composition of natural transformations"
+  )
+open import synthetic-homotopy-theory.equivalences-sequential-diagrams using
+  ( equiv-sequential-diagram -- "natural equivalence"
+  )
 ```
 
-Lemma 3.6: Dropping a head of a sequential diagram preserves the sequential
-colimit.
+**Lemma 3.5**: Functoriality of the Sequential Colimit.
 
 ```agda
-import synthetic-homotopy-theory.shifts-sequential-diagrams using
-  ( up-cocone-shift-sequential-diagram ;
-    compute-sequential-colimit-shift-sequential-diagram) -- apply to 1
+open import synthetic-homotopy-theory.functoriality-sequential-colimits using
+  ( map-hom-standard-sequential-colimit -- "a natural transformation induces a map"
+  ; preserves-id-map-hom-standard-sequential-colimit -- "1∞ ~ id(A∞)"
+  ; preserves-comp-map-hom-standard-sequential-colimit -- "(σ ∘ τ)∞ ~ σ∞ ∘ τ∞"
+  ; htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram -- "homotopy of natural transformations induces a homotopy"
+  ; equiv-equiv-standard-sequential-colimit -- "if τ is an equivalence, then τ∞ is an equivalence"
+  )
 ```
 
-Lemma 3.7: Dropping finitely many objects from the head of a sequential diagram
-preserves the sequential colimit.
+**Lemma 3.6**: Dropping a head of a sequential diagram preserves the sequential
+colimit.
+
+**Lemma 3.7**: Dropping finitely many vertices from the beginning of a
+sequential diagram preserves the sequential colimit.
+
+Denoting by `A[k]` the sequence `A` with the first `k` vertices removed, we show
+that the type of cocones under `A[k]` is equivalent to the type of cocones under
+`A`, and conclude that any sequential colimit of `A[k]` also has the universal
+property of a colimit of `A`. Specializing to the standard sequential colimit,
+we get and equivalence `A[k]∞ ≃ A∞`.
 
 ```agda
-import synthetic-homotopy-theory.shifts-sequential-diagrams using
-  ( compute-sequential-colimit-shift-sequential-diagram)
+open import synthetic-homotopy-theory.shifts-sequential-diagrams using
+  ( compute-sequential-colimit-shift-sequential-diagram -- "A[k]∞ ≃ A∞"
+  )
+compute-sequential-colimit-shift-sequential-diagram-once =
+  λ l (A : sequential-diagram l) →
+    compute-sequential-colimit-shift-sequential-diagram A 1
 ```
 
-Liftings?
+## 4 Fibered Sequences
 
-## 4. Fibered Sequences
+The fourth section defines fibered sequences, which we call _dependenct
+sequential diagrams_ in the library. It introduces the "Σ of a sequence", which
+we call the _total sequential diagram_, and asks the main question about the
+interplay between Σ and taking the colimit.
 
-Definition 4.1: Fibered sequences. In agda-unimath, a "sequence fibered over a
-sequence (A, a)" is called a "dependent sequential diagram over (A, a)", and it
-is defined in its curried form: instead of `B : Σ (n : ℕ) A(n) → 𝒰`, we use
-`B : (n : N) → A(n) → 𝒰`.
+The paper defines fibered sequences as a family over the total space
+`B : Σ ℕ A → 𝒰`, but we use the curried definition `B : (n : ℕ) → A(n) → 𝒰`.
+
+**Definition 4.1**: Fibered sequences. Equifibered sequences.
 
 ```agda
-import synthetic-homotopy-theory.dependent-sequential-diagrams using
-  ( dependent-sequential-diagram)
-  -- TODO?: equifibered sequences
+open import synthetic-homotopy-theory.dependent-sequential-diagrams using
+  ( dependent-sequential-diagram -- "A sequence (B, b) fibered over (A, a)"
+  )
 ```
 
-Lemma 4.2: The descent property of sequential colimits
+**Lemma 4.2**: The type of families over a colimit is equivalent to the type of
+equifibered sequences.
+
+This property is also called the _descent property of sequential colimits_,
+because it characterizes families over a sequential colimit.
 
 ```agda
 -- TODO
 ```
 
-Definition 4.3: Total sequential diagram of a dependent sequential diagram.
+**Definition 4.3**: Σ of a fibered sequence.
 
 ```agda
-import synthetic-homotopy-theory.total-sequential-diagrams using
-  ( total-sequential-diagram ;
-    pr1-total-sequential-diagram)
+open import synthetic-homotopy-theory.total-sequential-diagrams using
+  ( total-sequential-diagram -- "Σ (A, a) (B, b)"
+  ; pr1-total-sequential-diagram -- "the canonical projection"
+  )
 ```
 
-TODO: Decide how to treat (C∞, c∞).
+TODO: (C∞, c∞).
 
-## 5. Colimits and Sums
+## 5 Colimits and Sums
 
-Theorem 5.1: Interaction between `colim` and `Σ`.
+**Theorem 5.1**: Interaction between `colim` and `Σ`.
 
 ```agda
 -- TODO
 ```
 
-## 6. Induction on the Sum of Sequential Colimits
+## 6 Induction on the Sum of Sequential Colimits
 
--- The induction principle for a sum of sequential colimits follows from the
+```agda
+-- TODO
+```
 
-## 7. Applications of the Main Theorem
+## 7 Applications of the Main Theorem
 
-Lemma 7.1: TODO description
+**Lemma 7.1**: TODO description.
 
 ```agda
 -- TODO
 ```
 
-Lemma 7.2: Colimit of the terminal sequential diagram is contractible
+**Lemma 7.2**: Colimit of the terminal sequential diagram is contractible.
 
 ```agda
 -- TODO
 ```
 
-Lemma 7.3: Encode-decode. This principle is called the _Fundamental theorem of
-identity types_ in the library.
+**Lemma 7.3**: Encode-decode.
+
+This principle is called the _Fundamental theorem of identity types_ in the
+library.
 
 ```agda
-import foundation.fundamental-theorem-of-identity-types using
+open import foundation.fundamental-theorem-of-identity-types using
   ( fundamental-theorem-id)
 ```
 
-Lemma 7.4: Characterization of path spaces of images of the canonical maps into
-the sequential colimit.
+**Lemma 7.4**: Characterization of path spaces of images of the canonical maps
+into the sequential colimit.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.5: The loop space of a sequential colimit is the sequential colimit
-of loop spaces.
+**Corollary 7.5**: The loop space of a sequential colimit is the sequential
+colimit of loop spaces.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.6: For a morphism of sequential diagrams, the fibers of the induced
-map between sequential colimits are characterized as sequential colimits of the
-fibers.
+**Corollary 7.6**: For a morphism of sequential diagrams, the fibers of the
+induced map between sequential colimits are characterized as sequential colimits
+of the fibers.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.7.1: If each type in a sequential diagram is `k`-truncated, then the
-colimit is `k`-truncated.
+**Corollary 7.7.1**: If each type in a sequential diagram is `k`-truncated, then
+the colimit is `k`-truncated.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.7.2: The `k`-truncation of a sequential colimit is the sequential
-colimit of `k`-truncations.
+**Corollary 7.7.2**: The `k`-truncation of a sequential colimit is the
+sequential colimit of `k`-truncations.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.7.3: If each type in a sequential diagram is `k`-connected, then the
-colimit is `k`-connected.
+**Corollary 7.7.3**: If each type in a sequential diagram is `k`-connected, then
+the colimit is `k`-connected.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.7.4: If each component of a morphism between sequential diagrams is
-`k`-truncated/`k`-connected, then the induced map of sequential colimits is
+**Corollary 7.7.4**: If each component of a morphism between sequential diagrams
+is `k`-truncated/`k`-connected, then the induced map of sequential colimits is
 `k`-truncated/`k`-connected.
 
 ```agda
 -- TODO
 ```
 
-Corollary 7.7.5: If each map in a sequential diagram is
+**Corollary 7.7.5**: If each map in a sequential diagram is
 `k`-truncated/`k`-connected, then the first injection into the colimit is
 `k`-truncated/`k`-connected.