Product Type in Coq

Question

I'm having trouble passing a parameter to a product type in coq. I have a definition that looks like,

    Definition bar (a:Type) := a->Type.

I need to define a function that takes in 'a' and the thing made by 'bar a' and outputs their product/ordered pair. So I tried the following.

    Definition foo (a:Type)(b:bar a):= prod a b.

Which gives me the error

The term "b" has type "bar a" while it is expected to have type "Type".

What's really confusing here is that this,

    Definition foo (a:Type) := prod a (bar a). 

works just fine. Clearly 'bar a' has type 'Type', so I'm not sure how to fix my original definition. I suspect I'm not passing variables properly.

Answer 1

To see an error, expand bar a in your foo definition:

Definition foo (a:Type)(b:a->Type):= prod a b.

Now it should be clear that b is not a type, it is a function from a to Type.

And as you never get an object of type a, you can't apply b to anything, and can't get a Type from it.

For the second definition, expand again to see why it works:

Definition foo (a:Type) := prod a (a->Type).

Both a and a->Type are valid Type's for a product.