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 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)$$

• 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)$$

These definitions of graph result in different possible definitions of a W-suspension, whose points are generated by the vertices of the graph and whose paths are generated by the edges of the graph.

W-suspensions of binary type families

The first notion of graph leads to the following higher inductive type:

Given a graph $(A, R)$, one could construct the W-suspension $\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)$ which is generated by the graph in the following sense: there are point constructors

$$\mathrm{points}:A \to \underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)$$

and for each $x:A$ and $y:A$, path constructors

$$\mathrm{paths}(x, y):R(x, y) \to \left(\mathrm{points}(x) =_{\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)} \mathrm{points}(y)\right)$$

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

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

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

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

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

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

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

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

The large recursion principle of $\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)$ says that given

• a type family $x:A \vdash C(x)$
• a dependent function $c_\mathrm{equiv}:\prod_{x:A} \prod_{y:A} R(x, y) \to (C(x) \simeq C(y))$

there exists a type family $z:\left(\underset{x:A, y:A}{\mathrm{Wsus}} R(x, y)\right) \vdash D(z)$ such that

• for all $x:A$, $D(c(x)) \equiv C(x)$, and
• for all $x:A$, $y:A$, and $r:R(x, y)$, $\mathrm{tr}_C(\mathrm{paths}(x,y,r)) \equiv c_\mathrm{equiv}(x, y, r):C(x) \simeq C(y)$

Sojakova W-suspensions

The second notion of graph leads to the following higher inducive 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)$

W-suspensions of parallel functions

For the final notion of graph, the resulting definition of W-suspension is just the coequalizer type of $s:R \to A$ and $t:R \to A$.

$$\mathrm{Wsus}_{R,A}(s, t) \coloneqq \mathrm{coeq}_{R,A}(s, t)$$

Relation between the definitions

W-suspensions in the first sense could be constructed as the coequalizer of the left and middle dependent pair projections $\pi_{\sum}^A$ and $\pi_{\sum}^A \circ \pi_{\sum}^{\sum_{y:A} R(-, y)}$ of the dependent pair type $\sum_{x:A} \sum_{y:A} R(x, y)$, both of which have domain $\sum_{x:A} \sum_{y:A} R(x, y)$ and codomain $A$:

$$\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y) \coloneqq \mathrm{coeq}_{\sum_{x:A} \sum_{y:A} R(x, y),A}(\pi_{\sum}^A, \pi_{\sum}^A \circ \pi_{\sum}^{\sum_{y:A} R(-, y)})$$

Alternatively, given two parallel functions $s:B \to A$ and $t:B \to A$, the coequalizer of $s$ and $t$ could be defined as the W-suspension (in the first sense) generated by the graph defined by the family of dependent sum types $\sum_{z:B} (s(z) =_A x) \times (t(z) =_A y)$

$$\underset{x:A,y:A}{\mathrm{Wsus}} \sum_{z:B} (s(z) =_A x) \times (t(z) =_A y)$$

Related concepts

• coequalizer type

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