Higher Coinductive Types

From cLab
Revision as of 14:59, 26 May 2015 by H.basold (talk | contribs) (Finished p-adic integers example)
Jump to: navigation, search


The following is rather speculative, and it only represents my (Henning) personal view on what Higher Coinductive Types should be.

Since Higher Inductive Types (HITs) are all about equations, my take on Higher Coinductive Types (HiCT?) are that they represent subobjects. This is supported by the duality between equations and logics,coequalisers and equalisers, colimits and limits etc. In the following, we look at one particular example and try to give a general scheme for defining HiCTs. The latter is a combination of the Gabe Dijkstra's and my work presented at TYPES'15.

Example: p-adic integers

For the purpose of the description, it is not necessary to know what p-adic integers are, rather it suffices to know that they can be constructed as a certain limit, see Wikipedia.

Let [math]\mathbb{Z}[/math] be the integers, p a prime number and [math](p^n) \subseteq \mathbb{Z}[/math] be the ideal generated by [math]p^n[/math], that is, numbers of the for [math]p^n k[/math] for [math]k \in \mathbb{Z}[/math]. Then we can consider the quotient [math]\mathbb{Z}/(p^n)[/math] of integers modulo [math]p^n[/math] for every natural number n. Now, consider the following sequence (for example in the category of rings)

[math] 1 = \mathbb{Z}/(p^0) \xleftarrow{\pi_0} \mathbb{Z}/(p^1) \xleftarrow{\pi_1} \dotsm \mathbb{Z}/(p^n) \xleftarrow{\pi_n} \mathbb{Z}/(p^{n+1}) \dotsm [/math]

where the projections are given by [math]\pi_n(k) = k \mod p^n[/math]. Then the p-adic integers [math]\mathbb{Z}_p[/math] are the limit of this sequence.

Observe now that elements of [math]\mathbb{Z}_p[/math] are actually sequences [math](a_n)_{n \in \N}[/math], such that

  1. [math]a_n \in \mathbb{Z}/(p^n)[/math] and
  2. [math]a_n \cong a_{n+1} \pmod{p^n}[/math].

This observation allows us to view the p-adic integers as final dialgebra (coinductive type) in the following way.

Let El A be the type of elements of the type A be given by the following type

[math] \begin{align*} & \mathop{\mathrm{codata}} \mathop{\mathrm{El}} (A : \mathop{\mathrm{Set}}) : A \to \mathop{\mathrm{Set}} \mathop{\mathrm{where}} \\ & \quad triv : (a : A) \to \mathop{\mathrm{El}} A a \to \mathbf{1} \end{align*} [/math]

Note that there is, for every type A, a trivial introduction rule for El A: Let [math]\mathrm{id} : (a : A) \to \mathbf{1} \to \mathbf{1}[/math] be the weakened identity map, i.e., [math]\mathrm{id} = \lambda a \, x. x[/math]. Then the corecursion principle gives us a map [math]\mathop{\mathrm{corec}} \mathrm{id} : (a : A) \to \mathbf{1} \to \mathop{\mathrm{El}} A[/math].

Assume that we have defined the type [math]\mathbb{Z}/(p^n)[/math], for example by just enumerating the elements, and that we have also defined the congruence-modulo relation [math]\_ \cong \_ \pmod{\_}[/math]. Then the idea is that the p-adic integers at stage n are given by the following type, and the p-adic integers are then represented as [math]\Z_p = I_p \, 1[/math].

[math] \begin{align*} & \mathop{\mathrm{codata}} I_p : \N \to \mathop{\mathrm{Set}} \mathop{\mathrm{where}} \\ & \quad \begin{aligned} & \mathrm{hd} : (n : \N) \to I_p \, n \to \mathbb{Z}/(p^n) \\ & \mathrm{tl} : (n : \N) \to I_p \, n \to I_p \, (n + 1) \\ & \mathrm{proj} : (n : \N) \to (a : I_p \, n) \to \mathop{\mathrm{El}} \, (I_p \, n) \, a \to \mathop{\mathrm{hd}} a \cong \mathrm{hd} (\mathop{\mathrm{tl}} a) \pmod{p^n} \end{aligned} \end{align*} [/math]

Intuitively, this should give rise to the following introduction rule

[math] \frac{ \begin{align*} & C : \N \to \mathrm{Set} \\ & h : (n : \N) \to C \, n \to \mathbb{Z}/(p^n) \\ & t : (n : \N) \to C \, n \to C \, (n+1) \\ & p : (n : \N) \to (a : C \, n) \to \mathop{\mathrm{El}} \, (C \, n) \, a \to \mathop{\mathrm{hd}} a \cong \mathrm{hd} (\mathop{\mathrm{tl}} a) \pmod{p^n} \end{align*} }{ \mathop{\mathrm{corec}} h \, t \, p : (n : \N) \to C \, n \to I_p \, n } [/math]

Let [math]f = \mathop{\mathrm{corec}} h \, t \, p[/math], then I would expect the following computation rules

[math] \begin{align*} & \mathrm{hd} \, n \, (f \, n \, x) = h \, n \, x \\ & \mathrm{tl} \, n \, (f \, n \, x) = f \, (n+1) \, (t \, n \, x) \\ & \mathrm{proj} \, n \, (f \, n \, x) \, q = p \, n \, x \, (\mathrm{extr}_f \, q) \end{align*} [/math]

where for [math]q : \mathrm{El} \, (I_p \, n) \, (f \, n \, x)[/math] we have a term [math]\mathrm{extr}_f \, q : \mathrm{El} \, (C \, n) \, x[/math] that extracts the proof of the fact that x is an element of C n. This is analogous to [math]\mathrm{ap}_f[/math] used for HITs to extract proofs from composed proofs.

General Syntax