The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> Can I force Q to map into Type somehow, perhaps by using another layer of 
> indirection?

I can answer my own question. The following does it:

Parameter A : Type.
Definition Universe := Type.
Definition cow (P : forall (x : A), A -> Type) : Type := forall x y : A, P x 
y.
Inductive Q (x : A) : A -> Universe := horn : Q x x.
Definition q := cow Q.
Definition r := forall x y : A, Q x y.

However, I suspect I fixed the level of Q to some particular Type(i)
by doing so. Hmm. This is a second reason why we would want to work
with a fixed universe in HoTT. It's how Vladimir did things to avoid
various unviverse inconsistencies. The trouble is that there is no way
to parametrize a piece of Coq code with a universe, so we're screwed
when we want to have two levels of universes.

Any suggestions? How much beer is it worth to get better support for
explicit universes?

With kind regards,

Andrej