The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

On Mon, Jun 3, 2013 at 12:38 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

universes

I can see that if you can define types as sets of elements satisfying arbitrary specifications, then to solve the particular equality problem I used as an example, in general, would be to   solving program equivalence. Bzzzt. That said, I'd be happy with just name or syntactic equivalence. I think what you are saying is that even that level of computation with types as values is out of reach in Coq. Correct? Coq lacks functionalities to "destruct/inspect" and/or "construct" type definitions. E.g., to write a function that takes a type and returns a type that is a composition of that type with some new type information. Have I basically got this right?

And the answer is to build my own type system within Coq and to use its types, rather than Coq types, to do what I want?

Kevin