Connected CW complexes (#1133)

* t * duplicate * wups * rme * ganea stuff * w * w * w * fix * stuff * stuff * more * .. * done? * wups * wups * wups * fixes * ugh... * wups * stuff * stuff * stuff * stuf * More * stuff * stuff * stuff * done? * stuff * cleanup * readme * wups * ugh * wups * broken code * ojdå * comments * Pointed * done? * p2 * stuff * wip... * stuff * almost * pretty much done * cleaning * cleaning * connected done? * connected clean * minor * fixes
agda · Sep 19, 2024 · 53e400e · 53e400e
1 parent e2370fb
commit 53e400e
Show file tree

Hide file tree

Showing 17 changed files with 3,065 additions and 96 deletions.
diff --git a/Cubical/CW/Base.agda b/Cubical/CW/Base.agda
@@ -7,6 +7,7 @@ module Cubical.CW.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Pointed
 
 open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
 open import Cubical.Data.Nat.Order
@@ -102,6 +103,9 @@ isFinCW {ℓ = ℓ} X =
 finCW : (ℓ : Level) → Type (ℓ-suc ℓ)
 finCW ℓ = Σ[ A ∈ Type ℓ ] ∥ isFinCW A ∥₁
 
+finCW∙ : (ℓ : Level) → Type (ℓ-suc ℓ)
+finCW∙ ℓ = Σ[ A ∈ Pointed ℓ ] ∥ isFinCW (fst A) ∥₁
+
 finCWexplicit : (ℓ : Level) → Type (ℓ-suc ℓ)
 finCWexplicit ℓ = Σ[ A ∈ Type ℓ ] (isFinCW A)
 
@@ -147,6 +151,10 @@ to_cofibCW n C x = inr x
 CW↪∞ : (C : CWskel ℓ) → (n : ℕ) → fst C n → realise C
 CW↪∞ C n x = incl x
 
+CW↪Iterate : ∀ {ℓ} (T : CWskel ℓ) (n m : ℕ) → fst T n → fst T (m +ℕ n)
+CW↪Iterate T n zero = idfun _
+CW↪Iterate T n (suc m) x = CW↪ T (m +ℕ n) (CW↪Iterate T n m x)
+
 finCW↑ : (n m : ℕ) → (m ≥ n) → finCWskel ℓ n → finCWskel ℓ m
 fst (finCW↑ m n p C) = fst C
 fst (snd (finCW↑ m n p C)) = snd C .fst