The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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. :])