Higher Coinductive Types
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.
Letbe the integers, p a prime number and be the ideal generated by , that is, numbers of the for for . Then we can consider the quotient of integers modulo for every natural number n. Now, consider the following sequence (for example in the category of rings)
where the projections are given by. Then the p-adic integers are the limit of this sequence.
Observe now that elements ofare actually sequences , such that
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
Note that there is, for every type A, a trivial introduction rule for El A: Letbe the weakened identity map, i.e., . Then the corecursion principle gives us a map .
Assume that we have defined the type, for example by just enumerating the elements, and that we have also defined the congruence-modulo relation . 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 .
Intuitively, this should give rise to the following introduction rule
Let, then I would expect the following computation rules
where forwe have a term that extracts the proof of the fact that x is an element of C n. This is analogous to used for HITs to extract proofs from composed proofs.