# Higher Coinductive Types

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

## 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.

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 be 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 of are actually sequence , such that,

1. and
2. .

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

TBC