nLab coequalizer type

Idea

The instantiation of a coequalizer as a type in dependent type theory.

Definition

In dependent type theory, given types $A$ and $B$ and functions $f:A \to B$ and $g:A \to B$, the coequalizer type or coequaliser type of $f$ and $g$ is a higher inductive type $\mathrm{coeq}_{A,B}(f, g)$. There are two different way to define the coequalizer type. The first way states that $\mathrm{coeq}_{A,B}(f, g)$ is generated by the constructors

$$\mathrm{in} \colon B \to \mathrm{coeq}_{A,B}(f, g)$$

$$\mathrm{glue} \colon \prod_{x:A}in(f(x)) =_{\mathrm{coeq}_{A,B}(f, g)} in(g(x))$$

The second way states that $\mathrm{coeq}_{A,B}(f, g)$ is generated by

$$\mathrm{in} \colon B \to \mathrm{coeq}_{A,B}(f, g)$$

$$\mathrm{glue} \colon \prod_{x:B} \prod_{y:B} \prod_{z:A} (f(z) =_B x) \to (g(z) =_B y) \to (\mathrm{in}(x) =_{\mathrm{coeq}_{A,B}(f, g)} \mathrm{in}(y))$$

Induction and recursion principles

The recursion principle for coequalizer types says that given a type $C$ together with

• a function $c_\mathrm{in}:B \to C$
• a dependent function $c_\mathrm{glue}:\prod_{x:B} \prod_{y:B} \prod_{z:A} (f(z) =_B x) \to (g(z) =_B y) \to (c_\mathrm{in}(x) =_C c_\mathrm{in}(y))$

there exists a function $c:\mathrm{coeq}_{A, B}(f, g) \to C$ such that

• for all $x:B$, $c(\mathrm{in}(x)) \equiv c_\mathrm{in}(x)$, and
• for all $x:B$, $y:B$, $z:A$, $p:f(z) =_B x$, and $q:g(z) =_B y$,
  $$\mathrm{ap}_c(\mathrm{glue}(x,y,z,p,q)) \equiv c_\mathrm{glue}(x, y, z, p, q)$$

Similarly, the induction principle says that given a type family $C(w)$ indexed by $w:\mathrm{coeq}_{A, B}(f, g)$ together with

• a dependent function $c_\mathrm{in}:\prod_{x:B} C(\mathrm{in}(x))$
• a dependent function $c_\mathrm{glue}:\prod_{x:B} \prod_{y:B} \prod_{z:A} \prod_{p:f(z) =_B x} \prod_{q:g(z) =_B y} c_\mathrm{in}(x) =_C^{\mathrm{glue}(x,y,z,p,q)} c_\mathrm{in}(y)$

there exists a dependent function $c:\prod_{z:\mathrm{coeq}_{A, B}(f, g)} C(z)$ such that

• for all $x:B$, $c(\mathrm{in}(x)) \equiv c_\mathrm{points}(x)$, and
• for all $x:B$, $y:B$, $z:A$, $p:s(z) =_B x$, and $q:g(z) =_B y$,
  $$\mathrm{apd}_c(\mathrm{glue}(x,y,z,p,q)) \equiv c_\mathrm{glue}(x,y,z,p,q)$$

Properties

Relation to W-suspensions

W-suspensions could be constructed as the coequalizer type 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 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)$$

Examples

• The sum type of a type $T$ with itself is the coequalizer of two copies of the unique function $\mathrm{rec}_\emptyset^T$ from the empty type to $T$.
  $$T + T \coloneqq \mathrm{coeq}_{\emptyset, T}(\mathrm{rec}_\emptyset^T, \mathrm{rec}_\emptyset^T)$$
• The circle type is the coequalizer of any two endofunctions $f:C \to C$ and $g:C \to C$ on a contractible type $C$.
  $$S^1 \coloneqq \mathrm{coeq}_{C, C}(f, g) \quad \mathrm{given} \quad p:\mathrm{isContr}(C)$$
• The interval type is the coequalizer of the constant functions with value $\mathrm{false}$ and $\mathrm{true}$ from any contractible type $C$ to the boolean domain.
  $$\mathbb{I} \coloneqq \mathrm{coeq}_{C, \mathrm{bool}}(\mathrm{const}_{C, \mathrm{bool}}(\mathrm{false}). \mathrm{const}_{C, \mathrm{bool}}(\mathrm{true})) \quad \mathrm{given} \quad p:\mathrm{isContr}(C)$$
• More generally, the suspension of a type $T$ is the coequalizer of the constant functions with value $\mathrm{false}$ and $\mathrm{true}$ from $T$ to the boolean domain.
  $$\Sigma T \coloneqq \mathrm{coeq}_{T, \mathrm{bool}}(\mathrm{const}_{T, \mathrm{bool}}(\mathrm{false}). \mathrm{const}_{T, \mathrm{bool}}(\mathrm{true}))$$
• The cyclic group of order $n + 1$ for natural number $n:\mathbb{N}$ is the coequalizer of the constant functions with value $0$ and $n + 1$ from any contractible type $C$ to the natural numbers type.
  $$\mathbb{Z}_{n + 1} \coloneqq \mathrm{coeq}_{C, \mathbb{N}}(\mathrm{const}_{C, \mathbb{N}}(0), \mathrm{const}_{C, \mathbb{N}}(n + 1)) \quad \mathrm{given} \quad p:\mathrm{isContr}(C)$$
• The pushout of a span $f:C \to A$ and $g:C \to B$ is the coequalizer of the composite functions $\mathrm{in}_{A + B}^A \circ f$ and $\mathrm{in}_{A + B}^B \circ g$, each with domain $C$ and codomain the sum type $A + B$:
  $$A \sqcup_{f,g}^C B \coloneqq \mathrm{coeq}_{C, A + B}(\mathrm{in}_{A + B}^A \circ f, \mathrm{in}_{A + B}^B \circ g)$$

Propositional truncation

The propositional truncation of a h-set $A$ is the set truncation of the coequalizer of the two product projection functions $\pi_1:A \times A \to A$ and $\pi_2:A \times A \to A$ of the product type $A \times A$

$$\Vert A \Vert_{-1} \coloneqq \Vert \mathrm{coeq}_{A \times A,A}(\pi_1, \pi_2) \Vert_0$$

See also

• coequalizer, homotopy coequalizer
• propositional truncation
• W-suspension

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)