The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Actually, as I have accidentally discovered recently there is a way to 
control the universe assignment in Coq. For example, one can start one's 
development with something like that:


Definition Type1:=Type.
Definition Type0:Type1:=Type.
Definition jj01:Type0 -> Type1:= fun T => T.  

This fixes two universes Type0 and Type1 such that Type0:Type1 and Type0 is a 
sub-universe of Type1. In further development you may use Type0 or Type1 
everywhere instead of Type. Some definitions may have to be repeated twice 
once for Type0 and once for Type1. 

Vladimir. 




On Sep 9, 2010, at 12:11 AM, Adam Chlipala wrote:

> Daniel Schepler wrote:
>> Then I proved a lemma:
>> 
>> Lemma eq_dep_is_pair_equality_after_conversion:
>>   forall (U:Type) (P:U->Type) (p q:U) (x:P p) (y:P q),
>>     eq_dep U P p x q y<->
>>        p = q /\
>>        forall (e:P p=P q),
>>          y = convert_equal_types (P p) (P q) e x.
>> 
>> That seems to abstract out the role of q in y's type enough so that I can 
>> now
>> "apply<- eq_dep_is_pair_equality_after_conversion" and then do rewrites.
>> 
>> But I was wondering if there was a more standard way to deal with dependent
>> types in proving statements like eq_dep.
>>   
> 
> I haven't used this library yet, but you might find it helpful:
>    http://www.pps.jussieu.fr/~gil/Heq/
> 
>> The other problem I ran into is that when I tried to define the category of
>> categories, it gave a universe error.  I think I see what it's complaining
>> about, that trying to input Category into an instance of Category violates 
>> the
>> type hierarchy.  So I guess I'd need to say something like "the category of
>> level n categories is a level n+1 category".  But I'm not sure how to do 
>> that.
>>   
> 
> Every few months, someone asks this question on coq-club. :)
> 
> The answer is that you are out of luck, if you want to keep encoding 
> category theoretic concepts without introducing a layer of syntax.  Coq has 
> no universe polymorphism.  Not only that, but there is no way to mention 
> universe levels explicitly in source code, let alone quantify over unknown 
> levels.  (Maybe a Coq developer will point out some recent feature (perhaps 
> debugging-oriented) for including explicit levels, but I've never seen one. 
> :])