nLab W-suspension

 Idea

A W-suspension is similar to a W-type, except instead of being inductively generated by term constructors and function constructors, W-suspensions are inductively generated by term constructors and identification constructors.

 Definition

There are multiple possible definitions of a (directed, pseudo-) graph in dependent type theory:

• a graph consists of a type $A$ and a binary type family $R(x, y)$ indexed by $x:A$ and $y:A$. $A$ is the type of vertices of a graph and each $R(x, y)$ is the type of edges of a graph.

• a graph consists of a type $A$ and a type $R$ and two functions $s:R \to A$ and $t:R \to A$. $A$ is the type of vertices in $A$, and the type of edges the type of edges between $x:A$ and $y:A$ in the graph is the type

$$\sum_{r:R} (s(r) =_A x) \times (t(r) =_A y)$$

• a graph consists of types $A$ and $B$, a type family $R(z)$ indexed by $z:B$, and functions $s:B \to A$ and $t:B \to A$. $A$ is the type of vertices of a graph, $B$ is the type of endpoint configurations of edges in the graph, and $R(x)$ is the type of edges in the graph given an endpoint configuration $x:B$. Given elements $x:A$ and $y:A$, the type of edges between $x:A$ and $y:A$ in the graph is the type

$$\sum_{z:B} R(z) \times (s(z) =_A x) \times (t(z) =_A y)$$

The first definition of a graph leads to the notion of graph quotient and the second definition of a graph leads to the notion of coequalizer type. The third definition of a graph leads to the notion of a W-suspension, a higher inductive type defined in Sojakova15:

Given types $A$ and $B$, a type family $R(x)$ indexed by $x:B$, and functions $s:B \to A$ and $t:B \to A$, one could construct the W-suspension $\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$ which is generated by the graph in the following sense: there are point constructors

$$\mathrm{points}:A \to \underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$$

and for each endpoint configuration $x:B$, path constructors

$$\mathrm{paths}(x):R(x) \to \left(\mathrm{points}(s(x)) =_{\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)} \mathrm{points}(t(x))\right)$$

The recursion principle of $\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$ says that given a type $C$ together with

• a function $c_\mathrm{points}:A \to C$
• a dependent function $c_\mathrm{paths}:\prod_{x:B} R(x) \to (c_\mathrm{points}(s(x)) =_C c_\mathrm{points}(t(x)))$

there exists a function $c:\left(\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)\right) \to C$ such that

• for all $x:A$, $c(\mathrm{points}(x)) \equiv c_\mathrm{points}(x)$, and
• for all $x:B$, and $r:R(x)$, $\mathrm{ap}_c(\mathrm{paths}(s,r)) \equiv c_\mathrm{paths}(s, r)$

Similarly, the induction principle of $\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$ says that given a type family $C(z)$ indexed by $z:\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$ together with

• a dependent function $c_\mathrm{points}:\prod_{x:A} C(\mathrm{points}(x))$
• a dependent function $c_\mathrm{paths}:\prod_{x:B} \prod_{r:R(x)} c_\mathrm{points}(s(x)) =_C^{\mathrm{paths}(x,r)} c_\mathrm{points}(t(x))$

there exists a dependent function $c:\prod_{z:\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)} C(z)$ such that

• for all $x:A$, $c(\mathrm{points}(x)) \equiv c_\mathrm{points}(x)$, and
• for all $x:B$, and $r:R(x)$, $\mathrm{apd}_c(\mathrm{paths}(x,r)) \equiv c_\mathrm{paths}(x, r)$

Related concepts

• coequalizer type

• graph quotient

• W-type

 References

• Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 [arXiv:1402.0761, doi:10.1145/2775051.2676983]