CW

CW module contains basic definitions and theorems about general theory of CW-complexes.

FOUNDATIONS

CW-complexes are fundamental objects in homotopy type theory. They're presented in cubical type checker in the form of higher (co)-inductive types (HITs). Just like regular (co)-inductive types could be described as recursive terminating (well-founded) or non-terminating trees, higher inductive types could be described as CW-complexes. Defining HIT means to define some CW-complex directly using cubical homogeneous composition structure as an element of initial algebra inside cubical model.

(HIT). With a given context variables Δ,K ⊢ (Γ,Ξ,Ψ,𝜑,𝑒) and telescope (𝛿 : Δ) (𝑖 : 𝕀) (𝜑 : 𝔽) (𝑢₀: H 𝛿 [𝜑 ↦ 𝑢[0/𝑖]]) every HIT is defines as: 1) ctorⁱ (𝛾: Γⁱ [𝛿]) (𝑥: Ξⁱ [𝛿,𝛾] → H 𝛿) (s: Ψₓ) : H 𝛿 [𝜑ₛ ↦ 𝑒[𝛾,𝑥]]; 2) hcompⁱ [𝜑 ↦ 𝑢] 𝑢₀ : H 𝛿 [𝜑 ↦ 𝑢[1/𝑖]]; 3) transpⁱ 𝜑 𝑢₀ : H 𝛿 [1] [𝜑 ↦ 𝑢₀].

. One of the notables is pushout as it's used to define the cell attachment formally, as others cofibrant objects.

data pushout (A B C: U) (f: C -> A) (g: C -> B)
       = po1 (_: A)
       | po2 (_: B)
       | po3 (c: C) <i> [ (i = 0) -> po1 (f c) ,
                          (i = 1) -> po2 (g c) ]

. Here are some examples of using dimensions to construct spherical shapes.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ]

data S2 = point | surf <i j> [ (i = 0) -> point, (i = 1) -> point,
                               (j = 0) -> point, (j = 1) -> point ]

data D3 (x: S2) = border (x: S2)
    | space <i j k> [ ( i = 0) -> border x, (i = 1) -> border x ,
                      ( j = 0) -> border x, (j = 1) -> border x ,
                      ( k = 0) -> border x, (k = 1) -> border x ]

. Structure of same as of . ASCII proof that comp parameters are the same as in surf constructor:

I2 (A: U) (a0 a1 b0 b1: A) (u: Path A a0 a1) (v: Path A b0 b1)
      (r0: Path A a0 b0) (r1: Path A a1 b1) : U
      = PathP (<i> (PathP (<j> A) (u@i) (v@i))) r0 r1

plain (A: U) (x: A): I2 A x x x x (<i> x) (<i> x) (<i> x) (<i> x)
      = <i j> comp (<_>A) x [(i = 0) -> <i> x, (i = 1) -> <i> x,
                             (j = 0) -> <i> x, (j = 1) -> <i> x ]

Recursive and parametrised HITs such as Truncation and Quotients along with Hopf construction became possible after hcomptrans branch in cubicaltt and paper "On Higher Inductive Types in Cubical Type Theory" by Thierry Coquand, Simon Huber, and Anders Mörtberg. This paper describes decomposing of composition operation into homogeneous composition and transport operation, so that they preserve the universe level and are strictly stable under substitution. This decomposition is intended to solve the problem of interpretation of higher inductive types with parameters.

MATHEMATICS

In definition of homotopy groups, a special role belongs to inclusions . We study spaces obtained through iterated attachments of along .

(Attachment). Attaching n-cell to a space along a map means taking a pushout

where the notation means that the result depends on homotopy class of .

(CW-Complex). Inductively. The only CW-complex of dimention is . A CW-complex of dimension on is a space obtained by attaching a collection of n-cells to a CW-complex of dimension .

A CW-complex is a space which is the colimit(X_i) of a sequence of CW-complexes of dimension , with obtained from by i-cell attachments. Thus if X is a CW-complex, it comes with a filtration where is a CW-complex of dimension called the i-skeleton, and hence the filtration is called the skeletal filtration.