The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

           Dear Venanzio,

The reason of your problem is that Coq does not support the so-called
universe polymorphism. This means that all the instance of a given
constant are supposed to live in the same universe. In your case, the
axiom allV_invariant, induces a constraint over the universe of the
constant sigT, which is incompatible with its later use in set_union.


The easy patch is to duplicate the fautive constants; in your case,
the following will do:


(* PART THREE *)

Section Union.

Variable s : V.

Inductive sigT' [A : Type; P : A->Type] : Type :=
      existT' : (x:A)(P x)->(sigT' A P).


Local A := (sigT' (index_type s)
                 [x : (index_type s)](index_type (index_fun s x))).

Local g : A -> V :=
  [a : A]Cases a of
           (existT' x y) => (index_fun (index_fun s x) y)
         end.

Definition set_union : V := (sup ? ? A g).

End Union.



I should point out that Lego supports universe polymorphism.

I agree that the implicit universes of Coq can quickly get a pain in
the ass, and that explicit universe variables should be prefered. My
best choice would be some system similar to the one implemented in
NuPRL.

So far for the direct answer to your question. I however wanted to
point out that I already did a formalization of Peter Aczel's
encoding in Coq. It is included in the distribution in
contrib/Rocq/ZF.

I wrote a (short) paper about this, for the last TACS conference (LNCS
1281, also available on my web page).

I my encoding, I mainly focused on an impredicative version of Aczel's
encoding, that is, set-theoretical propositions are encoded in the
universe Prop.

The drawback of the impredicative encoding is that the existential
quantifier is less constructive, since one cannot extract the witness
of a proof of "there exists a set s.t. ...".

The advantages of the impredicative encoding are:

* The obtained set theory is more powerfull (one has the powerset).

* One has not to deal with the painful distinctions between restricted
and unrestricted quantification, as it is necessary in Aczel's CZF
(precisely, for keeping the universe consistency). You might very well
encounter some problems when reaching that point.


To sum up, the predicative encoding is for the real
constructivist. The impredicative one is more comfortable and gives
more information about the logical strength of the system.


In my encoding, I included a file which contains some of the
predicative encoding (Constructive.v). But it is far les developped
than the predicative one.


Another example of playing with universes can be found in my
developement, in the file Hierarchy.v, wich sketches how to exhibit an
inaccessible cardinal, by using an additional universe.



Best wishes,




Benjamin Werner
----------------------------------------------------------------------------
Projet Coq
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: 
Benjamin.Werner AT inria.fr
Phone:  +33 (1) 39 63 52 31
Mobile: +33 (6) 11 82 55 02
Fax:    +33 (1) 39 63 56 84
http://pauillac.inria.fr/~werner
-----------------------------------------------------------------------------