The Coq mailing list

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

On 06/03/2013 12:25 PM, Kevin Sullivan wrote:
> Hi folks, sorry for a newbie question. I've started playing around 
> with types as values, but I'm not sure how to do simple computations 
> with such values. One such computation would be comparison for 
> equality. I'm obviously missing some basic knowlege. Here's a simple 
> but broken program that should make my intent clear. What do I need to 
> go read to make this work? Thanks!
>
> Definition teq (t1 t2: Set) : bool :=
>   if (t1 = t2) then true else false.

What you're asking for is impossible in general.  Very few useful 
"computations" can be performed directly on Coq types.  Instead, when 
such computations seem necessary, folks use deep embeddings of type 
syntax (sometimes called "universes") with functions compiling them into 
types.

Perhaps Chapter 11 of CPDT <http://adam.chlipala.net/cpdt/> would be of 
interest as an example.