Redirected from "W-suspensions".
Contents
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 and a binary type family indexed by and . is the type of vertices of a graph and each is the type of edges of a graph.
-
a graph consists of types and , a type family indexed by , and functions and . is the type of vertices of a graph, is the type of endpoint configurations of edges in the graph, and is the type of edges in the graph given an endpoint configuration . Given elements and , the type of edges between and in the graph is the type
- a graph consists of a type and a type and two functions and . is the type of vertices in , and the type of edges the type of edges between and 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.
W-suspensions of binary type families
The first notion of graph leads to the following higher inductive type:
Given a graph , one could construct the W-suspension which is generated by the graph in the following sense: there are point constructors
and for each and , path constructors
The recursion principle of says that given a type together with
- a function
- a dependent function
there exists a function such that
- for all , , and
- for all , , and ,
Similarly, the induction principle of says that given a type family indexed by together with
- a dependent function
- a dependent function
there exists a dependent function such that
- for all , , and
- for all , , and ,
The large recursion principle of says that given
- a type family
- a dependent function
there exists a type family such that
- for all , , and
- for all , , and ,
Sojakova W-suspensions
The second notion of graph leads to the following higher inducive type defined in Sojakova15:
Given types and , a type family indexed by , and functions and , one could construct the W-suspension which is generated by the graph in the following sense: there are point constructors
and for each endpoint configuration , path constructors
The recursion principle of says that given a type together with
- a function
- a dependent function
there exists a function such that
- for all , , and
- for all , and ,
Similarly, the induction principle of says that given a type family indexed by together with
- a dependent function
- a dependent function
there exists a dependent function such that
- for all , , and
- for all , and ,
W-suspensions of parallel functions
For the final notion of graph, the resulting definition of W-suspension is just the coequalizer type of and .
Relation between the definitions
W-suspensions in the first sense could be constructed as the coequalizer of the left and middle dependent pair projections and of the dependent pair type , both of which have domain and codomain :
Alternatively, given two parallel functions and , the coequalizer of and could be defined as the W-suspension (in the first sense) generated by the graph defined by the family of dependent sum types
References