# CW-Complex

CW package contains basic theorems about general theory of CW-complexes.

# FOUNDATIONS

CW-complexes are fundamental objects in homotopy type theory. They're even present 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.

**Examples.** 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) ]
```

**Shperes and Disks.** 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 $I^2$ same as of $S^2$**. 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) ([email protected]) ([email protected]))) 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 Mö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 $S^{n−1} \incmap D^n$. We study spaces obtained through iterated attachments of $D^n$ along $S^{n−1}$.

**Definition** (Attachment). Attaching n-cell to a space $X$
along a map $f : S^{n-1} \rightarrow X$ means taking a pushout

where the notation $X \cup_f D^n$ means that the result depends on homotopy class of $f$.

**Definition** (CW-Complex). Inductively. The only
CW-complex of dimention $-1$ is $\varnothing$.
A CW-complex of dimension $\leqslant n$ on $X$ is a
space $X$ obtained by attaching a collection of n-cells
to a CW-complex of dimension $n−1$.

A CW-complex is a space $X$ which is the colimit(X_i) of a sequence $X_{-1} = \varnothing \incmap X_0 \incmap X_1 \incmap X_2 \incmap ... X$ of CW-complexes $X_i$ of dimension $\leqslant n$, with $X_{i+1}$ obtained from $X_i$ by i-cell attachments. Thus if X is a CW-complex, it comes with a filtration $$ \varnothing \incmap X_0 \incmap X_1 \incmap X_2 \incmap ... X $$ where $X_i$ is a CW-complex of dimension $\leqslant i$ called the i-skeleton, and hence the filtration is called the skeletal filtration.