# 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.

```
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) ]
```

`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 ]
```

**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 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

where the notation

A CW-complex is a space