The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.