[Agda] Positive but not strictly positive types

[Martin Escardo]

On 09/04/15 17:07, Vilhelm Sjöberg wrote:
> On 2015-04-09 11:49, Andrés Sicard-Ramírez wrote:
>> Retaking the discussion in
>> http://thread.gmane.org/gmane.comp.lang.agda/6008, it's known that
>> using *negative* types it's possible
>>
>> a) to prove absurdity or
>> b) to write non-terminating terms.
>>
>> Is there some example in *Agda* of a positive but not strictly
>> positive type which allows a) or b)?
> I'm interested in the answer to this question also. If I correctly
> understand what Thierry Coquand wrote in the thread you mention, the
> answer is no; because Agda is predicative allowing positive datatypes
> would be sound. But it would be interesting to see this fleshed out more.
> 
> I wrote up a blog post about using non-strictly positive datatypes to
> get a paradox in Coq:
> http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/

If you modify the construction on your post (by Coquand) replacing
Prop by the two-point type 2 (the booleans) with points 0 and 1, you
won't get a contradiction.

data N : Set where
 flatten : ((N -> 2) -> 2) -> N

Andrej Bauer, Alex Simpson and myself looked at the initial algebra of
((- -> 2) -> 2) in cartesian closed categories of topological spaces
in 2007 (in Siberia, during a Domains workshop).

Moreover, the initial algebra is the natural numbers object!

What follows is sketchy and a bit technical and you may wish to skip
it.

But you may wish to see a Haskell version of part of this by
Andrej in his nice blog post
http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/

Firstly, (N->2) is the "Cantor space", a compact Hausdorff space, and
2 is a discrete space. And for any compact Hausdorff space C and any
discrete space D, the exponential (C->D) exists and is a again a
discrete space.

So the exponential ((N->2)->2) is discrete. But also, for any space X,
the continuous maps X->2 are (in bijection with) the clopens (clopen
and open sets). And the Cantor space has countably many clopens.

So ((N->2)->2) is a countable discrete space, and hence homeomorphic
(that is, isomorphic) to N. What Andrej does in his post is to
implement such an isomorphism in Haskell.

Now we need to actually construct an initial algebra ((N->2)->2)->N.

First, build any isomorphism phi:N->((N->2)->2) such that the modulus
of uniform continuity of the function phi(n) is <= n. (I think
Andrej's construction in the blog will do, but anyway this can be
done.)

Then the inverse of phi is an initial algebra. Here is Alex's
argument: Given an algebra f: ((X->2)->2)->X we need to construct the
unique homomorphism h: N->X. The homomorphism property gives the
following recursive equation for h:

  h(n) = f(\p. phi(n)(\m. p(h(m))))

which is well-defined and uniquely determined by induction on n, using
the assumed property of phi.

This argument works e.g. in the topological topos, which is a model of
type theory.

Hence you won't be able to derive any contradiction from an initial
algebra for ((- -> 2) -> 2). You won't be able to construct looping
programs either, because all this can be done from the assumption of a
modulus-of-uniform continuity functional, which can be computably
realized.

More interestingly, phi is also a final coalgebra. But I will skip
this here, so that you have something to think about yourself. :-)

However, I don't think we have thought about the following question:
work in type theory (e.g. in Agda or Coq) assuming an initial algebra
for this functor. Can we show it is isomorphic to the natural numbers,
without assuming uniform continuity principles for the Cantor space?
And then perhaps derive a uniform continuity principle from this?

Martin