Sequential diagrams
Content created by Fredrik Bakke, Vojtěch Štěpančík and Egbert Rijke.
Created on 2023-10-23.
Last modified on 2024-05-23.
module synthetic-homotopy-theory.sequential-diagrams where
Imports
open import elementary-number-theory.natural-numbers open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.universe-levels
Idea
A sequential diagram (A, a)
is a sequence of
types A : ℕ → 𝒰
over the natural numbers, equipped with a family of maps
aₙ : Aₙ → Aₙ₊₁
for all n
.
They can be represented by diagrams
a₀ a₁ a₂
A₀ ---> A₁ ---> A₂ ---> ⋯
extending infinitely to the right.
Sequential diagrams are dual to inverse sequential diagrams, and are also sometimes called cotowers.
Definition
sequential-diagram : (l : Level) → UU (lsuc l) sequential-diagram l = Σ (ℕ → UU l) (λ A → (n : ℕ) → A n → A (succ-ℕ n)) module _ { l : Level} (A : sequential-diagram l) where family-sequential-diagram : ℕ → UU l family-sequential-diagram = pr1 A map-sequential-diagram : (n : ℕ) → family-sequential-diagram n → family-sequential-diagram (succ-ℕ n) map-sequential-diagram = pr2 A
module _ { l : Level} (X : UU l) where constant-sequential-diagram : sequential-diagram l pr1 constant-sequential-diagram _ = X pr2 constant-sequential-diagram _ x = x
Properties
The identity type of sequential diagrams is characterized in the file about equivalences of sequential diagrams.
Postcomposition sequential diagrams
Given a sequential diagram A
and a type X
there is a sequential diagram
X → A
defined by levelwise postcomposition.
(f₀ ∘ -) (f₁ ∘ -) (f₂ ∘ -)
(X → A₀) -------> (X → A₁) -------> (X → A₂) -------> (X → A₃) -------> ⋯
module _ {l1 l2 : Level} (X : UU l1) (A : sequential-diagram l2) where postcomp-sequential-diagram : sequential-diagram (l1 ⊔ l2) pr1 postcomp-sequential-diagram n = X → family-sequential-diagram A n pr2 postcomp-sequential-diagram n g x = map-sequential-diagram A n (g x)
A sequential diagram of contractible types consists of equivalences
This is an easy corollary of the fact that every map between contractible types is an equivalence.
module _ {l1 : Level} {A : sequential-diagram l1} where is-equiv-sequential-diagram-is-contr : ((n : ℕ) → is-contr (family-sequential-diagram A n)) → (n : ℕ) → is-equiv (map-sequential-diagram A n) is-equiv-sequential-diagram-is-contr contrs n = is-equiv-is-contr ( map-sequential-diagram A n) ( contrs n) ( contrs (succ-ℕ n))
References
- [SvDR20]
- Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, 845–858. Association for Computing Machinery, 07 2020. doi:10.1145/3373718.3394801.
Recent changes
- 2024-05-23. Fredrik Bakke. Fix citation tag configuration for some references (#1143).
- 2024-04-18. Vojtěch Štěpančík. Equivalences are closed under "transfinite composition" (#1117).
- 2024-04-10. Vojtěch Štěpančík. Shifts and unshifts of concepts around sequential colimits (#1070).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2024-01-11. Fredrik Bakke. Rename "towers" to "inverse sequential diagrams" (#990).