The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Nov 6, 2006, at 10:01 AM, 
jean-francois.monin AT imag.fr
 wrote:

> 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...


Humm... Well, it appears my understanding of the Type hierarchy is  
fuzzier than I thought.  It looks like some more reading is in order.


> 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


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
          -- TMBG