natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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.
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
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.
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
and for each $x:A$ and $y:A$, path constructors
The recursion principle of $\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)$ says that given a type $C$ together with
there exists a function $c:\left(\underset{x:A, y:A}{\mathrm{Wsus}} R(x, y)\right) \to C$ such that
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
there exists a dependent function $c:\prod_{z:\underset{x:A, y:A}{\mathrm{Wsus}} R(x, y)} C(z)$ such that
The large recursion principle of $\underset{x:A,y:A}{\mathrm{Wsus}} R(x, y)$ says that given
there exists a type family $z:\left(\underset{x:A, y:A}{\mathrm{Wsus}} R(x, y)\right) \vdash D(z)$ such that
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
and for each endpoint configuration $x:B$, path constructors
The recursion principle of $\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)$ says that given a type $C$ together with
there exists a function $c:\left(\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)\right) \to C$ such that
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
there exists a dependent function $c:\prod_{z:\underset{x:B}{\mathrm{Wsus}^{s, t}} R(x)} C(z)$ such that
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$.
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$:
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)$
Last revised on February 1, 2024 at 21:04:43. See the history of this page for a list of all contributions to it.