The Coq mailing list

[jean-francois.monin AT imag.fr]

Robert Dockins a ecrit :
 > > Do you too run into universe inconsistencies?
 > 
 > I did.  Adding the definition of distT to the development I posted in  
 > my last email gives rise to universe inconsistencies.  I tried a  
 > number of workarounds, including adding a duplicate definition of  
 > terms under a different name, but I couldn't get anything to work.
 > 
 > I think you might be right about universe polymorphism.  The goal is  
 > to define the join operation, which has type:
 > 
 > forall A:Type, Term (Term A) -> Term A
 > 
 > If I understand the situation correctly, there isn't any way at all  
 > to define a function with this type if Term is in sort Type.   
 > Actually, you could replace Term with _any_ definition in sort Type  
 > and this would still be impossible.  

Not quite: 

Inductive Term (A:Type) : Type := TI : A -> A -> Term A.

Definition p1 : forall A:Type, Term (Term A) -> Term A.
intros A (x,y); exact x.
Defined.

Of course your example is more complex...
Best,

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 40