The Coq mailing list

[André Hirschowitz <ah AT unice.fr>]

> > Inductive Ztwo : Type :=
> >
> > O :Ztwo
> > | ZtwoS : {S: Ztwo ->Ztwo ;  Z2axiom :  forall n : Ztwo ,  SSn =n} .
> >
> >
> > would be problematic?
>
> Mainly because it has non sense (or I am stupid),
> I don't even understand what would be the type of ZtwoS
The intended meaning is

Variable Ztwo: Type.
Variable ZtwoO: Ztwo.
Variable ZtwoS: Ztwo ->Ztwo.
Hypothesis Z2axiom :  forall n : Ztwo ,  ZtwoS (ZtwoS n) =n.

This is not yet problematic. But we want to know more:
   - at first that these assumptions are "consistent" and also
   -some initiality, which will warrant (essential) uniqueness.

Here initiality means something like

"a function from Ztwo to another Type T is given by a term v of type T 
(for ZtwoO)
and a term r : T ->T satisfying forall x \in T, r(r x)=x.".

Initiality should be witnessed by Coq constructions extending Case and 
Fixpoint. In order to be correct, these new constructions should 
generate proof obligations. May-be this generation could be (slighty?) 
problematic.

It may be also not so easy to identify a good class of "allowed" axioms 
(for instance
ZtwoO \neq ZtwoO should be rejected).

ah