coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] the type of natural numbers

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: roconnor AT theorem.ca
Cc: BruinBear123 AT aol.com, Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] the type of natural numbers
Date: Wed, 27 Jul 2005 11:18:31 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Definition Nat := forall C: Set, C -> (C -> C) -> C.

What if pick a set A and define x:Nat to correspond to 0 for C=A and to 1 for C<>A? Is it doable? More generally, if I can define any non- constant function Set -> nat then I could "twist" a member of Nat corresponding to a member of nat by this function and get an exotic element of Nat which is not in nat.

Having Nat isomorphic to nat would mean then that there are no non- constant functions Set -> nat. Is it so?

Vladimir.

[Coq-Club] the type of natural numbers, BruinBear123
- Re: [Coq-Club] the type of natural numbers, Venanzio Capretta
- Re: [Coq-Club] the type of natural numbers, roconnor
  - Re: [Coq-Club] the type of natural numbers, Vladimir Voevodsky
- Re: [Coq-Club] the type of natural numbers, jevgenijs