The Coq mailing list

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

On 08/05/2012 08:51 PM, Jason Gross wrote: 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?

Does the following address your issue?


Parameter Category : forall (objC : Type), (objC -> objC -> Type) -> Type.
Parameter Functor : forall objC homC, Category objC homC
  -> forall objD homD, Category objD homD
    -> Type.

Definition functorLike := forall objC homC, Category objC homC
  -> forall objD homD, Category objD homD
    -> Type.

Definition type : functorLike :=
  fun _ _ _ _ _ _ => Type.

Definition arrow (F G : functorLike) : functorLike :=
  fun _ _ C _ _ D => F _ _ C _ _ D -> G _ _ C _ _ D.

Infix "-->" := arrow (right associativity, at level 100).

Definition NaturalTransformationType : functorLike :=
  Functor --> Functor --> type.

Eval compute in NaturalTransformationType.

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.