$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

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


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.


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

$$ \begin{array}{ccc} S^{n-1} & \mapright{\mathbf{f}} & X \\ \mapdown{} & & \mapdown{} \\ D^n & \mapright{} & X \cup_f D^n \\ \end{array} $$

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.