The Coq mailing list

[Venanzio Capretta <venanzio AT cs.kun.nl>]

I met a strange Universe inconsistency when trying to define Peter 
Aczel's type theoretic interpretation of Constructive Set Theory.

I have these definitions :

(* PART ONE *)

(* Product of two types. *)
Definition prodT : Type -> Type -> Type :=
[A, B : Type](sigT A [x:A]B).

Definition iffT : Type -> Type -> Type :=
[A, B : Type](prodT (A -> B) (B -> A)).

(* W types. *)
Inductive W [A : Type; B : A->Type] : Type :=
  sup : (a : A)(f : (B a) -> (W A B))(W A B).

(* Aczel's type of sets V. *)
Definition V := (W Type [a:Type]a).

(* (index_type a) is the Type on which the elements of a are indexed. *)
Definition index_type : V -> Type :=
[a : V]
Cases a of
  (sup A f) => A
end.

(* (index_fun a) is the indexing function defining the set a. *)
Definition index_fun : (a:V)(index_type a) -> V :=
[a : V]
<[a:V](index_type a) -> V>
Cases a of
  (sup A f) => f
end.

(* Equality for sets. *)
Fixpoint set_eq [a : V] : V -> Type :=
Cases a of
  (sup A f) => 
    [b : V]
    (prodT
      (x : A)
      (sigT (index_type b) 
        [y:(index_type b)](set_eq (f x) (index_fun b y)))
      (y : (index_type b))
      (sigT A
        [x:A](set_eq (f x) (index_fun b y)))
    )
end.

(* epsilon relation (being an element). *)
Definition set_eps : V -> V -> Type :=
[a, b : V](sigT (index_type b) [y:(index_type b)](set_eq a (index_fun b y))).

(* Definition of quantifiers over V. *)

(* Universal quantifier. *)
Definition allV : V -> (V -> Type) -> Type :=
[a : V][phi : V -> Type]
  (x : (index_type a))(phi (index_fun a x)).

(* Existential quantifier. *)
Definition exV : V -> (V -> Type) -> Type :=
[a : V][phi : V -> Type]
  (sigT (index_type a) [x:(index_type a)](phi (index_fun a x))).

Section Set_induction.

Variable phi : V -> Type.

Theorem set_induction :
  ((y : V)((allV y phi) -> (phi y))) -> (x : V)(phi x).

Intro b.
Induction x.
Intros A f h.
Apply b.
Red.
Simpl.
Assumption.

Qed.

End Set_induction.

(* END OF PART ONE *)

The type V is intended as a type of sets with the equivalence relation 
set_eq standing for extensional equality and set_eps for the membership 
relation. Now I define the union of two sets:

(* PART TWO *)

(* Definition of being an invariant formula on V :          *)
(* a formula is invariant if it is the same for equal sets. *)
Definition invariant_formula : (V -> Type) -> Type :=
  [phi : V -> Type](x, y : V)(set_eq x y) -> (phi x) -> (phi y).

Axiom allV_invariant : (phi : V -> Type)(invariant_formula phi) ->
                       (y : V)(iffT (allV y phi) 
                                    ((x:V)(set_eps x y) -> (phi x))
                              ).

(* END OF PART TWO *)

The axiom allV_invariant is actually provable, but I didn't include the 
proof for brevity (the problem persists with or without the proof).

(* PART THREE *)

Section Union.

Variable s : V.

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.

(* END OF PART THREE *)

At the point where set_union is defined I get the error:

Error: Universe Inconsistency

The strange part is that when I leave out PART TWO this doesn't happen 
and the definition of set_union is good. Also is I give PART TWO after 
PART ONE there is no problem.

Why is that happening?

(I am using Coq6.2)

An other question. Some tyme I would need to have direct control on the 
Universe index, and write explicitly Type(n), instead of letting Coq 
infer it. Is there any way of doing it, or something equivalent?

Thanks,
  Venanzio Capretta
  University of Nijmegen