Higher Coinductive Types

From cLab
Revision as of 16:38, 25 May 2015 by H.basold (talk | contribs) (Created page with "== Idea == The following is rather speculative, and it only represents my (Henning) personal view on what Higher Coinductive Types should be. Since [http://ncatlab.org/nlab/s...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Idea

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 sequence [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{El} (A : \mathop{Set}) : A \to \mathop{Set} \mathop{\mathrm{where}} \\ & \quad triv : (a : A) \to \mathop{El} A a \to \mathbb{1} \end{align*} [/math]

TBC