The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I wonder if the following "mutually inductive" definition is possible  in any 
 of the languages/proof assistants (e.g. Agda):



Inductive U (T:Type) :Type := gen: U |  prod: forall X:U, forall P: elem X -> 
Type,  U

with

fixpoint elem (X:U) : Type := 

match X with 

| gen => T

| prod Y P => forall y: elem Y, P y

end.

.


The intuition behind it is to define the universe U generated by a type T 
with respect to dependent products together with the function elem: U -> T 
which sends X:U to its underlying "type of elements". 

The basic problem here is that a type is inductively defined simultaneously 
with a fix-point function on it. 

Vladimir.