nLab graph quotient

 Idea

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

Definition

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.

Given a graph $(A, R)$, one could construct the graph quotient $A / R$ which is generated by the graph in the following sense: there are point constructors

$$\mathrm{points}:A \to (A / R)$$

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

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

The recursion principle of $A / R$ 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:(A / R) \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 $A / R$ says that given a type family $C(z)$ indexed by $z:A / R$ 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:A / R} 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 $A / R$ 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:A / R \vdash D(z)$ such that

• for all $x:A$, $D(\mathrm{points}(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)$

Relation to coequalizer types

Graph quotients can 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$:

$$A / R \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 graph quotient generated by the graph defined by the family of dependent sum types $\sum_{z:B} (s(z) =_A x) \times (t(z) =_A y)$

$$A / \sum_{z:B} (s(z) =_A -) \times (t(z) =_A -)$$

Related concepts

• coequalizer type

• W-suspension

• W-type

References

• Egbert Rijke, The join construction, 26 Jan 2017, (arXiv:1701.07538)