Connectedness (HoTT)

In (book) HoTT, A type X is n-connected iff its $n$ truncation is contraction.

$\parallel X{\parallel }_n\simeq \ast$

For any X there is a “best possible” n-type with map $X:|\_{|}_n:X\to \parallel X{\parallel }_n$

For any other n-type Y,

$$|\_{|}_n:(\parallel X{\parallel }_n\to Y)\to (X\to Y)$$

Examples: $\parallel \perp {\parallel }_{-1}=\perp$ $\parallel X{\parallel }_{-1}=\top$ for any $X\ne \perp$ $\parallel \Sigma \mathbb{N}[\_]{\parallel }_0=\mathbb{N}$ - The hSet truncation of FinSet.

Thm: $\parallel X{\parallel }_n$ is the image of

$$\begin{array}{r}X\to (X\to (n-1)-\mathrm{Type})\\ \lambda xy\to \parallel x\equiv y{\parallel }_{n-1}\end{array}$$

X is:

• -2 connected in all cases.
• -1 connected iff X is inhabited
• 0 connected iff $\exists x\in X.\forall y\in X.\parallel x\equiv y\parallel$ has one connected component.

Thm: X is n-connected iff $X\perp f$ for every n-truncation f

Thm if X is n-connected then its suspension S X is (n + 1)-connected. Proof Suppose Y is an n+1 - type $(SX\to Y)\to \Sigma ns:Y.X\to n\equiv s$

Corollory: $S^{n+1}$ is n-connected (n=1 : $S^2$ then all loops are contractable)

Serre class Theorem

Infinity-connected

X is infinity connected iff X is n-connected for all $n:\mathbb{N}$.

X is infinity tuncated iff A orth X for all $\infty$-connected A

Theorem If countable choice holds then can define $\parallel X{\parallel }_{\infty }:={\lim }_{\leftarrow }(\cdots \to \parallel X{\parallel }_n\to \parallel X{\parallel }_{n-1}\to \cdots \to \parallel X{\parallel }_0)$

Open problem: Can it be defined in general

Fact there is a model where S^2 is not $\infty$-truncated