The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Vladimir: That would probably work (at one point, I was doing this using [Set] for [uu0.UU], and [Type] for [uu1.UU]), but I don't like having to keep track of which things should be in which universe (it is nice when Coq can do it for me, and I like having it so that a functor is a functor, regardless of what level of category it comes from), and it is slightly annoying to maintain two copies of all my code.  Thanks!, though.

Adam: that sounds like it would work, but it's not clear to me how to formalize it.  Do you have an example, or more details you could give me?

Thanks!

-Jason

On Fri, Aug 3, 2012 at 6:48 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

May be this would help. In the Univalent Foundations library I routinely had to deal with two universe levels (originally with three). I wrote all the constructions which used only one universe in file uu.v where at the start one introduces a universe by

Definition UU:=Type.

and then works consistently with this UU. Then made copies of this file uu0, uu1, uu2. When I need two universes I import uu0 and uu1 and introduce notations

Notation UU0: = uu0.UU .

Notation UU1 := uu1.UU .

and then consistently use these two universes. Then, if really needed one can make several copies of the files with two-level universe hierarchies and import them to the ones using three levels. 

It is certainly better than to use the opaque and messy universe management of Coq.

Vladimir.

On Fri, Aug 3, 2012 at 8:20 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Jason Gross wrote:

For example, it would be nice if I could not have to say that a natural transformation was of type
  NaturalTransformation : forall objC homC (C : @Category objC homC) objD homD (D : @Category objD homD), @Functor objC homC C objD homD D -> @Functor objC homC C objD homD D -> Type
and instead say that a NaturalTransformation was of type
  NaturalTransformation : forall (C : @Category _ _) (D : @Category _ _), @Functor C D -> @Functor C D -> Type

Why not define a new [->]-like operator that does the quantification in its definition?  Basically, the game is to abstract out common quantification patterns into operators.