- reindex spheres
- define pmap in terms of ppi

- move move_to_lib and pointed to library

talk with Favonia about:
- dependent pointed maps
- higher cube filling strategies
- HIT equivalences
- algebra


/-
Adjointness:
Σ X ⟶ Y    X ∧ Y → Z
=======    ===========
X → Ω Y    X → (Y → Z)

Spectrum: Y : ℕ → Type* with e : Ω Yₙ₊₁ ≃* Yₙ.


HOMOLOGY:
Hₙ(X, Y) :≡? ∥ X ∧ Ω² (Y (n+2)) ∥₀ ≃ ∥ X ∧ Y n ∥₀

Eilenberg Steenrod-axioms:
H : ℤ → Type* → AbGroup
- functorial in second argument
- (optional): respects pointed equivalences and pointed homotopies
axioms:
- the canonical map
-
- Given (Xᵢ)ᵢ : I → Type* (satisfying AC?) the canonical functor
  ⊕ hₙ
-/